From 32a40e44c3ba7de4dea1d09d2af83d0fa48fd65d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 29 Jan 2019 09:01:26 +0100
Subject: [PATCH] [wp] renaming call point properties
---
src/plugins/wp/dyncall.ml | 8 ++--
.../tests/wp_plugin/dynamic.i.0.report.json | 41 +++++++++----------
.../tests/wp_plugin/oracle/dynamic.res.oracle | 16 ++++----
.../oracle_qualif/dynamic.res.oracle | 14 +++----
4 files changed, 39 insertions(+), 40 deletions(-)
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index 3fdd8a3bcca..30251894440 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -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)))
diff --git a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
index a092c5cd51e..4ef68bd712e 100644
--- a/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json
@@ -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,
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index 80192d5d7d4..7c09c9927c0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index 38972927867..ae804245795 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -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
--
GitLab