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

[wp] optimise block in/out

parent 16c65085
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/calculus.ml
+ 3
− 2
View file @ 3f344200
......@@ -494,8 +494,9 @@ module Cfg (W : Mcfg.S) = struct
| Mcfg.SC_Function_frame -> "function frame"
| Mcfg.SC_Function_out -> "function out" )
(Pretty_utils.pp_list ~sep:", " Printer.pp_varinfo) vars;
W.scope wenv vars scope obj
match scope with
| Mcfg.(SC_Block_in | SC_Block_out) when vars = [] -> obj
| _ -> W.scope wenv vars scope obj
(** @return the WP stored for edge [e]. Compute it if it is not already
* there and store it. Also handle the Acut annotations. *)
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot
+ 59
− 75
View file @ 3f344200
......@@ -2,89 +2,73 @@ digraph f {
rankdir = TB ;
node [ style = filled, shape = box ] ;
N000 [ color = red, shape = circle, label = "*" ] ;
N074 [ color=red , label="Prove f_ensures" ] ;
N074 -> N000 [ style=dotted ] ;
N075 [ color=red , label="Prove f_ensures_2" ] ;
N075 -> N074 [ style=dotted ] ;
N076 [ label="" , shape=circle ] ;
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 ] ;
N058 -> N057 ;
N058 -> N056 ;
N059 [ color=lightblue , label="F-out { a b }" ] ;
N059 -> N058 ;
N060 [ label="Label wp:post" ] ;
N060 -> N059 ;
N061 [ color=lightblue , label="B-out { __retres }" ] ;
N061 -> N060 ;
N062 [ color=orange , label="Return __retres" ] ;
N062 -> N061 ;
N063 [ label="Label wp:sid27 (Stmt s27)" ] ;
N063 -> N062 ;
N064 [ label="Label wp:sid26 (Stmt s26)" ] ;
N064 -> N063 ;
N065 [ color=green , label="Assume f_assert" ] ;
N065 -> N064 ;
N066 [ color=red , label="Prove f_assert" ] ;
N066 -> N065 [ style=dotted ] ;
N067 [ label="" , shape=circle ] ;
N067 -> N066 ;
N067 -> N065 ;
N068 [ label="Label wp:sid25 (Stmt s25)" ] ;
N068 -> N067 ;
N069 [ color=orange , label="__retres := a + b" ] ;
N069 -> N068 ;
N070 [ label="Label wp:sid6 (Stmt s6)" ] ;
N070 -> N069 ;
N071 [ label="Label wp:sid24 (Stmt s24)" ] ;
N071 -> N070 ;
N072 [ color=orange , label="Return __retres" ] ;
N072 -> N061 ;
N073 [ label="Label wp:sid27 (Stmt s27)" ] ;
N073 -> N072 ;
N074 [ color=orange , label="__retres := -1" ] ;
N074 -> N073 ;
N075 [ label="Label wp:sid8 (Stmt s8)" ] ;
N075 -> N074 ;
N076 [ color=green , label="Assume f_ensures_3" ] ;
N076 -> N075 ;
N076 -> N074 ;
N077 [ color=lightblue , label="F-out { a b }" ] ;
N077 [ color=orange , label="Havoc f_assigns:
assigns __retres;" ] ;
N077 -> N076 ;
N078 [ label="Label wp:post" ] ;
N078 -> N077 ;
N079 [ color=lightblue , label="B-out { __retres }" ] ;
N078 [ color=cyan , label="If a > 0" ] ;
N078 -> N071 ;
N078 -> N000 [ style=dotted ];
N079 [ label="Label wp:sid4 (Stmt s4)" ] ;
N079 -> N078 ;
N080 [ color=orange , label="Return __retres" ] ;
N080 [ label="" , shape=circle ] ;
N080 -> N077 ;
N080 -> N079 ;
N081 [ color=lightblue , label="B-out { }" ] ;
N081 [ label="Label wp:sid2 (Stmt s2)" ] ;
N081 -> N080 ;
N082 [ color=lightblue , label="B-out { }" ] ;
N082 [ color=lightblue , label="B-in { __retres }" ] ;
N082 -> N081 ;
N083 [ color=lightblue , label="B-out { }" ] ;
N083 [ color=lightblue , label="F-frame { a b }" ] ;
N083 -> N082 ;
N084 [ label="Label wp:sid27 (Stmt s27)" ] ;
N084 [ label="Label wp:pre" ] ;
N084 -> N083 ;
N085 [ label="Label wp:sid26 (Stmt s26)" ] ;
N085 [ color=lightblue , label="F-in { a b }" ] ;
N085 -> N084 ;
N086 [ color=green , label="Assume f_assert" ] ;
N086 [ color=lightblue , label="Global { }" ] ;
N086 -> N085 ;
N087 [ color=red , label="Prove f_assert" ] ;
N087 -> N086 [ style=dotted ] ;
N088 [ label="" , shape=circle ] ;
N088 -> N087 ;
N088 -> N086 ;
N089 [ label="Label wp:sid25 (Stmt s25)" ] ;
N089 -> N088 ;
N090 [ color=orange , label="__retres := a + b" ] ;
N090 -> N089 ;
N091 [ label="Label wp:sid6 (Stmt s6)" ] ;
N091 -> N090 ;
N092 [ color=lightblue , label="B-in { }" ] ;
N092 -> N091 ;
N093 [ label="Label wp:sid24 (Stmt s24)" ] ;
N093 -> N092 ;
N094 [ color=lightblue , label="B-in { }" ] ;
N094 -> N093 ;
N095 [ color=orange , label="Return __retres" ] ;
N095 -> N079 ;
N096 [ label="Label wp:sid27 (Stmt s27)" ] ;
N096 -> N095 ;
N097 [ color=orange , label="__retres := -1" ] ;
N097 -> N096 ;
N098 [ label="Label wp:sid8 (Stmt s8)" ] ;
N098 -> N097 ;
N099 [ color=green , label="Assume f_ensures_3" ] ;
N099 -> N098 ;
N100 [ color=orange , label="Havoc f_assigns:
assigns __retres;" ] ;
N100 -> N099 ;
N101 [ color=lightblue , label="B-in { }" ] ;
N101 -> N000 [ style=dotted ];
N102 [ color=lightblue , label="B-out { }" ] ;
N102 -> N101 ;
N103 [ color=cyan , label="If a > 0" ] ;
N103 -> N094 ;
N103 -> N102 ;
N104 [ label="Label wp:sid4 (Stmt s4)" ] ;
N104 -> N103 ;
N105 [ color=lightblue , label="B-in { }" ] ;
N105 -> N104 ;
N106 [ label="" , shape=circle ] ;
N106 -> N100 ;
N106 -> N105 ;
N107 [ label="Label wp:sid2 (Stmt s2)" ] ;
N107 -> N106 ;
N108 [ color=lightblue , label="B-in { __retres }" ] ;
N108 -> N107 ;
N109 [ color=lightblue , label="F-frame { a b }" ] ;
N109 -> N108 ;
N110 [ label="Label wp:pre" ] ;
N110 -> N109 ;
N111 [ color=lightblue , label="F-in { a b }" ] ;
N111 -> N110 ;
N112 [ color=lightblue , label="Global { }" ] ;
N112 -> N111 ;
N113 [ color=cyan , label="Function f" ] ;
N113 -> N112 ;
N087 [ color=cyan , label="Function f" ] ;
N087 -> N086 ;
}
src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
+ 58
− 74
View file @ 3f344200
......@@ -2,80 +2,64 @@ digraph f {
rankdir = TB ;
node [ style = filled, shape = box ] ;
N000 [ color = red, shape = circle, label = "*" ] ;
N114 [ color=lightblue , label="F-out { a b }" ] ;
N114 -> N000 [ style=dotted ];
N115 [ label="Label wp:post" ] ;
N088 [ color=lightblue , label="F-out { a b }" ] ;
N088 -> N000 [ style=dotted ];
N089 [ label="Label wp:post" ] ;
N089 -> N088 ;
N090 [ color=lightblue , label="B-out { __retres }" ] ;
N090 -> N089 ;
N091 [ color=orange , label="Return __retres" ] ;
N091 -> N090 ;
N092 [ label="Label wp:sid27 (Stmt s27)" ] ;
N092 -> N091 ;
N093 [ label="Label wp:sid26 (Stmt s26)" ] ;
N093 -> N092 ;
N094 [ color=green , label="Assume f_assert" ] ;
N094 -> N093 ;
N095 [ label="Label wp:sid25 (Stmt s25)" ] ;
N095 -> N094 ;
N096 [ color=orange , label="__retres := a + b" ] ;
N096 -> N095 ;
N097 [ label="Label wp:sid6 (Stmt s6)" ] ;
N097 -> N096 ;
N098 [ label="Label wp:sid24 (Stmt s24)" ] ;
N098 -> N097 ;
N099 [ color=orange , label="Return __retres" ] ;
N099 -> N090 ;
N100 [ label="Label wp:sid27 (Stmt s27)" ] ;
N100 -> N099 ;
N101 [ color=orange , label="__retres := -1" ] ;
N101 -> N100 ;
N102 [ label="Label wp:sid8 (Stmt s8)" ] ;
N102 -> N101 ;
N103 [ color=green , label="Assume f_ensures_3" ] ;
N103 -> N102 ;
N104 [ color=red , label="Assigns f_assigns" ] ;
N105 [ label="" , shape=circle ] ;
N105 -> N104 ;
N105 -> N103 ;
N106 [ color=red , label="Prove f_ensures_3" ] ;
N106 -> N105 [ style=dotted ] ;
N107 [ label="" , shape=circle ] ;
N107 -> N106 ;
N107 -> N105 ;
N108 [ color=cyan , label="If a > 0" ] ;
N108 -> N098 ;
N108 -> N107 ;
N109 [ label="Label wp:sid4 (Stmt s4)" ] ;
N109 -> N108 ;
N110 [ label="Label wp:sid2 (Stmt s2)" ] ;
N110 -> N109 ;
N111 [ color=lightblue , label="B-in { __retres }" ] ;
N111 -> N110 ;
N112 [ color=lightblue , label="F-frame { a b }" ] ;
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=lightblue , label="B-out { __retres }" ] ;
N116 [ color=cyan , label="Function f" ] ;
N116 -> N115 ;
N117 [ color=orange , label="Return __retres" ] ;
N117 -> N116 ;
N118 [ color=lightblue , label="B-out { }" ] ;
N118 -> N117 ;
N119 [ color=lightblue , label="B-out { }" ] ;
N119 -> N118 ;
N120 [ color=lightblue , label="B-out { }" ] ;
N120 -> N119 ;
N121 [ label="Label wp:sid27 (Stmt s27)" ] ;
N121 -> N120 ;
N122 [ label="Label wp:sid26 (Stmt s26)" ] ;
N122 -> N121 ;
N123 [ color=green , label="Assume f_assert" ] ;
N123 -> N122 ;
N124 [ label="Label wp:sid25 (Stmt s25)" ] ;
N124 -> N123 ;
N125 [ color=orange , label="__retres := a + b" ] ;
N125 -> N124 ;
N126 [ label="Label wp:sid6 (Stmt s6)" ] ;
N126 -> N125 ;
N127 [ color=lightblue , label="B-in { }" ] ;
N127 -> N126 ;
N128 [ label="Label wp:sid24 (Stmt s24)" ] ;
N128 -> N127 ;
N129 [ color=lightblue , label="B-in { }" ] ;
N129 -> N128 ;
N130 [ color=orange , label="Return __retres" ] ;
N130 -> N116 ;
N131 [ label="Label wp:sid27 (Stmt s27)" ] ;
N131 -> N130 ;
N132 [ color=orange , label="__retres := -1" ] ;
N132 -> N131 ;
N133 [ label="Label wp:sid8 (Stmt s8)" ] ;
N133 -> N132 ;
N134 [ color=green , label="Assume f_ensures_3" ] ;
N134 -> N133 ;
N135 [ color=red , label="Assigns f_assigns" ] ;
N136 [ label="" , shape=circle ] ;
N136 -> N135 ;
N136 -> N134 ;
N137 [ color=red , label="Prove f_ensures_3" ] ;
N137 -> N136 [ style=dotted ] ;
N138 [ label="" , shape=circle ] ;
N138 -> N137 ;
N138 -> N136 ;
N139 [ color=lightblue , label="B-in { }" ] ;
N139 -> N138 ;
N140 [ color=lightblue , label="B-out { }" ] ;
N140 -> N139 ;
N141 [ color=cyan , label="If a > 0" ] ;
N141 -> N129 ;
N141 -> N140 ;
N142 [ label="Label wp:sid4 (Stmt s4)" ] ;
N142 -> N141 ;
N143 [ color=lightblue , label="B-in { }" ] ;
N143 -> N142 ;
N144 [ label="Label wp:sid2 (Stmt s2)" ] ;
N144 -> N143 ;
N145 [ color=lightblue , label="B-in { __retres }" ] ;
N145 -> N144 ;
N146 [ color=lightblue , label="F-frame { a b }" ] ;
N146 -> N145 ;
N147 [ label="Label wp:pre" ] ;
N147 -> N146 ;
N148 [ color=lightblue , label="F-in { a b }" ] ;
N148 -> N147 ;
N149 [ color=lightblue , label="Global { }" ] ;
N149 -> N148 ;
N150 [ color=cyan , label="Function f" ] ;
N150 -> N149 ;
}
src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot
+ 37
− 45
View file @ 3f344200
......@@ -2,55 +2,47 @@ digraph g {
rankdir = TB ;
node [ style = filled, shape = box ] ;
N000 [ color = red, shape = circle, label = "*" ] ;
N049 [ color=red , label="Prove g_ensures_2" ] ;
N049 -> N000 [ style=dotted ] ;
N050 [ color=lightblue , label="F-out { a b }" ] ;
N035 [ color=red , label="Prove g_ensures_2" ] ;
N035 -> N000 [ style=dotted ] ;
N036 [ color=lightblue , label="F-out { a b }" ] ;
N036 -> N035 ;
N037 [ label="Label wp:post" ] ;
N037 -> N036 ;
N038 [ color=lightblue , label="B-out { __retres }" ] ;
N038 -> N037 ;
N039 [ color=orange , label="Return __retres" ] ;
N039 -> N038 ;
N040 [ label="Label wp:sid32 (Stmt s32)" ] ;
N040 -> N039 ;
N041 [ label="Label wp:sid31 (Stmt s31)" ] ;
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 ] ;
N044 -> N043 ;
N044 -> N042 ;
N045 [ label="Label wp:sid30 (Stmt s30)" ] ;
N045 -> N044 ;
N046 [ color=orange , label="__retres := a + b" ] ;
N046 -> N045 ;
N047 [ label="Label wp:sid13 (Stmt s13)" ] ;
N047 -> N046 ;
N048 [ label="Label wp:sid29 (Stmt s29)" ] ;
N048 -> N047 ;
N049 [ label="Label wp:sid11 (Stmt s11)" ] ;
N049 -> N048 ;
N050 [ color=lightblue , label="B-in { __retres }" ] ;
N050 -> N049 ;
N051 [ label="Label wp:post" ] ;
N051 [ color=lightblue , label="F-frame { a b }" ] ;
N051 -> N050 ;
N052 [ color=lightblue , label="B-out { __retres }" ] ;
N052 [ label="Label wp:pre" ] ;
N052 -> N051 ;
N053 [ color=orange , label="Return __retres" ] ;
N053 [ color=lightblue , label="F-in { a b }" ] ;
N053 -> N052 ;
N054 [ color=lightblue , label="B-out { }" ] ;
N054 [ color=lightblue , label="Global { }" ] ;
N054 -> N053 ;
N055 [ color=lightblue , label="B-out { }" ] ;
N055 [ color=cyan , label="Function g" ] ;
N055 -> N054 ;
N056 [ label="Label wp:sid32 (Stmt s32)" ] ;
N056 -> N055 ;
N057 [ label="Label wp:sid31 (Stmt s31)" ] ;
N057 -> N056 ;
N058 [ color=green , label="Assume g_assert" ] ;
N058 -> N057 ;
N059 [ color=red , label="Prove g_assert" ] ;
N059 -> N058 [ style=dotted ] ;
N060 [ label="" , shape=circle ] ;
N060 -> N059 ;
N060 -> N058 ;
N061 [ label="Label wp:sid30 (Stmt s30)" ] ;
N061 -> N060 ;
N062 [ color=orange , label="__retres := a + b" ] ;
N062 -> N061 ;
N063 [ label="Label wp:sid13 (Stmt s13)" ] ;
N063 -> N062 ;
N064 [ color=lightblue , label="B-in { }" ] ;
N064 -> N063 ;
N065 [ label="Label wp:sid29 (Stmt s29)" ] ;
N065 -> N064 ;
N066 [ color=lightblue , label="B-in { }" ] ;
N066 -> N065 ;
N067 [ label="Label wp:sid11 (Stmt s11)" ] ;
N067 -> N066 ;
N068 [ color=lightblue , label="B-in { __retres }" ] ;
N068 -> N067 ;
N069 [ color=lightblue , label="F-frame { a b }" ] ;
N069 -> N068 ;
N070 [ label="Label wp:pre" ] ;
N070 -> N069 ;
N071 [ color=lightblue , label="F-in { a b }" ] ;
N071 -> N070 ;
N072 [ color=lightblue , label="Global { }" ] ;
N072 -> N071 ;
N073 [ color=cyan , label="Function g" ] ;
N073 -> N072 ;
}
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