Skip to content

Commit dfc1ea4

Browse files
reuktheyoucheng
reuk
authored and
theyoucheng
committed
Initialise variables in symex_target_equation.h
Corrected simplify lhs in ai_domain_baset The boolean flag was the wrong way round for ai_simplify_lhs - this corrects this. Added unit tests to validate the return meaning of ai_simplify_lhs These tests use a mock implementation of the `ai_domain_baset` interface just to validate that true means no simplification. Fix nullptr Fix linter errors, ignoring big-int and miniz Allow invariants with structured exceptions Revert "[depends: diffblue#1063] Use nullptr to represent null pointers (targets master)" goto-symex^2: goto-symex for symbolic execution Goto merged before jumping out the goto-symex operator loop, for handling GOTO and ASSERT
1 parent f1aedd6 commit dfc1ea4

File tree

65 files changed

+2841
-137
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

65 files changed

+2841
-137
lines changed

‎.travis.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ install:
159159

160160
script:
161161
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
162-
COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
162+
COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
163163
eval ${PRE_COMMAND} ${COMMAND}
164164
- COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
165165
eval ${PRE_COMMAND} ${COMMAND}

‎regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ DIRS = ansi-c \
66
goto-instrument \
77
goto-instrument-typedef \
88
goto-diff \
9+
invariants \
910
test-script \
1011
# Empty last line
1112

‎regression/cbmc/invariant-failure/main.c

Lines changed: 0 additions & 4 deletions
This file was deleted.

‎regression/invariants/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
driver

‎regression/invariants/Makefile

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
default: tests.log
2+
3+
SRC = driver.cpp
4+
5+
INCLUDES = -I ../../src
6+
7+
OBJ += ../../src/util/util$(LIBEXT)
8+
9+
include ../../src/config.inc
10+
include ../../src/common
11+
12+
test: driver$(EXEEXT)
13+
@if ! ../test.pl -c ../driver ; then \
14+
../failed-tests-printer.pl ; \
15+
exit 1 ; \
16+
fi
17+
18+
tests.log: ../test.pl driver$(EXEEXT)
19+
@if ! ../test.pl -c ../driver ; then \
20+
../failed-tests-printer.pl ; \
21+
exit 1 ; \
22+
fi
23+
24+
show:
25+
@for dir in *; do \
26+
if [ -d "$$dir" ]; then \
27+
vim -o "$$dir/*.c" "$$dir/*.out"; \
28+
fi; \
29+
done;
30+
31+
driver$(EXEEXT): $(OBJ)
32+
$(LINKBIN)

‎regression/invariants/driver.cpp

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
/*******************************************************************\
2+
3+
Module: Invariant violation testing
4+
5+
Author: Chris Smowton, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Invariant violation testing
11+
12+
#include <string>
13+
#include <sstream>
14+
#include <util/invariant.h>
15+
16+
/// An example of structured invariants-- this contains fields to
17+
/// describe the error to a catcher, and also produces a human-readable
18+
/// message containing all the information for use by the current aborting
19+
/// invariant implementation and/or any generic error catcher in the future.
20+
class structured_error_testt: public invariant_failedt
21+
{
22+
std::string pretty_print(int code, const std::string &desc)
23+
{
24+
std::ostringstream ret;
25+
ret << "Error code: " << code
26+
<< "\nDescription: " << desc;
27+
return ret.str();
28+
}
29+
30+
public:
31+
const int error_code;
32+
const std::string description;
33+
34+
structured_error_testt(
35+
const std::string &file,
36+
const std::string &function,
37+
int line,
38+
const std::string &backtrace,
39+
int code,
40+
const std::string &_description):
41+
invariant_failedt(
42+
file,
43+
function,
44+
line,
45+
backtrace,
46+
pretty_print(code, _description)),
47+
error_code(code),
48+
description(_description)
49+
{
50+
}
51+
};
52+
53+
/// Causes an invariant failure dependent on first argument value.
54+
/// One ignored argument is accepted to conform with the test.pl script,
55+
/// which would be the input source file for other cbmc driver programs.
56+
/// Returns 1 on unexpected arguments.
57+
int main(int argc, char** argv)
58+
{
59+
if(argc!=3)
60+
return 1;
61+
std::string arg=argv[1];
62+
if(arg=="structured")
63+
INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
64+
else if(arg=="string")
65+
INVARIANT(false, "Test invariant failure");
66+
else if(arg=="precondition-structured")
67+
PRECONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
68+
else if(arg=="precondition-string")
69+
PRECONDITION(false);
70+
else if(arg=="postcondition-structured")
71+
POSTCONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
72+
else if(arg=="postcondition-string")
73+
POSTCONDITION(false);
74+
else if(arg=="check-return-structured")
75+
CHECK_RETURN_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
76+
else if(arg=="check-return-string")
77+
CHECK_RETURN(false);
78+
else if(arg=="unreachable-structured")
79+
UNREACHABLE_STRUCTURED(structured_error_testt, 1, "Structured error"); // NOLINT
80+
else if(arg=="unreachable-string")
81+
UNREACHABLE;
82+
else if(arg=="data-invariant-structured")
83+
DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
84+
else if(arg=="data-invariant-string")
85+
DATA_INVARIANT(false, "Test invariant failure");
86+
else
87+
return 1;
88+
}

‎regression/cbmc/invariant-failure/test.desc renamed to ‎regression/invariants/invariant-failure/test.desc

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
CORE
2-
main.c
3-
--test-invariant-failure
2+
dummy_parameter.c
3+
string
44
^EXIT=(0|127|134|137)$
55
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
Test invariant failure
68
Invariant check failed
79
^(Backtrace)|(Backtraces not supported)$
810
--

‎regression/invariants/invariant-failure10/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
dummy_parameter.c
3+
unreachable-structured
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
Invariant check failed
8+
Error code: 1
9+
Description: Structured error
10+
^(Backtrace)|(Backtraces not supported)$
11+
--
12+
^warning: ignoring
13+
^VERIFICATION SUCCESSFUL$

‎regression/invariants/invariant-failure11/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
dummy_parameter.c
3+
data-invariant-string
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
Test invariant failure
8+
Invariant check failed
9+
^(Backtrace)|(Backtraces not supported)$
10+
--
11+
^warning: ignoring
12+
^VERIFICATION SUCCESSFUL$

‎regression/invariants/invariant-failure12/test.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
dummy_parameter.c
3+
data-invariant-structured
4+
^EXIT=(0|127|134|137)$
5+
^SIGNAL=0$
6+
--- begin invariant violation report ---
7+
Invariant check failed
8+
Error code: 1
9+
Description: Structured error
10+
^(Backtrace)|(Backtraces not supported)$
11+
--
12+
^warning: ignoring
13+
^VERIFICATION SUCCESSFUL$

0 commit comments

Comments
 (0)