diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml index b380551db5cb297379d100977a108ff8731e173a..da054bcaad82194f5901158523788b48b3572cd1 100644 --- a/src/plugins/wp/calculus.ml +++ b/src/plugins/wp/calculus.ml @@ -495,9 +495,8 @@ module Cfg (W : Mcfg.S) = struct | Mcfg.SC_Global -> "global" | Mcfg.SC_Block_in -> "block in" | Mcfg.SC_Block_out -> "block out" - | Mcfg.SC_Function_in -> "function in" - | Mcfg.SC_Function_frame -> "function frame" - | Mcfg.SC_Function_out -> "function out" ) + | Mcfg.SC_Frame_in -> "frame in" + | Mcfg.SC_Frame_out -> "frame out" ) (Pretty_utils.pp_list ~sep:", " Printer.pp_varinfo) vars; match scope with | Mcfg.(SC_Block_in | SC_Block_out) when vars = [] -> obj @@ -564,13 +563,12 @@ module Cfg (W : Mcfg.S) = struct Wp_error.unsupported "strange CFGs." | Cil2cfg.VfctIn -> let obj = get_only_succ env cfg v in - let obj = wp_scope wenv formals Mcfg.SC_Function_in obj in let obj = wp_scope wenv [] Mcfg.SC_Global obj in obj | Cil2cfg.VblkIn (Cil2cfg.Bfct, b) -> let obj = get_only_succ env cfg v in let obj = wp_scope wenv b.blocals Mcfg.SC_Block_in obj in - let obj = wp_scope wenv formals Mcfg.SC_Function_frame obj in + let obj = wp_scope wenv formals Mcfg.SC_Frame_in obj in obj | Cil2cfg.VblkOut (Cil2cfg.Bfct, b) -> let obj = get_only_succ env cfg v in @@ -604,7 +602,7 @@ module Cfg (W : Mcfg.S) = struct | Cil2cfg.VfctOut | Cil2cfg.Vexit -> let obj = get_only_succ env cfg v (* exitpost / postcondition *) in - wp_scope wenv formals Mcfg.SC_Function_out obj + wp_scope wenv formals Mcfg.SC_Frame_out obj | Cil2cfg.Vend -> W.empty (* LC : unused entry point... diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml index 5fbdbfb4a427e3d99779ef907b88f4f86a50cbc5..6091b24dc5af8716fc40177bdbc5c32f852adfd5 100644 --- a/src/plugins/wp/cfgDump.ml +++ b/src/plugins/wp/cfgDump.ml @@ -234,9 +234,8 @@ struct let pp_scope sc fmt xs = let title = match sc with | Mcfg.SC_Global -> "Global" - | Mcfg.SC_Function_in -> "F-in" - | Mcfg.SC_Function_frame -> "F-frame" - | Mcfg.SC_Function_out -> "F-out" + | Mcfg.SC_Frame_in -> "F-in" + | Mcfg.SC_Frame_out -> "F-out" | Mcfg.SC_Block_in -> "B-in" | Mcfg.SC_Block_out -> "B-out" in begin diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml index ddf5fcd5cd106baefc927cdf99524ba73d63bd54..35f5540f842c253bc5e1f90afbe41b4b7ef998d9 100644 --- a/src/plugins/wp/cfgWP.ml +++ b/src/plugins/wp/cfgWP.ml @@ -1203,11 +1203,10 @@ struct let hs = M.frame (L.current env) in let vcs = gmap (assume_vc ~descr:"Heap" ~domain:true hs) wp.vcs in { wp with vcs } - | Mcfg.SC_Function_in -> wp - | Mcfg.SC_Function_frame -> - wp_scope env wp ~descr:"Function Frame" Enter xs - | Mcfg.SC_Function_out -> - wp_scope env wp ~descr:"Function Exit" Leave xs + | Mcfg.SC_Frame_in -> + wp_scope env wp ~descr:"Frame In" Enter xs + | Mcfg.SC_Frame_out -> + wp_scope env wp ~descr:"Frame Out" Leave xs | Mcfg.SC_Block_in -> wp_scope env wp ~descr:"Block In" Enter xs | Mcfg.SC_Block_out -> diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.ml index 1961d71cf9088927f26d864d29bde37787ada17e..873001be1ebceef7f7c3212b4b449f6f02319a6d 100644 --- a/src/plugins/wp/mcfg.ml +++ b/src/plugins/wp/mcfg.ml @@ -24,9 +24,8 @@ open Cil_types type scope = | SC_Global - | SC_Function_in (* Just before the pre-state *) - | SC_Function_frame (* Just after the introduction of formals *) - | SC_Function_out (* Post-state *) + | SC_Frame_in + | SC_Frame_out | SC_Block_in | SC_Block_out diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle index 72989020ecec9747960fbc528524a8b097623523..38bac71fd69ff2c3cd3c95e63c9b1d4086154818 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle @@ -208,7 +208,7 @@ Assume { Have: (ta_y_0=true). (* Pre-condition *) Have: (ta_y_0=true). - (* Function Frame *) + (* Frame In *) Have: (ta_y_1=true) /\ (ta_y_0=false). (* Block In *) Have: (Init_tmp_0=false) /\ (ta_tmp_0=false). @@ -222,7 +222,7 @@ Assume { Have: ((Init_tmp_0=true) -> (Init_tmp_1=true)). (* Return *) Have: tmp_0 = call_param_0. - (* Function Exit *) + (* Frame Out *) Have: (ta_y_3=true). } Prove: call_param_0 = 0. @@ -243,7 +243,7 @@ Assume { Have: (ta_y_1=true). (* Pre-condition *) Have: (ta_y_1=true). - (* Function Frame *) + (* Frame In *) Have: (ta_y_2=true) /\ (ta_y_1=false). (* Block In *) Have: (ta_tmp_0=false). @@ -271,7 +271,7 @@ Assume { Have: (ta_y_1=true). (* Pre-condition *) Have: (ta_y_1=true). - (* Function Frame *) + (* Frame In *) Have: (ta_y_2=true) /\ (ta_y_1=false). (* Block In *) Have: (ta_tmp_0=false). @@ -291,7 +291,7 @@ Assume { Have: (ta_y_0=true). (* Pre-condition *) Have: (ta_y_0=true). - (* Function Frame *) + (* Frame In *) Have: (ta_y_1=true) /\ (ta_y_0=false). (* Block In *) Have: (Init_tmp_0=false) /\ (ta_tmp_1=false). @@ -314,7 +314,7 @@ Assume { Have: (ta_y_1=true). (* Pre-condition *) Have: (ta_y_1=true). - (* Function Frame *) + (* Frame In *) Have: (ta_y_0=true) /\ (ta_y_1=false). (* Block In *) Have: (ta_tmp_0=false). @@ -331,7 +331,7 @@ Assume { Have: (ta_y_1=true). (* Pre-condition *) Have: (ta_y_1=true). - (* Function Frame *) + (* Frame In *) Have: (ta_y_2=true) /\ (ta_y_1=false). (* Block In *) Have: (ta_tmp_0=false). diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot index 077cfed3a2e1434664df16c14606fadf8d9e4e0c..c480b21b82a420b250b7d4038e3d096670e938ee 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot @@ -2,73 +2,71 @@ digraph f { rankdir = TB ; node [ style = filled, shape = box ] ; N000 [ color = red, shape = circle, label = "*" ] ; - N056 [ color=red , label="Prove f_ensures" ] ; - N056 -> N000 [ style=dotted ] ; - N057 [ color=red , label="Prove f_ensures_2" ] ; - N057 -> N056 [ style=dotted ] ; - N058 [ label="" , shape=circle ] ; + N054 [ color=red , label="Prove f_ensures" ] ; + N054 -> N000 [ style=dotted ] ; + N055 [ color=red , label="Prove f_ensures_2" ] ; + N055 -> N054 [ style=dotted ] ; + N056 [ label="" , shape=circle ] ; + N056 -> N055 ; + N056 -> N054 ; + N057 [ color=lightblue , label="F-out { a b }" ] ; + N057 -> N056 ; + N058 [ label="Label wp:post" ] ; N058 -> N057 ; - N058 -> N056 ; - N059 [ color=lightblue , label="F-out { a b }" ] ; + N059 [ color=lightblue , label="B-out { __retres }" ] ; N059 -> N058 ; - N060 [ label="Label wp:post" ] ; + N060 [ color=orange , label="Return __retres" ] ; N060 -> N059 ; - N061 [ color=lightblue , label="B-out { __retres }" ] ; + N061 [ label="Label wp:sid27 (Stmt s27)" ] ; N061 -> N060 ; - N062 [ color=orange , label="Return __retres" ] ; + N062 [ label="Label wp:sid26 (Stmt s26)" ] ; N062 -> N061 ; - N063 [ label="Label wp:sid27 (Stmt s27)" ] ; + N063 [ color=green , label="Assume f_assert" ] ; N063 -> N062 ; - N064 [ label="Label wp:sid26 (Stmt s26)" ] ; - N064 -> N063 ; - N065 [ color=green , label="Assume f_assert" ] ; + N064 [ color=red , label="Prove f_assert" ] ; + N064 -> N063 [ style=dotted ] ; + N065 [ label="" , shape=circle ] ; N065 -> N064 ; - N066 [ color=red , label="Prove f_assert" ] ; - N066 -> N065 [ style=dotted ] ; - N067 [ label="" , shape=circle ] ; + N065 -> N063 ; + N066 [ label="Label wp:sid25 (Stmt s25)" ] ; + N066 -> N065 ; + N067 [ color=orange , label="__retres := a + b" ] ; N067 -> N066 ; - N067 -> N065 ; - N068 [ label="Label wp:sid25 (Stmt s25)" ] ; + N068 [ label="Label wp:sid6 (Stmt s6)" ] ; N068 -> N067 ; - N069 [ color=orange , label="__retres := a + b" ] ; + N069 [ label="Label wp:sid24 (Stmt s24)" ] ; N069 -> N068 ; - N070 [ label="Label wp:sid6 (Stmt s6)" ] ; - N070 -> N069 ; - N071 [ label="Label wp:sid24 (Stmt s24)" ] ; + N070 [ color=orange , label="Return __retres" ] ; + N070 -> N059 ; + N071 [ label="Label wp:sid27 (Stmt s27)" ] ; N071 -> N070 ; - N072 [ color=orange , label="Return __retres" ] ; - N072 -> N061 ; - N073 [ label="Label wp:sid27 (Stmt s27)" ] ; + N072 [ color=orange , label="__retres := -1" ] ; + N072 -> N071 ; + N073 [ label="Label wp:sid8 (Stmt s8)" ] ; N073 -> N072 ; - N074 [ color=orange , label="__retres := -1" ] ; + N074 [ color=green , label="Assume f_ensures_3" ] ; N074 -> N073 ; - N075 [ label="Label wp:sid8 (Stmt s8)" ] ; - N075 -> N074 ; - N076 [ color=green , label="Assume f_ensures_3" ] ; - N076 -> N075 ; - N077 [ color=orange , label="Havoc f_assigns: + N075 [ color=orange , label="Havoc f_assigns: assigns __retres;" ] ; + N075 -> N074 ; + N076 [ color=cyan , label="If a > 0" ] ; + N076 -> N069 ; + N076 -> N000 [ style=dotted ]; + N077 [ label="Label wp:sid4 (Stmt s4)" ] ; N077 -> N076 ; - N078 [ color=cyan , label="If a > 0" ] ; - N078 -> N071 ; - N078 -> N000 [ style=dotted ]; - N079 [ label="Label wp:sid4 (Stmt s4)" ] ; + N078 [ label="" , shape=circle ] ; + N078 -> N075 ; + N078 -> N077 ; + N079 [ label="Label wp:sid2 (Stmt s2)" ] ; N079 -> N078 ; - N080 [ label="" , shape=circle ] ; - N080 -> N077 ; + N080 [ color=lightblue , label="B-in { __retres }" ] ; N080 -> N079 ; - N081 [ label="Label wp:sid2 (Stmt s2)" ] ; + N081 [ color=lightblue , label="F-in { a b }" ] ; N081 -> N080 ; - N082 [ color=lightblue , label="B-in { __retres }" ] ; + N082 [ label="Label wp:pre" ] ; N082 -> N081 ; - N083 [ color=lightblue , label="F-frame { a b }" ] ; + N083 [ color=lightblue , label="Global { }" ] ; N083 -> N082 ; - N084 [ label="Label wp:pre" ] ; + N084 [ color=cyan , label="Function f" ] ; N084 -> N083 ; - N085 [ color=lightblue , label="F-in { a b }" ] ; - N085 -> N084 ; - N086 [ color=lightblue , label="Global { }" ] ; - N086 -> N085 ; - N087 [ color=cyan , label="Function f" ] ; - N087 -> N086 ; } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot index be3a8a3a5db7557308b6a855e36ed03b49a2a6ea..adc97b189dd30ed107c620cded36762ba14ef83f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot @@ -2,64 +2,62 @@ digraph f { rankdir = TB ; node [ style = filled, shape = box ] ; N000 [ color = red, shape = circle, label = "*" ] ; - N088 [ color=lightblue , label="F-out { a b }" ] ; - N088 -> N000 [ style=dotted ]; - N089 [ label="Label wp:post" ] ; + N085 [ color=lightblue , label="F-out { a b }" ] ; + N085 -> N000 [ style=dotted ]; + N086 [ label="Label wp:post" ] ; + N086 -> N085 ; + N087 [ color=lightblue , label="B-out { __retres }" ] ; + N087 -> N086 ; + N088 [ color=orange , label="Return __retres" ] ; + N088 -> N087 ; + N089 [ label="Label wp:sid27 (Stmt s27)" ] ; N089 -> N088 ; - N090 [ color=lightblue , label="B-out { __retres }" ] ; + N090 [ label="Label wp:sid26 (Stmt s26)" ] ; N090 -> N089 ; - N091 [ color=orange , label="Return __retres" ] ; + N091 [ color=green , label="Assume f_assert" ] ; N091 -> N090 ; - N092 [ label="Label wp:sid27 (Stmt s27)" ] ; + N092 [ label="Label wp:sid25 (Stmt s25)" ] ; N092 -> N091 ; - N093 [ label="Label wp:sid26 (Stmt s26)" ] ; + N093 [ color=orange , label="__retres := a + b" ] ; N093 -> N092 ; - N094 [ color=green , label="Assume f_assert" ] ; + N094 [ label="Label wp:sid6 (Stmt s6)" ] ; N094 -> N093 ; - N095 [ label="Label wp:sid25 (Stmt s25)" ] ; + N095 [ label="Label wp:sid24 (Stmt s24)" ] ; N095 -> N094 ; - N096 [ color=orange , label="__retres := a + b" ] ; - N096 -> N095 ; - N097 [ label="Label wp:sid6 (Stmt s6)" ] ; + N096 [ color=orange , label="Return __retres" ] ; + N096 -> N087 ; + N097 [ label="Label wp:sid27 (Stmt s27)" ] ; N097 -> N096 ; - N098 [ label="Label wp:sid24 (Stmt s24)" ] ; + N098 [ color=orange , label="__retres := -1" ] ; N098 -> N097 ; - N099 [ color=orange , label="Return __retres" ] ; - N099 -> N090 ; - N100 [ label="Label wp:sid27 (Stmt s27)" ] ; + N099 [ label="Label wp:sid8 (Stmt s8)" ] ; + N099 -> N098 ; + N100 [ color=green , label="Assume f_ensures_3" ] ; N100 -> N099 ; - N101 [ color=orange , label="__retres := -1" ] ; - N101 -> N100 ; - N102 [ label="Label wp:sid8 (Stmt s8)" ] ; + N101 [ color=red , label="Assigns f_assigns" ] ; + N102 [ label="" , shape=circle ] ; N102 -> N101 ; - N103 [ color=green , label="Assume f_ensures_3" ] ; - N103 -> N102 ; - N104 [ color=red , label="Assigns f_assigns" ] ; - N105 [ label="" , shape=circle ] ; + N102 -> N100 ; + N103 [ color=red , label="Prove f_ensures_3" ] ; + N103 -> N102 [ style=dotted ] ; + N104 [ label="" , shape=circle ] ; + N104 -> N103 ; + N104 -> N102 ; + N105 [ color=cyan , label="If a > 0" ] ; + N105 -> N095 ; N105 -> N104 ; - N105 -> N103 ; - N106 [ color=red , label="Prove f_ensures_3" ] ; - N106 -> N105 [ style=dotted ] ; - N107 [ label="" , shape=circle ] ; + N106 [ label="Label wp:sid4 (Stmt s4)" ] ; + N106 -> N105 ; + N107 [ label="Label wp:sid2 (Stmt s2)" ] ; N107 -> N106 ; - N107 -> N105 ; - N108 [ color=cyan , label="If a > 0" ] ; - N108 -> N098 ; + N108 [ color=lightblue , label="B-in { __retres }" ] ; N108 -> N107 ; - N109 [ label="Label wp:sid4 (Stmt s4)" ] ; + N109 [ color=lightblue , label="F-in { a b }" ] ; N109 -> N108 ; - N110 [ label="Label wp:sid2 (Stmt s2)" ] ; + N110 [ label="Label wp:pre" ] ; N110 -> N109 ; - N111 [ color=lightblue , label="B-in { __retres }" ] ; + N111 [ color=lightblue , label="Global { }" ] ; N111 -> N110 ; - N112 [ color=lightblue , label="F-frame { a b }" ] ; + N112 [ color=cyan , label="Function f" ] ; N112 -> N111 ; - N113 [ label="Label wp:pre" ] ; - N113 -> N112 ; - N114 [ color=lightblue , label="F-in { a b }" ] ; - N114 -> N113 ; - N115 [ color=lightblue , label="Global { }" ] ; - N115 -> N114 ; - N116 [ color=cyan , label="Function f" ] ; - N116 -> N115 ; } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot index 4fffdb8fb16edd8f2e3eb57b430c493b7f3da9f4..90e91e8e87a4a2f5abc71d260f9fcf9dbdb53fbf 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot @@ -2,47 +2,45 @@ digraph g { rankdir = TB ; node [ style = filled, shape = box ] ; N000 [ color = red, shape = circle, label = "*" ] ; - N035 [ color=red , label="Prove g_ensures_2" ] ; - N035 -> N000 [ style=dotted ] ; - N036 [ color=lightblue , label="F-out { a b }" ] ; + N034 [ color=red , label="Prove g_ensures_2" ] ; + N034 -> N000 [ style=dotted ] ; + N035 [ color=lightblue , label="F-out { a b }" ] ; + N035 -> N034 ; + N036 [ label="Label wp:post" ] ; N036 -> N035 ; - N037 [ label="Label wp:post" ] ; + N037 [ color=lightblue , label="B-out { __retres }" ] ; N037 -> N036 ; - N038 [ color=lightblue , label="B-out { __retres }" ] ; + N038 [ color=orange , label="Return __retres" ] ; N038 -> N037 ; - N039 [ color=orange , label="Return __retres" ] ; + N039 [ label="Label wp:sid32 (Stmt s32)" ] ; N039 -> N038 ; - N040 [ label="Label wp:sid32 (Stmt s32)" ] ; + N040 [ label="Label wp:sid31 (Stmt s31)" ] ; N040 -> N039 ; - N041 [ label="Label wp:sid31 (Stmt s31)" ] ; + N041 [ color=green , label="Assume g_assert" ] ; N041 -> N040 ; - N042 [ color=green , label="Assume g_assert" ] ; - N042 -> N041 ; - N043 [ color=red , label="Prove g_assert" ] ; - N043 -> N042 [ style=dotted ] ; - N044 [ label="" , shape=circle ] ; + N042 [ color=red , label="Prove g_assert" ] ; + N042 -> N041 [ style=dotted ] ; + N043 [ label="" , shape=circle ] ; + N043 -> N042 ; + N043 -> N041 ; + N044 [ label="Label wp:sid30 (Stmt s30)" ] ; N044 -> N043 ; - N044 -> N042 ; - N045 [ label="Label wp:sid30 (Stmt s30)" ] ; + N045 [ color=orange , label="__retres := a + b" ] ; N045 -> N044 ; - N046 [ color=orange , label="__retres := a + b" ] ; + N046 [ label="Label wp:sid13 (Stmt s13)" ] ; N046 -> N045 ; - N047 [ label="Label wp:sid13 (Stmt s13)" ] ; + N047 [ label="Label wp:sid29 (Stmt s29)" ] ; N047 -> N046 ; - N048 [ label="Label wp:sid29 (Stmt s29)" ] ; + N048 [ label="Label wp:sid11 (Stmt s11)" ] ; N048 -> N047 ; - N049 [ label="Label wp:sid11 (Stmt s11)" ] ; + N049 [ color=lightblue , label="B-in { __retres }" ] ; N049 -> N048 ; - N050 [ color=lightblue , label="B-in { __retres }" ] ; + N050 [ color=lightblue , label="F-in { a b }" ] ; N050 -> N049 ; - N051 [ color=lightblue , label="F-frame { a b }" ] ; + N051 [ label="Label wp:pre" ] ; N051 -> N050 ; - N052 [ label="Label wp:pre" ] ; + N052 [ color=lightblue , label="Global { }" ] ; N052 -> N051 ; - N053 [ color=lightblue , label="F-in { a b }" ] ; + N053 [ color=cyan , label="Function g" ] ; N053 -> N052 ; - N054 [ color=lightblue , label="Global { }" ] ; - N054 -> N053 ; - N055 [ color=cyan , label="Function g" ] ; - N055 -> N054 ; }