File tree Expand file tree Collapse file tree 2 files changed +39
-0
lines changed
regression/goto-instrument/replace-function-body-union-with-const-member Expand file tree Collapse file tree 2 files changed +39
-0
lines changed Original file line number Diff line number Diff line change 1+ #include <assert.h>
2+
3+ union WithConstMember {
4+ int non_const ;
5+ const int is_const ;
6+ };
7+
8+ union WithConstMember globalUnion ;
9+ void havoc_union (union WithConstMember * u );
10+
11+ int main (void )
12+ {
13+ union WithConstMember paramUnion ;
14+ globalUnion .non_const = 10 ;
15+ paramUnion .non_const = 20 ;
16+ assert (globalUnion .non_const == 10 );
17+ assert (globalUnion .is_const == 10 );
18+ assert (paramUnion .non_const == 20 );
19+ assert (paramUnion .is_const == 20 );
20+ havoc_union (& paramUnion );
21+ assert (globalUnion .non_const == 10 );
22+ assert (globalUnion .is_const == 10 );
23+ assert (paramUnion .non_const == 20 );
24+ assert (paramUnion .is_const == 20 );
25+ }
Original file line number Diff line number Diff line change 1+ CORE
2+ main.c
3+ --replace-function-body 'havoc_union' --replace-function-body-options 'havoc,params:.*,globals:(?!__).*'
4+ ^SIGNAL=0$
5+ ^EXIT=10$
6+ ^\[main.assertion.1\] assertion globalUnion.non_const == 10: SUCCESS$
7+ ^\[main.assertion.2\] assertion globalUnion.is_const == 10: SUCCESS$
8+ ^\[main.assertion.3\] assertion paramUnion.non_const == 20: SUCCESS$
9+ ^\[main.assertion.4\] assertion paramUnion.is_const == 20: SUCCESS$
10+ ^\[main.assertion.5\] assertion globalUnion.non_const == 10: FAILURE$
11+ ^\[main.assertion.6\] assertion globalUnion.is_const == 10: FAILURE$
12+ ^\[main.assertion.7\] assertion paramUnion.non_const == 20: FAILURE$
13+ ^\[main.assertion.8\] assertion paramUnion.is_const == 20: FAILURE$
14+ ^VERIFICATION FAILED$
You can’t perform that action at this time.
0 commit comments