From ca0d87d3993f57c64ad4e7b563b454b3f2173bef Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 17 Jan 2019 14:53:20 +0100
Subject: [PATCH] [wp] fixes dynamic calls
---
src/plugins/wp/dyncall.ml | 14 +-
.../tests/wp_plugin/dynamic.i.0.report.json | 101 ++++----
.../tests/wp_plugin/oracle/dynamic.res.oracle | 223 ++++++++++++++----
.../oracle_qualif/dynamic.res.oracle | 64 +++--
src/plugins/wp/wpAnnot.ml | 2 +-
5 files changed, 283 insertions(+), 121 deletions(-)
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index f57519b8a90..7e3e4259a2f 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -212,10 +212,18 @@ let compute () =
(* --- Registry --- *)
(* -------------------------------------------------------------------------- *)
-let get ?(bhv=Cil.default_behavior_name) stmt =
+let get ?bhv stmt =
compute () ;
- try CallPoints.find (bhv,stmt)
- with Not_found -> []
+ let get bhv =
+ try CallPoints.find (bhv,stmt)
+ with Not_found -> []
+ in
+ match bhv with
+ | None -> get Cil.default_behavior_name
+ | Some bhv ->
+ (match get bhv with
+ | [] -> get Cil.default_behavior_name
+ | l -> l)
(* -------------------------------------------------------------------------- *)
(* --- Registry --- *)
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 b97f0a37aa9..3fc42db1868 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
@@ -1,32 +1,30 @@
-{ "wp:global": { "alt-ergo": { "total": 12, "valid": 3, "unknown": 9,
- "rank": 14 },
- "qed": { "total": 10, "valid": 10 },
- "wp:main": { "total": 22, "valid": 13, "unknown": 9,
- "rank": 14 } },
+{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 16 },
+ "qed": { "total": 43, "valid": 43 },
+ "wp:main": { "total": 46, "valid": 46, "rank": 16 } },
"wp:functions": { "call": { "specialization_f1_pre_at_call_stmt_3":
{ "alt-ergo": { "total": 1, "valid": 1,
- "rank": 14 },
+ "rank": 16 },
"wp:main": { "total": 1, "valid": 1,
- "rank": 14 } },
+ "rank": 16 } },
"call_stmt_calls_f1_f2": { "alt-ergo":
{ "total": 1,
"valid": 1,
- "rank": 6 },
+ "rank": 8 },
"wp:main": { "total": 1,
"valid": 1,
- "rank": 6 } },
+ "rank": 8 } },
"call_post": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } },
"wp:section": { "alt-ergo": { "total": 2,
"valid": 2,
- "rank": 14 },
+ "rank": 16 },
"qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 4,
"valid": 4,
- "rank": 14 } } },
+ "rank": 16 } } },
"guarded_call": { "guarded_call_stmt_calls_g": { "qed":
{ "total": 1,
"valid": 1 },
@@ -57,48 +55,55 @@
"wp:main": { "total": 5,
"valid": 5,
"rank": 5 } } },
- "behavior": { "behavior_bhv1_assign": { "alt-ergo":
- { "total": 2,
- "unknown": 2 },
+ "behavior": { "behavior_stmt_for_bhv1_calls_h1_h2":
+ { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1, "valid": 1 } },
+ "behavior_bhv1_assign": { "qed": { "total": 6,
+ "valid": 6 },
"wp:main":
- { "total": 2,
- "unknown": 2 } },
- "behavior_bhv1_post": { "alt-ergo":
- { "total": 1,
- "unknown": 1 },
+ { "total": 6,
+ "valid": 6 } },
+ "behavior_bhv1_post": { "qed": { "total": 2,
+ "valid": 2 },
"wp:main":
- { "total": 1,
- "unknown": 1 } },
- "wp:section": { "alt-ergo": { "total": 3,
- "unknown": 3 },
- "wp:main": { "total": 3,
- "unknown": 3 } } },
- "some_behaviors": { "some_behaviors_bhv1_assign":
- { "alt-ergo": { "total": 2,
- "unknown": 2 },
- "wp:main": { "total": 2,
- "unknown": 2 } },
+ { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 9,
+ "valid": 9 },
+ "wp:main": { "total": 9,
+ "valid": 9 } } },
+ "some_behaviors": { "some_behaviors_stmt_for_bhv1_calls_h1_h2_h0":
+ { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "some_behaviors_stmt_for_bhv0_calls_h1_h2_h0":
+ { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "some_behaviors_bhv1_assign":
+ { "qed": { "total": 7, "valid": 7 },
+ "wp:main": { "total": 7,
+ "valid": 7 } },
"some_behaviors_bhv0_assign":
- { "alt-ergo": { "total": 2,
- "unknown": 2 },
- "wp:main": { "total": 2,
- "unknown": 2 } },
- "some_behaviors_bhv0_post": { "alt-ergo":
- { "total": 1,
- "unknown": 1 },
+ { "qed": { "total": 9, "valid": 9 },
+ "wp:main": { "total": 9,
+ "valid": 9 } },
+ "some_behaviors_bhv0_post": { "qed":
+ { "total": 3,
+ "valid": 3 },
"wp:main":
- { "total": 1,
- "unknown": 1 } },
- "some_behaviors_bhv1_post": { "alt-ergo":
- { "total": 1,
- "unknown": 1 },
+ { "total": 3,
+ "valid": 3 } },
+ "some_behaviors_bhv1_post": { "qed":
+ { "total": 3,
+ "valid": 3 },
"wp:main":
- { "total": 1,
- "unknown": 1 } },
- "wp:section": { "alt-ergo": { "total": 6,
- "unknown": 6 },
- "wp:main": { "total": 6,
- "unknown": 6 } } },
+ { "total": 3,
+ "valid": 3 } },
+ "wp:section": { "qed": { "total": 24,
+ "valid": 24 },
+ "wp:main": { "total": 24,
+ "valid": 24 } } },
"no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_27":
{ "qed": { "total": 1, "valid": 1 },
"wp:main": { "total": 1, "valid": 1 } },
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 7ce392e0cd6..339f2ca6cd5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -4,36 +4,63 @@
[wp] Computing dynamic calls.
[wp] Dynamic call(s): 5.
[wp] Loading driver 'share/wp.driver'
-[wp] tests/wp_plugin/dynamic.i:65: Warning:
- Ignored function pointer (see -wp-dynamic)
-[wp] tests/wp_plugin/dynamic.i:78: Warning:
- Ignored function pointer (see -wp-dynamic)
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/dynamic.i:65: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_plugin/dynamic.i:78: Warning:
- Missing assigns clause (assigns 'everything' instead)
------------------------------------------------------------
Function behavior with behavior bhv1
------------------------------------------------------------
-Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 62) in 'behavior':
-Assume { Type: is_sint32(X1_0). (* Heap *) Have: region(G_h1_57) <= 0. }
-Prove: X1_0 = 1.
+Goal for bhv1 calls h1 h2 in 'behavior' at instruction (file tests/wp_plugin/dynamic.i, line 65):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 62) in 'behavior' (1/2):
+Tags: Call h1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 62) in 'behavior' (2/2):
+Tags: Call h2.
+Prove: true.
------------------------------------------------------------
-Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior':
-Effect at line 65
-Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
-Prove: false.
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior' (2/2):
+Call Effect at line 65
+Tags: Call h2.
+Prove: true.
------------------------------------------------------------
-Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior':
-Effect at line 65
-Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
-Prove: false.
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior' (1/4):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior' (2/4):
+Call Effect at line 65
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior' (3/4):
+Call Result at line 65
+Tags: Call h1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 61) in 'behavior' (4/4):
+Call Result at line 65
+Tags: Call h2.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -153,50 +180,156 @@ Prove: true.
Function some_behaviors with behavior bhv0
------------------------------------------------------------
-Goal Post-condition for 'bhv0' (file tests/wp_plugin/dynamic.i, line 75) in 'some_behaviors':
-Assume {
- Type: is_sint32(X1_1) /\ is_sint32(X1_0).
- (* Heap *)
- Have: region(G_h0_68) <= 0.
-}
-Prove: X1_0 = X1_1.
+Goal for bhv0 calls h1 h2 h0 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv0' (file tests/wp_plugin/dynamic.i, line 75) in 'some_behaviors' (1/3):
+Tags: Call h0.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv0' (file tests/wp_plugin/dynamic.i, line 75) in 'some_behaviors' (2/3):
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv0' (file tests/wp_plugin/dynamic.i, line 75) in 'some_behaviors' (3/3):
+Tags: Call h1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (2/3):
+Call Effect at line 78
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (3/3):
+Call Effect at line 78
+Tags: Call h1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (1/6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (2/6):
+Call Effect at line 78
+Tags: Call h2.
+Prove: true.
------------------------------------------------------------
-Goal Assigns for 'bhv0' nothing in 'some_behaviors':
-Effect at line 78
-Assume { (* Heap *) Have: region(G_h0_68) <= 0. }
-Prove: false.
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (3/6):
+Call Effect at line 78
+Tags: Call h1.
+Prove: true.
------------------------------------------------------------
-Goal Assigns for 'bhv0' nothing in 'some_behaviors':
-Effect at line 78
-Assume { (* Heap *) Have: region(G_h0_68) <= 0. }
-Prove: false.
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (4/6):
+Call Result at line 78
+Tags: Call h0.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (5/6):
+Call Result at line 78
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv0' nothing in 'some_behaviors' (6/6):
+Call Result at line 78
+Tags: Call h1.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function some_behaviors with behavior bhv1
------------------------------------------------------------
-Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 71) in 'some_behaviors':
-Assume { Type: is_sint32(X1_0). (* Heap *) Have: region(G_h1_57) <= 0. }
-Prove: X1_0 = 1.
+Goal for bhv1 calls h1 h2 h0 in 'some_behaviors' at instruction (file tests/wp_plugin/dynamic.i, line 78):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 71) in 'some_behaviors' (1/3):
+Tags: Call h0.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 71) in 'some_behaviors' (2/3):
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'bhv1' (file tests/wp_plugin/dynamic.i, line 71) in 'some_behaviors' (3/3):
+Tags: Call h1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors' (1/2):
+Prove: true.
------------------------------------------------------------
-Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors':
-Effect at line 78
-Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
-Prove: false.
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors' (2/2):
+Call Effect at line 78
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors' (1/5):
+Prove: true.
------------------------------------------------------------
-Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors':
-Effect at line 78
-Assume { (* Heap *) Have: region(G_h1_57) <= 0. }
-Prove: false.
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors' (2/5):
+Call Effect at line 78
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors' (3/5):
+Call Result at line 78
+Tags: Call h0.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors' (4/5):
+Call Result at line 78
+Tags: Call h2.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns for 'bhv1' (file tests/wp_plugin/dynamic.i, line 70) in 'some_behaviors' (5/5):
+Call Result at line 78
+Tags: Call h1.
+Prove: true.
------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call':
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 407920ab0a3..358446cbbe9 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
@@ -4,19 +4,17 @@
[wp] Computing dynamic calls.
[wp] Dynamic call(s): 5.
[wp] Loading driver 'share/wp.driver'
-[wp] tests/wp_plugin/dynamic.i:65: Warning:
- Ignored function pointer (see -wp-dynamic)
-[wp] tests/wp_plugin/dynamic.i:78: Warning:
- Ignored function pointer (see -wp-dynamic)
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/dynamic.i:65: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_plugin/dynamic.i:78: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] 22 goals scheduled
-[wp] [Alt-Ergo] Goal typed_behavior_bhv1_post : Unknown
-[wp] [Alt-Ergo] Goal typed_behavior_bhv1_assign_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_behavior_bhv1_assign_normal : Unknown
+[wp] 46 goals scheduled
+[wp] [Qed] Goal typed_behavior_stmt_for_bhv1_calls_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
+[wp] [Qed] Goal typed_behavior_bhv1_assign_exit_part2 : Valid
+[wp] [Qed] Goal typed_behavior_bhv1_assign_normal_part1 : Valid
+[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] [Qed] Goal typed_call_post_part1 : Valid
[wp] [Qed] Goal typed_call_post_part2 : Valid
@@ -30,22 +28,40 @@
[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] [Alt-Ergo] Goal typed_some_behaviors_bhv0_post : Unknown
-[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv0_assign_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv0_assign_normal : Unknown
-[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv1_post : Unknown
-[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv1_assign_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_some_behaviors_bhv1_assign_normal : Unknown
-[wp] Proved goals: 13 / 22
- Qed: 10
- Alt-Ergo: 3 (unknown: 9)
+[wp] [Qed] Goal typed_some_behaviors_stmt_for_bhv0_calls_h1_h2_h0 : 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
+[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_exit_part1 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_exit_part2 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_exit_part3 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part1 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part2 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv0_assign_normal_part3 : Valid
+[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_for_bhv1_calls_h1_h2_h0 : 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
+[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_exit_part1 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_exit_part2 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part1 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part2 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part3 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part4 : Valid
+[wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part5 : Valid
+[wp] Proved goals: 46 / 46
+ Qed: 43
+ Alt-Ergo: 3
[wp] Report 'tests/wp_plugin/dynamic.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-call 2 2 (52..64) 4 100%
+call 2 2 (56..80) 4 100%
guarded_call 4 1 (16..28) 5 100%
-behavior - - 3 0.0%
-some_behaviors - - 6 0.0%
+behavior 9 - 9 100%
+some_behaviors 24 - 24 100%
no_call 4 - 4 100%
-------------------------------------------------------------
[wp] Warning: Memory model hypotheses for function 'guarded_call':
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index d09c0a11e90..98b350f6eb6 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -769,7 +769,7 @@ let get_call_annots config v s fct =
if calls=[] then
begin
Wp_parameters.warning ~once:true ~source:(fst (Stmt.loc s))
- "Ignored function pointer (see -wp-dynamic)" ;
+ "Missigns 'calls' clause dedicated to dynamic calls (see WP manual)";
let annots = WpStrategy.add_call_assigns_any WpStrategy.empty_acc s in
WpStrategy.empty_acc, (annots , annots)
end
--
GitLab