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

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

+1-1
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

+1
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

-4
This file was deleted.

‎regression/invariants/.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
driver

‎regression/invariants/Makefile

+32
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

+88
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

+4-2
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

+13
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

+12
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

+13
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$

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

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
dummy_parameter.c
3+
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-failure3/test.desc

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

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

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
dummy_parameter.c
3+
precondition-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-failure5/test.desc

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

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

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
dummy_parameter.c
3+
postcondition-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-failure7/test.desc

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

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

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
dummy_parameter.c
3+
check-return-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-failure9/test.desc

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

‎regression/symex2/Makefile

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
default: tests.log
2+
3+
test:
4+
@../test.pl -c ../../../src/cbmc/cbmc
5+
6+
tests.log: ../test.pl
7+
@../test.pl -c ../../../src/cbmc/cbmc/
8+
9+
show:
10+
@for dir in *; do \
11+
if [ -d "$$dir" ]; then \
12+
vim -o "$$dir/*.c" "$$dir/*.out"; \
13+
fi; \
14+
done;
15+
16+
clean:
17+
find -name '*.out' -execdir $(RM) '{}' \;
18+
find -name '*.gb' -execdir $(RM) '{}' \;
19+
$(RM) tests.log

‎regression/symex2/array1/main.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
2+
struct some_struct
3+
{
4+
int x, y, z;
5+
} some_struct_array[10];
6+
7+
int some_int_array[10];
8+
9+
int main()
10+
{
11+
int i;
12+
13+
// zero initialization
14+
assert(some_int_array[1]==0);
15+
if(i>=0 && i<10) assert(some_int_array[i]==0);
16+
17+
some_int_array[5]=5;
18+
assert(some_int_array[1]==0);
19+
assert(some_int_array[5]==5);
20+
}

‎regression/symex2/array1/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--clustering
4+
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
^warning: ignoring

‎regression/symex2/function_pointer1/main.c

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
2+
void (*f_ptr)(void);
3+
4+
int global;
5+
6+
void f1(void)
7+
{
8+
global=1;
9+
}
10+
11+
void f2(void)
12+
{
13+
global=2;
14+
}
15+
16+
int main()
17+
{
18+
int input;
19+
20+
f_ptr=f1;
21+
f_ptr();
22+
assert(global==1);
23+
24+
f_ptr=f2;
25+
f_ptr();
26+
assert(global==2);
27+
28+
f_ptr=input?f1:f2;
29+
f_ptr();
30+
assert(global==(input?1:2));
31+
}

0 commit comments

Comments
 (0)