Skip to content
Snippets Groups Projects
Commit b435c0ea authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] refactor scope

parent 0c9f1377
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 130 additions and 141 deletions
src/plugins/wp/calculus.ml
+ 4
− 6
View file @ b435c0ea
......@@ -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...
......
src/plugins/wp/cfgDump.ml
+ 2
− 3
View file @ b435c0ea
......@@ -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
......
src/plugins/wp/cfgWP.ml
+ 4
− 5
View file @ b435c0ea
......@@ -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 ->
......
src/plugins/wp/mcfg.ml
+ 2
− 3
View file @ b435c0ea
......@@ -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
......
src/plugins/wp/tests/wp_hoare/oracle/dispatch_var2.0.res.oracle
+ 7
− 7
View file @ b435c0ea
......@@ -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).
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot
+ 46
− 48
View file @ b435c0ea
......@@ -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 ;
}
src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
+ 40
− 42
View file @ b435c0ea
......@@ -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 ;
}
src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot
+ 25
− 27
View file @ b435c0ea
......@@ -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 ;
}
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