File tree Expand file tree Collapse file tree 4 files changed +46
-0
lines changed Expand file tree Collapse file tree 4 files changed +46
-0
lines changed Original file line number Diff line number Diff line change 1+ int main ()
2+ {
3+ _Bool u = 1 ;
4+ _Bool * p = & u ;
5+
6+ // combination of _Bool, dereference, and pre-increment side-effect
7+ if (++ (* p ) != 1 )
8+ __CPROVER_assert (0 , "" );
9+
10+ // combination of _Bool, dereference, and compound assignment side-effect
11+ if (((* p ) += 1 ) != 1 )
12+ __CPROVER_assert (0 , "" );
13+
14+ // combination of _Bool, dereference, and assignment side-effect
15+ if (((* p ) = 1 ) != 1 )
16+ __CPROVER_assert (0 , "" );
17+
18+ __CPROVER_assert (* p == 1 , "" );
19+ }
Original file line number Diff line number Diff line change 1+ KNOWNBUG
2+ bool6.c
3+
4+ ^EXIT=0$
5+ ^SIGNAL=0$
6+ ^VERIFICATION SUCCESSFUL$
7+ --
8+ ^warning: ignoring
Original file line number Diff line number Diff line change 1+ #include <assert.h>
2+
3+ int main ()
4+ {
5+ _Bool u = 1 ;
6+
7+ // assert the type of side effects on _Bool
8+ assert (sizeof (++ u ) == sizeof (_Bool ));
9+ assert (sizeof (u += 1 ) == sizeof (_Bool ));
10+ assert (sizeof (u = 1 ) == sizeof (_Bool ));
11+ }
Original file line number Diff line number Diff line change 1+ KNOWNBUG
2+ bool7.c
3+
4+ ^EXIT=0$
5+ ^SIGNAL=0$
6+ ^VERIFICATION SUCCESSFUL$
7+ --
8+ ^warning: ignoring
You can’t perform that action at this time.
0 commit comments