1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
/* run.config*
STDOPT: +"-machdep gcc_x86_64"
*/
#include <string.h>
volatile int nondet;
struct empty {};
struct empty global_empty;
struct empty *pg = &global_empty;
typedef struct {
int a;
struct empty e;
int b;
} comp;
typedef struct {
struct empty s;
int i;
} comp_begin;
typedef struct {
char ch;
struct empty ss;
} comp_end;
comp f(comp s, comp *p) {
comp res;
res.a = s.b + 10;
res.b = s.a - 3;
res.e = nondet ? s.e : p->e;
return res;
}
//@ assigns \result \from \nothing;
struct empty ret_empty(void);
/*@ assigns \result \from pg;
ensures \result == pg;
*/
struct empty * ret_ptr_empty(void);
int main() {
struct empty e1, e2;
//@ assert sizeof(e1) == 0;
e1 = global_empty;
Frama_C_show_each_global_empty(global_empty);
Frama_C_show_each_e1(e1);
memcpy(&e2, &e1, sizeof(e1)); // imprecise, no builtin
comp c1, c2;
c1.a = 42;
c1.b = 77;
c1.e = e1;
memcpy(&c2, &c1, sizeof(c1)); // imprecise, no builtin
Frama_C_show_each_c2(c2);
Frama_C_show_each_c2_e(c2.e);
comp res = f(c2, &c1);
res.e = c1.e;
Frama_C_show_each_res(res);
comp_begin cb = {.i = 91};
comp_end ce = {.ch = 'Z'};
struct empty *p = &cb.s;
//@ assert \valid(p);
ce.ss = *p;
struct empty ret = ret_empty();
struct empty * ptr_ret = ret_ptr_empty();
struct empty copy_ptr_ret = *ptr_ret;
return 0;
}
|
