Commit 60d2031a authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] preparing new oracles for config 'prove'

parent d496fa37
......@@ -91,8 +91,10 @@ let extend () =
Wp.Wp_parameters.Share.set (InternalWpShare.get());
Wp.Wp_parameters.Verbose.set 0;
Globals.Functions.iter check_auto_func;
Report.Register.print ();
end else begin
File.pretty_ast ();
end;
File.pretty_ast ();
ok:=true (* no error, we can erase the file *)
in
Db.Toplevel.run := myrun
......
[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns0.i (no preprocessing)
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] [Qed] Goal typed_f_post_func_assign_part02 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part01 : Valid
[wp] [Qed] Goal typed_f_post_func_post_2 : Valid
[wp] [Qed] Goal typed_f_post_func_post : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part06 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part05 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part04 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part03 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part10 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part09 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part08 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part07 : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_S2_out_post : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_S1_out_post : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part12 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part11 : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_in_main_out_post : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_in_main_in_post : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_Sf_out_post : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_S_in_f_out_post : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part02 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part01 : Valid
[wp] [Qed] Goal typed_f_pre_func_post_2 : Valid
[wp] [Qed] Goal typed_f_pre_func_post : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part06 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part05 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part04 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part03 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part10 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part09 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part08 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part07 : Valid
[wp] [Qed] Goal typed_f_pre_func_buch_state_S_in_f_in_post : Valid
[wp] [Qed] Goal typed_f_pre_func_buch_state_S2_out_post : Valid
[wp] [Qed] Goal typed_f_pre_func_buch_state_S1_out_post : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part11 : Valid
[wp] [Qed] Goal typed_f_pre_func_buch_state_in_main_out_post : Valid
[wp] [Qed] Goal typed_f_pre_func_buch_state_Sf_out_post : Valid
[wp] [Qed] Goal typed_f_pre_func_buch_state_S_in_f_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part02 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part01 : Valid
[wp] [Qed] Goal typed_main_post_func_post_2 : Valid
[wp] [Qed] Goal typed_main_post_func_post : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part06 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part05 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part04 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part03 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part10 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part09 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part08 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part07 : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_S2_in_post : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_S1_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part12 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part11 : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_in_main_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_Sf_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_S_in_f_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_S2_out_post : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part02 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part01 : Valid
[wp] [Qed] Goal typed_main_pre_func_post_2 : Valid
[wp] [Qed] Goal typed_main_pre_func_post : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part06 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part05 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part04 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part03 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part10 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part09 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part08 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part07 : Valid
[wp] [Qed] Goal typed_main_pre_func_buch_state_S_in_f_out_post : Valid
[wp] [Qed] Goal typed_main_pre_func_buch_state_S2_out_post : Valid
[wp] [Qed] Goal typed_main_pre_func_buch_state_S1_out_post : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part11 : Valid
[wp] [Qed] Goal typed_main_pre_func_buch_state_in_main_out_post : Valid
[wp] [Qed] Goal typed_main_pre_func_buch_state_Sf_out_post : Valid
[wp] [Qed] Goal typed_main_pre_func_buch_state_Sf_in_post : Valid
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 1,
op_main = 0
};
enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
int X;
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@ ghost int S1 = 1; */
/*@ ghost int S2 = 0; */
/*@ ghost int S_in_f = 0; */
/*@ ghost int Sf = 0; */
/*@ ghost int in_main = 0; */
/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
behavior buch_state_S2_out:
ensures 0 ≡ S2;
behavior buch_state_S_in_f_in:
assumes 1 ≡ Sf;
ensures 1 ≡ S_in_f;
behavior buch_state_S_in_f_out:
assumes 0 ≡ Sf;
ensures 0 ≡ S_in_f;
behavior buch_state_Sf_out:
ensures 0 ≡ Sf;
behavior buch_state_in_main_out:
ensures 0 ≡ in_main;
*/
void f_pre_func(void)
{
/*@ ghost int S1_tmp; */
/*@ ghost int S2_tmp; */
/*@ ghost int S_in_f_tmp; */
/*@ ghost int Sf_tmp; */
/*@ ghost int in_main_tmp; */
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
S1_tmp = S1;
S2_tmp = S2;
S_in_f_tmp = S_in_f;
Sf_tmp = Sf;
in_main_tmp = in_main;
in_main_tmp = 0;
Sf_tmp = 0;
if (Sf == 1) S_in_f_tmp = 1; else S_in_f_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
S_in_f = S_in_f_tmp;
Sf = Sf_tmp;
in_main = in_main_tmp;
return;
}
[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
/*@ requires
1 ≡ S_in_f ∧ 0 ≡ S1 ∧ 0 ≡ S2 ∧ 0 ≡ Sf ∧ 0 ≡ in_main;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
behavior buch_state_S2_out:
ensures 0 ≡ S2;
behavior buch_state_S_in_f_out:
ensures 0 ≡ S_in_f;
behavior buch_state_Sf_out:
ensures 0 ≡ Sf;
behavior buch_state_in_main_in:
assumes 1 ≡ S_in_f;
ensures 1 ≡ in_main;
behavior buch_state_in_main_out:
assumes 0 ≡ S_in_f;
ensures 0 ≡ in_main;
*/
void f_post_func(void)
{
/*@ ghost int S1_tmp; */
/*@ ghost int S2_tmp; */
/*@ ghost int S_in_f_tmp; */
/*@ ghost int Sf_tmp; */
/*@ ghost int in_main_tmp; */
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
S1_tmp = S1;
S2_tmp = S2;
S_in_f_tmp = S_in_f;
Sf_tmp = Sf;
in_main_tmp = in_main;
if (S_in_f == 1) in_main_tmp = 1; else in_main_tmp = 0;
Sf_tmp = 0;
S_in_f_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
S_in_f = S_in_f_tmp;
Sf = Sf_tmp;
in_main = in_main_tmp;
return;
}
--------------------------------------------------------------------------------
--- Properties of Function 'f_pre_func'
--------------------------------------------------------------------------------
/*@ requires
1 ≡ Sf ∧ 0 ≡ S1 ∧ 0 ≡ S2 ∧ 0 ≡ S_in_f ∧ 0 ≡ in_main;
behavior Buchi_property_behavior:
ensures 0 ≡ S1 ∧ 0 ≡ S2 ∧ 0 ≡ S_in_f ∧ 0 ≡ Sf;
ensures 1 ≡ in_main;
*/
void f(void)
{
f_pre_func();
X ++;
f_post_func();
return;
}
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 35)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 36)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 41)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 44)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_in' (file /tmp/aorai_assigns_0.i, line 48)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 52)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 55)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 58)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 37)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S1_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S2_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_in_f_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_in_f_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_Sf_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_in_main_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
behavior buch_state_S2_out:
ensures 0 ≡ S2;
behavior buch_state_S_in_f_out:
ensures 0 ≡ S_in_f;
behavior buch_state_Sf_in:
assumes 1 ≡ S1;
ensures 1 ≡ Sf;
behavior buch_state_Sf_out:
assumes 0 ≡ S1;
ensures 0 ≡ Sf;
behavior buch_state_in_main_out:
ensures 0 ≡ in_main;
*/
void main_pre_func(void)
{
/*@ ghost int S1_tmp; */
/*@ ghost int S2_tmp; */
/*@ ghost int S_in_f_tmp; */
/*@ ghost int Sf_tmp; */
/*@ ghost int in_main_tmp; */
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
S1_tmp = S1;
S2_tmp = S2;
S_in_f_tmp = S_in_f;
Sf_tmp = Sf;
in_main_tmp = in_main;
in_main_tmp = 0;
if (S1 == 1) Sf_tmp = 1; else Sf_tmp = 0;
S_in_f_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
S_in_f = S_in_f_tmp;
Sf = Sf_tmp;
in_main = in_main_tmp;
return;
}
--------------------------------------------------------------------------------
--- Properties of Function 'f_post_func'
--------------------------------------------------------------------------------
/*@ requires
1 ≡ in_main ∧ 0 ≡ S1 ∧ 0 ≡ S2 ∧ 0 ≡ S_in_f ∧ 0 ≡ Sf;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
behavior buch_state_S1_out:
ensures 0 ≡ S1;
behavior buch_state_S2_in:
assumes 1 ≡ in_main;
ensures 1 ≡ S2;
behavior buch_state_S2_out:
assumes 0 ≡ in_main;
ensures 0 ≡ S2;
behavior buch_state_S_in_f_out:
ensures 0 ≡ S_in_f;
behavior buch_state_Sf_out:
ensures 0 ≡ Sf;
behavior buch_state_in_main_out:
ensures 0 ≡ in_main;
*/
void main_post_func(int res)
{
/*@ ghost int S1_tmp; */
/*@ ghost int S2_tmp; */
/*@ ghost int S_in_f_tmp; */
/*@ ghost int Sf_tmp; */
/*@ ghost int in_main_tmp; */
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
S1_tmp = S1;
S2_tmp = S2;
S_in_f_tmp = S_in_f;
Sf_tmp = Sf;
in_main_tmp = in_main;
in_main_tmp = 0;
Sf_tmp = 0;
S_in_f_tmp = 0;
if (in_main == 1) S2_tmp = 1; else S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
S_in_f = S_in_f_tmp;
Sf = Sf_tmp;
in_main = in_main_tmp;
return;
}
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 92)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 93)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 98)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 101)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 104)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 107)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_in' (file /tmp/aorai_assigns_0.i, line 111)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 115)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 94)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S1_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S2_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_in_f_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_Sf_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_in_main_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_in_main_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
/*@ requires
1 ≡ S1 ∧ 0 ≡ S2 ∧ 0 ≡ S_in_f ∧ 0 ≡ Sf ∧ 0 ≡ in_main;
assigns X, aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
behavior foo:
assigns X, aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main;
behavior Buchi_property_behavior:
ensures 0 ≡ S1 ∧ 0 ≡ S_in_f ∧ 0 ≡ Sf ∧ 0 ≡ in_main;
ensures 1 ≡ S2;
*/
int main(void)
{
main_pre_func();
/*@ assigns X; */
X ++;
/*@ assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
in_main, X;
*/
f();
main_post_func(X);
return X;
}
--------------------------------------------------------------------------------
--- Properties of Function 'f'
--------------------------------------------------------------------------------
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 162)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 163)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 168)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 171)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 174)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_in' (file /tmp/aorai_assigns_0.i, line 178)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 182)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 185)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 164)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S1_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S2_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_in_f_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_Sf_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_Sf_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_in_main_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main_post_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 219)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 220)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 225)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_in' (file /tmp/aorai_assigns_0.i, line 229)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 233)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 236)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 239)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 242)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 221)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S1_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S2_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S2_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_in_f_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_Sf_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_in_main_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
65 Completely validated
65 Total
--------------------------------------------------------------------------------
[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns1.i (no preprocessing)
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] [Qed] Goal typed_f_post_func_assign_part2 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part1 : Valid
[wp] [Qed] Goal typed_f_post_func_post_2 : Valid
[wp] [Qed] Goal typed_f_post_func_post : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_S2_out_post : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_S1_out_post : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part4 : Valid
[wp] [Qed] Goal typed_f_post_func_assign_part3 : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_in_main_out_post : Valid
[wp] [Qed] Goal typed_f_post_func_buch_state_Sf_out_post : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part2 : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part1 : Valid
[wp] [Qed] Goal typed_f_pre_func_post_2 : Valid
[wp] [Qed] Goal typed_f_pre_func_post : Valid
[wp] [Qed] Goal typed_f_pre_func_assign_part3 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part2 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part1 : Valid
[wp] [Qed] Goal typed_main_post_func_post_2 : Valid
[wp] [Qed] Goal typed_main_post_func_post : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_S1_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part4 : Valid
[wp] [Qed] Goal typed_main_post_func_assign_part3 : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_Sf_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_S_in_f_out_post : Valid
[wp] [Qed] Goal typed_main_post_func_buch_state_S2_out_post : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part2 : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part1 : Valid
[wp] [Qed] Goal typed_main_pre_func_post_2 : Valid
[wp] [Qed] Goal typed_main_pre_func_post : Valid
[wp] [Qed] Goal typed_main_pre_func_assign_part3 : Valid
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
S1 = 0,
S2 = 1,
S_in_f = 2,
Sf = 3,
in_main = 4
};
enum aorai_ListOper {
op_f = 1,
op_main = 0
};
enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
/*@ lemma in_main_deterministic_trans{L}: \true;
*/
/*@ lemma Sf_deterministic_trans{L}: \true;
*/
/*@ lemma S_in_f_deterministic_trans{L}: \true;
*/
/*@ lemma S2_deterministic_trans{L}: \true;
*/
/*@ lemma S1_deterministic_trans{L}: \true;
*/
int X;
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@ ghost int aorai_CurStates = S1; */
/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_S1_out:
ensures aorai_CurStates ≢ S1;
behavior buch_state_S2_out:
ensures aorai_CurStates ≢ S2;
behavior buch_state_S_in_f_in:
assumes aorai_CurStates ≡ Sf;
ensures aorai_CurStates ≡ S_in_f;
behavior buch_state_S_in_f_out:
assumes aorai_CurStates ≢ Sf;
ensures aorai_CurStates ≢ S_in_f;
behavior buch_state_Sf_out:
ensures aorai_CurStates ≢ Sf;
behavior buch_state_in_main_out:
ensures aorai_CurStates ≢ in_main;
*/
void f_pre_func(void)