-
Andre Maroneze authored
Some case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
Andre Maroneze authoredSome case studies (e.g. dyad) use some ugly casts from fd_set_t which lead to the analysis stopping too early. Changing the representation of fd_set_t should also help it better conform to the standard (since a fd_set_t should be able to hold FD_SETSIZE elements).
Refresh_visitor.res.oracle 1.59 KiB
[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;
}