Commit d17d0e43 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] much less verbose oracle for config 'prove'

parent 09e3f5ef
......@@ -52,7 +52,17 @@ let extend () =
let run = !Db.Toplevel.run in
fun f ->
let my_project = Project.create "Reparsing" in
let wp_compute_kf kf = Wp.VC.command (Wp.VC.generate_kf kf) in
let wp_compute_kf kf =
let vcs = Wp.VC.generate_kf kf in
Wp.VC.command vcs;
Bag.iter
(fun vc ->
if not (Wp.VC.is_proved vc) then
P.warning "Could not prove %a in automaton function %a"
Property.pretty (Wp.VC.get_property vc)
Kernel_function.pretty kf)
vcs
in
let check_auto_func kf =
let name = Kernel_function.get_name kf in
if Kernel_function.is_definition kf &&
......@@ -91,7 +101,6 @@ 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;
......
......@@ -2,166 +2,3 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'f_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 37)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 38)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 43)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 46)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_in' (file /tmp/aorai_assigns_0.i, line 50)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 54)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 57)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 60)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 39)
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.
--------------------------------------------------------------------------------
--- Properties of Function 'f_post_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 94)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 95)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 100)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 103)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 106)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 109)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_in' (file /tmp/aorai_assigns_0.i, line 113)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 117)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 96)
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.
--------------------------------------------------------------------------------
--- 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 166)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 167)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 172)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 175)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 178)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_in' (file /tmp/aorai_assigns_0.i, line 182)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 186)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 189)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 168)
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 223)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_0.i, line 224)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_0.i, line 229)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_in' (file /tmp/aorai_assigns_0.i, line 233)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_0.i, line 237)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_0.i, line 240)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_0.i, line 243)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_0.i, line 246)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_0.i, line 225)
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
--------------------------------------------------------------------------------
......@@ -2,166 +2,3 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'f_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_assigns_1.i, line 50)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_1.i, line 51)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_1.i, line 55)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_1.i, line 58)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_in' (file /tmp/aorai_assigns_1.i, line 62)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_1.i, line 66)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_1.i, line 69)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_1.i, line 72)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_1.i, line 52)
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.
--------------------------------------------------------------------------------
--- Properties of Function 'f_post_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_assigns_1.i, line 89)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_1.i, line 90)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_1.i, line 94)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_1.i, line 97)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_1.i, line 100)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_1.i, line 103)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_in' (file /tmp/aorai_assigns_1.i, line 107)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_1.i, line 111)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_1.i, line 91)
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.
--------------------------------------------------------------------------------
--- Properties of Function 'f'
--------------------------------------------------------------------------------
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_assigns_1.i, line 141)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_1.i, line 142)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_1.i, line 146)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_1.i, line 149)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_1.i, line 152)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_in' (file /tmp/aorai_assigns_1.i, line 156)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_1.i, line 160)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_1.i, line 163)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_1.i, line 143)
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_1.i, line 180)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_assigns_1.i, line 181)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S1_out' (file /tmp/aorai_assigns_1.i, line 185)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_in' (file /tmp/aorai_assigns_1.i, line 189)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S2_out' (file /tmp/aorai_assigns_1.i, line 193)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in_f_out' (file /tmp/aorai_assigns_1.i, line 196)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_Sf_out' (file /tmp/aorai_assigns_1.i, line 199)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_in_main_out' (file /tmp/aorai_assigns_1.i, line 202)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_assigns_1.i, line 182)
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
--------------------------------------------------------------------------------
......@@ -3,93 +3,3 @@
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'a_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 31)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 32)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_0.i, line 36)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_0.i, line 33)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'a_post_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 53)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 54)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_0.i, line 58)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_0.i, line 55)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'a'
--------------------------------------------------------------------------------
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 86)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 87)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_0.i, line 91)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_0.i, line 88)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main_post_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 108)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_0.i, line 109)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_0.i, line 113)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_0.i, line 110)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main'
--------------------------------------------------------------------------------
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
26 Completely validated
26 Total
--------------------------------------------------------------------------------
......@@ -2,181 +2,3 @@
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_bts1289_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
[report] Computing properties status...
--------------------------------------------------------------------------------
--- Properties of Function 'a_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 38)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 39)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_1.i, line 44)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_T_out' (file /tmp/aorai_bts1289_1.i, line 47)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_in' (file /tmp/aorai_bts1289_1.i, line 51)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_out' (file /tmp/aorai_bts1289_1.i, line 55)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_0_in' (file /tmp/aorai_bts1289_1.i, line 59)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_0_out' (file /tmp/aorai_bts1289_1.i, line 63)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_init_out' (file /tmp/aorai_bts1289_1.i, line 66)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_1.i, line 40)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_T_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_0_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_0_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_init_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'a_post_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 103)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 104)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in' (file /tmp/aorai_bts1289_1.i, line 110)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_1.i, line 114)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_T_in' (file /tmp/aorai_bts1289_1.i, line 118)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_T_out' (file /tmp/aorai_bts1289_1.i, line 122)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_out' (file /tmp/aorai_bts1289_1.i, line 125)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_0_out' (file /tmp/aorai_bts1289_1.i, line 128)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_init_out' (file /tmp/aorai_bts1289_1.i, line 131)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_1.i, line 105)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_T_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_T_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_0_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_init_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'a'
--------------------------------------------------------------------------------
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main_pre_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 206)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 207)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in' (file /tmp/aorai_bts1289_1.i, line 213)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_1.i, line 217)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_T_out' (file /tmp/aorai_bts1289_1.i, line 220)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_out' (file /tmp/aorai_bts1289_1.i, line 223)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_0_out' (file /tmp/aorai_bts1289_1.i, line 226)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_init_out' (file /tmp/aorai_bts1289_1.i, line 229)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_1.i, line 208)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_T_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_0_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_aorai_intermediate_state_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_init_out'
by Frama-C kernel.
[ Valid ] Default behavior
by Frama-C kernel.
--------------------------------------------------------------------------------
--- Properties of Function 'main_post_func'
--------------------------------------------------------------------------------
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 265)
by Wp.typed.
[ Valid ] Post-condition (file /tmp/aorai_bts1289_1.i, line 266)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_in' (file /tmp/aorai_bts1289_1.i, line 272)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_S_out' (file /tmp/aorai_bts1289_1.i, line 276)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_T_out' (file /tmp/aorai_bts1289_1.i, line 279)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_out' (file /tmp/aorai_bts1289_1.i, line 282)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_aorai_intermediate_state_0_out' (file /tmp/aorai_bts1289_1.i, line 285)
by Wp.typed.
[ Valid ] Post-condition for 'buch_state_init_out' (file /tmp/aorai_bts1289_1.i, line 288)
by Wp.typed.
[ Valid ] Assigns (file /tmp/aorai_bts1289_1.i, line 267)
by Wp.typed.
[ Valid ] Behavior 'buch_state_S_in'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_S_out'
by Frama-C kernel.
[ Valid ] Behavior 'buch_state_T_out'