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

[wp] renaming call point properties

parent 2db3b393
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/dyncall.ml
+ 4
− 4
View file @ 32a40e44
......@@ -98,11 +98,11 @@ module CallPoints = State_builder.Hashtbl(Point.Hashtbl)(Calls)(CInfo)
let property ~kf ~bhv ~stmt calls =
let fact =
if bhv = Cil.default_behavior_name then
Format.asprintf "@[<hov 2>calls%a at s%d@]"
pp_calls calls stmt.sid
Format.asprintf "@[<hov 2>call point%a@]"
pp_calls calls
else
Format.asprintf "@[<hov 2>calls%a for %s at s%d@]"
pp_calls calls bhv stmt.sid
Format.asprintf "@[<hov 2>call point%a for %s@]"
pp_calls calls bhv
in
Property.(ip_other fact (OLStmt (kf,stmt)))
......
src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
+ 20
− 21
View file @ 32a40e44
......@@ -8,13 +8,14 @@
"rank": 16 },
"wp:main": { "total": 1, "valid": 1,
"rank": 16 } },
"call_stmt_calls_f1_f2": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 8 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 8 } },
"call_stmt_call_point_f1_f2": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 8 },
"wp:main":
{ "total": 1,
"valid": 1,
"rank": 8 } },
"call_post": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
......@@ -27,12 +28,10 @@
"wp:main": { "total": 4,
"valid": 4,
"rank": 16 } } },
"guarded_call": { "guarded_call_stmt_calls_g": { "qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"guarded_call": { "guarded_call_stmt_call_point_g":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"guarded_call_post_2": { "qed":
{ "total": 2,
"valid": 2 },
......@@ -57,11 +56,11 @@
"wp:main": { "total": 5,
"valid": 5,
"rank": 5 } } },
"behavior": { "behavior_stmt_calls_h1_h2": { "qed":
{ "total": 1,
"behavior": { "behavior_stmt_call_point_h1_h2": { "qed":
{ "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"wp:main":
{ "total": 1,
"valid": 1 } },
"behavior_bhv1_assign": { "qed": { "total": 6,
"valid": 6 },
......@@ -77,11 +76,11 @@
"valid": 9 },
"wp:main": { "total": 9,
"valid": 9 } } },
"some_behaviors": { "some_behaviors_stmt_calls_h1_h2_h0_for_bhv1":
"some_behaviors": { "some_behaviors_stmt_call_point_h1_h2_h0_for_bhv1":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"some_behaviors_stmt_calls_h1_h2_h0_for_bhv0":
"some_behaviors_stmt_call_point_h1_h2_h0_for_bhv0":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
......@@ -109,7 +108,7 @@
"valid": 24 },
"wp:main": { "total": 24,
"valid": 24 } } },
"missing_context": { "missing_context_stmt_calls_h1":
"missing_context": { "missing_context_stmt_call_point_h1":
{ "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
......@@ -137,7 +136,7 @@
"no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_32":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1, "valid": 1 } },
"no_call_stmt_calls_unreachable_g":
"no_call_stmt_call_point_unreachable_g":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1, "valid": 1 } },
"no_call_post": { "qed": { "total": 2,
......
src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+ 8
− 8
View file @ 32a40e44
......@@ -17,7 +17,7 @@
Function behavior with behavior bhv1
------------------------------------------------------------
Goal Calls h1 h2 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
Goal Call point h1 h2 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
Prove: true.
------------------------------------------------------------
......@@ -75,7 +75,7 @@ Prove: true.
Function call
------------------------------------------------------------
Goal Calls f1 f2 in 'call' at instruction (file tests/wp_plugin/dynamic.i, line 30):
Goal Call point f1 f2 in 'call' at instruction (file tests/wp_plugin/dynamic.i, line 30):
Let a = Mptr_0[shiftfield_F1_S_f(closure_0)].
Let a_1 = global(G_f2_26).
Let a_2 = global(G_f1_20).
......@@ -114,7 +114,7 @@ Assume {
(* Pre-condition *)
Have: abs_int(x) <= 5.
(* Instance of 'f1' *)
(* Calls f1 f2 *)
(* Call point f1 f2 *)
Have: Mptr_0[shiftfield_F1_S_f(closure_0)] = global(G_f1_20).
}
Prove: ((-10) <= x) /\ (x <= 10).
......@@ -124,7 +124,7 @@ Prove: ((-10) <= x) /\ (x <= 10).
Function guarded_call
------------------------------------------------------------
Goal Calls g in 'guarded_call' at instruction (file tests/wp_plugin/dynamic.i, line 44):
Goal Call point g in 'guarded_call' at instruction (file tests/wp_plugin/dynamic.i, line 44):
Prove: true.
------------------------------------------------------------
......@@ -163,7 +163,7 @@ Prove: true.
Function missing_context
------------------------------------------------------------
Goal Calls h1 in 'missing_context' at instruction (file tests/wp_plugin/dynamic.i, line 87):
Goal Call point h1 in 'missing_context' at instruction (file tests/wp_plugin/dynamic.i, line 87):
Assume { (* Heap *) Have: region(p.base) <= 0. }
Prove: global(G_h1_57) = p.
......@@ -195,7 +195,7 @@ Prove: true.
Function no_call
------------------------------------------------------------
Goal Calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 100):
Goal Call point unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 100):
Prove: true.
------------------------------------------------------------
......@@ -221,7 +221,7 @@ Prove: true.
Function some_behaviors with behavior bhv0
------------------------------------------------------------
Goal Calls h1 h2 h0 for bhv0 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
Goal Call point h1 h2 h0 for bhv0 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
Prove: true.
------------------------------------------------------------
......@@ -306,7 +306,7 @@ Prove: true.
Function some_behaviors with behavior bhv1
------------------------------------------------------------
Goal Calls h1 h2 h0 for bhv1 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
Goal Call point h1 h2 h0 for bhv1 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
Prove: true.
------------------------------------------------------------
......
src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+ 7
− 7
View file @ 32a40e44
......@@ -5,7 +5,7 @@
[wp] tests/wp_plugin/dynamic.i:78: Warning: Missing 'calls' for default behavior
[wp] Warning: Missing RTE guards
[wp] 51 goals scheduled
[wp] [Qed] Goal typed_behavior_stmt_calls_h1_h2 : Valid
[wp] [Qed] Goal typed_behavior_stmt_call_point_h1_h2 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part1 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_post_part2 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_assign_exit_part1 : Valid
......@@ -14,25 +14,25 @@
[wp] [Qed] Goal typed_behavior_bhv1_assign_normal_part2 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_assign_normal_part3 : Valid
[wp] [Qed] Goal typed_behavior_bhv1_assign_normal_part4 : Valid
[wp] [Alt-Ergo] Goal typed_call_stmt_calls_f1_f2 : Valid
[wp] [Alt-Ergo] Goal typed_call_stmt_call_point_f1_f2 : Valid
[wp] [Qed] Goal typed_call_post_part1 : Valid
[wp] [Qed] Goal typed_call_post_part2 : Valid
[wp] [Alt-Ergo] Goal typed_call_call_f1_pre : Valid
[wp] [Qed] Goal typed_guarded_call_stmt_calls_g : Valid
[wp] [Qed] Goal typed_guarded_call_stmt_call_point_g : Valid
[wp] [Alt-Ergo] Goal typed_guarded_call_post_part1 : Valid
[wp] [Qed] Goal typed_guarded_call_post_part2 : Valid
[wp] [Qed] Goal typed_guarded_call_post_2_part1 : Valid
[wp] [Qed] Goal typed_guarded_call_post_2_part2 : Valid
[wp] [Alt-Ergo] Goal typed_missing_context_stmt_calls_h1 : Unknown
[wp] [Alt-Ergo] Goal typed_missing_context_stmt_call_point_h1 : Unknown
[wp] [Qed] Goal typed_missing_context_post : Valid
[wp] [Qed] Goal typed_missing_context_assign_exit : Valid
[wp] [Qed] Goal typed_missing_context_assign_normal_part1 : Valid
[wp] [Qed] Goal typed_missing_context_assign_normal_part2 : Valid
[wp] [Qed] Goal typed_no_call_stmt_calls_unreachable_g : Valid
[wp] [Qed] Goal typed_no_call_stmt_call_point_unreachable_g : Valid
[wp] [Qed] Goal typed_no_call_post_part1 : Valid
[wp] [Qed] Goal typed_no_call_post_part2 : Valid
[wp] [Qed] Goal typed_no_call_call_unreachable_g_pre : Valid
[wp] [Qed] Goal typed_some_behaviors_stmt_calls_h1_h2_h0_for_bhv0 : Valid
[wp] [Qed] Goal typed_some_behaviors_stmt_call_point_h1_h2_h0_for_bhv0 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_post_part1 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_post_part2 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_post_part3 : Valid
......@@ -45,7 +45,7 @@
[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part4 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part5 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part6 : Valid
[wp] [Qed] Goal typed_some_behaviors_stmt_calls_h1_h2_h0_for_bhv1 : Valid
[wp] [Qed] Goal typed_some_behaviors_stmt_call_point_h1_h2_h0_for_bhv1 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_post_part1 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_post_part2 : Valid
[wp] [Qed] Goal typed_some_behaviors_bhv1_post_part3 : Valid
......
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