File tree 2 files changed +14
-7
lines changed
cbmc/pragma_cprover_enable_disable_multiple
contracts/assigns_enforce_havoc_object 2 files changed +14
-7
lines changed Original file line number Diff line number Diff line change @@ -7,10 +7,12 @@ int main()
7
7
8
8
#pragma CPROVER check push
9
9
#pragma CPROVER check enable "pointer-overflow"
10
- #pragma CPROVER check enable "pointer-overflow" // should not print an error message
10
+ // should not print an error message
11
+ #pragma CPROVER check enable "pointer-overflow"
11
12
#pragma CPROVER check push
12
13
#pragma CPROVER check disable "pointer-primitive"
13
- #pragma CPROVER check enable "pointer-primitive" // should print an error message
14
+ // should print an error message
15
+ #pragma CPROVER check enable "pointer-primitive"
14
16
#pragma CPROVER check pop
15
17
#pragma CPROVER check pop
16
18
return 0 ;
Original file line number Diff line number Diff line change 2
2
#include <stdlib.h>
3
3
4
4
int x = 0 ;
5
- typedef struct stc {
5
+ typedef struct stc
6
+ {
6
7
int i ;
7
8
int j ;
8
9
} stc ;
9
10
10
- typedef struct stb {
11
+ typedef struct stb
12
+ {
11
13
stc * c ;
12
14
} stb ;
13
15
14
- typedef struct sta {
15
- union {
16
+ typedef struct sta
17
+ {
18
+ union
19
+ {
16
20
stb * b ;
17
21
int i ;
18
22
int j ;
@@ -23,7 +27,8 @@ int nondet_int();
23
27
24
28
void bar (sta * a )
25
29
{
26
- if (nondet_bool ()) return ;
30
+ if (nondet_bool ())
31
+ return ;
27
32
__CPROVER_havoc_object (a -> u .b -> c );
28
33
return ;
29
34
}
You can’t perform that action at this time.
0 commit comments