Newer
Older
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
[kernel] Parsing tests/syntax/Refresh_visitor.i (no preprocessing)
Start
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] tests/syntax/Refresh_visitor.i:17: Warning:
assertion got status unknown.
[eva] tests/syntax/Refresh_visitor.i:23: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:24: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:29: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:30: loop invariant got status valid.
[eva] tests/syntax/Refresh_visitor.i:32: starting to merge loop iterations
[eva] tests/syntax/Refresh_visitor.i:26: starting to merge loop iterations
[eva:alarm] tests/syntax/Refresh_visitor.i:14: Warning:
function main: postcondition got status unknown.
[eva] Recording results for main
[eva] done for function main
/* Generated by Frama-C */
struct S {
int i ;
};
struct matrix {
int m[100] ;
};
/*@ lemma foo: ∀ struct S x; x.i ≥ 0 ∨ x.i < 0;
*/
/*@ ensures \result ≥ \old(x.i); */
int main(struct S x, struct matrix m)
{
struct matrix m_t;
int y = x.i;
/*@ assert y ≡ x.i; */ ;
int i = 0;
int j = 0;
i = 0;
/*@ loop invariant 0 ≤ i ≤ 2;
loop invariant 0 ≤ j ≤ 2;
loop assigns i, j, m_t;
*/
while (i < 2) {
j = 0;
/*@ loop invariant 0 ≤ j ≤ 2;
loop invariant 0 ≤ i < 2;
loop assigns j, m_t;
*/
while (j < 2) {
m_t.m[i * 2 + j] = m.m[j * 2 + i];
j ++;
}
i ++;
}
return y;
}