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
|
/* run.config
OPT: -val -print -journal-disable -scope-verbose 1 -remove-redundant-alarms -context-width 3
*/
/*
echo '!Db.Scope.check_asserts();;' \
| bin/toplevel.top -val tests/scope/bts383.c
*/
int v;
void if1 (int * p) {
if (*p > 0)
v = *p;
}
int if2 (int c, int * p) {
if (c)
v = *p;
return *p;
}
void loop1 (int * p) {
int i;
int n = *p;
for (i = 0; i < n; i++) {
v = *p;
}
}
int loop2 (int n, int * p) {
int i;
for (i = 0; i < n; i++) {
v = *p;
}
return *p;
}
void out_char (char c);
void out_string (const char *value)
{
for(; *value; value++)
out_char(*value);
}
typedef struct { int a; int b; } Tstruct;
int fstruct (Tstruct * ps) {
int x;
ps->a = 3;
ps->b = 5;
ps->a = ps->b;
ps->b = ps->a;
x = ps->a + ps->b;
ps++;
ps->a = 3;
ps->b = 5;
ps->a = ps->b;
ps->b = ps->a;
x += ps->a + ps->b;
return x;
}
int main (int * p, Tstruct * ps) {
int x;
x = *(p+1);
v = *(p+1);
if1(p+1);
if2(x,p+1);
loop1(p+1);
loop2(x,p+1);
out_string(p+1);
x += fstruct (ps+1);
return x;
}
|
