File tree 2 files changed +62
-0
lines changed
regression/goto-instrument/replace-function-body-complex-struct
2 files changed +62
-0
lines changed Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+ #include <stdlib.h>
3
+
4
+ struct ComplexStruct
5
+ {
6
+ struct
7
+ {
8
+ int some_variable ;
9
+ const int some_constant ;
10
+ } struct_contents ;
11
+ union {
12
+ int some_integer ;
13
+ double some_double ;
14
+ } union_contents ;
15
+ struct ComplexStruct * pointer_contents ;
16
+ };
17
+
18
+ void havoc_complex_struct (struct ComplexStruct * p );
19
+
20
+ int main (void )
21
+ {
22
+ struct ComplexStruct child_struct = {{11 , 21 }, {.some_integer = 31 }, NULL };
23
+ struct ComplexStruct main_struct = {
24
+ {10 , 20 }, {.some_double = 13.0 }, & child_struct };
25
+ assert (main_struct .pointer_contents -> struct_contents .some_variable == 11 );
26
+ assert (main_struct .struct_contents .some_variable == 10 );
27
+ assert (main_struct .struct_contents .some_constant == 20 );
28
+ assert (
29
+ main_struct .union_contents .some_double < 14.0 &&
30
+ main_struct .union_contents .some_double > 12.0 );
31
+
32
+ havoc_complex_struct (& main_struct );
33
+
34
+ // everything (except constants) in the main struct was havocced
35
+ assert (main_struct .pointer_contents -> struct_contents .some_variable == 11 );
36
+ assert (main_struct .struct_contents .some_variable == 10 );
37
+ assert (main_struct .struct_contents .some_constant == 20 );
38
+ assert (
39
+ main_struct .union_contents .some_double < 14.0 &&
40
+ main_struct .union_contents .some_double > 12.0 );
41
+ // the child struct was NOT havocced because we can't follow pointers
42
+ assert (child_struct .struct_contents .some_variable == 11 );
43
+ assert (child_struct .union_contents .some_integer == 31 );
44
+ assert (child_struct .pointer_contents == NULL );
45
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.c
3
+ --replace-function-body 'havoc_complex_struct' --replace-function-body-options 'havoc,params:.*'
4
+ ^SIGNAL=0$
5
+ ^EXIT=10$
6
+ \[main.assertion.1\] assertion main_struct.pointer_contents->struct_contents.some_variable == 11: SUCCESS
7
+ \[main.assertion.2\] assertion main_struct.struct_contents.some_variable == 10: SUCCESS
8
+ \[main.assertion.3\] assertion main_struct.struct_contents.some_constant == 20: SUCCESS
9
+ \[main.assertion.4\] assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: SUCCESS
10
+ \[main.assertion.5\] assertion main_struct.pointer_contents->struct_contents.some_variable == 11: FAILURE
11
+ \[main.assertion.6\] assertion main_struct.struct_contents.some_variable == 10: FAILURE
12
+ \[main.assertion.7\] assertion main_struct.struct_contents.some_constant == 20: SUCCESS
13
+ \[main.assertion.8\] assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: FAILURE
14
+ \[main.assertion.9\] assertion child_struct.struct_contents.some_variable == 11: SUCCESS
15
+ \[main.assertion.10\] assertion child_struct.union_contents.some_integer == 31: SUCCESS
16
+ \[main.assertion.11\] assertion child_struct.pointer_contents == NULL: SUCCESS
17
+ ^VERIFICATION FAILED$
You can’t perform that action at this time.
0 commit comments