Commit 9fbc41f2 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

update oracles

parent dbcf9ef1
......@@ -275,8 +275,8 @@ int main(void)
/*@ ghost main_pre_func(); */
/*@ assigns X; */
X ++;
/*@ assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main, X;
/*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
*/
f();
/*@ ghost main_post_func(X); */
......
......@@ -213,7 +213,7 @@ int main(void)
/*@ ghost main_pre_func(); */
/*@ assigns X; */
X ++;
/*@ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, X; */
/*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; */
f();
/*@ ghost main_post_func(X); */
return X;
......
......@@ -9,9 +9,9 @@ int f(int z)
int y = 2;
/*@ assigns y; */
__asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
/*@ for b: assigns x, y; */
/*@ assigns x;
assigns x \from y; */
/*@ for b: assigns x, y; */
__asm__ ("mov %1, %0\n\t" : "=r" (x) : "r" (y));
/*@ assigns x, y;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment