diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 7e485e323bef5d461e2985706f00e47022059611..560df2f561d6b89dec4b452815df43f21035c38a 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -843,23 +843,15 @@ struct
module Nullable_extension =
struct
- let type_term typing_context loc e =
- match e.Logic_ptree.lexpr_node with
- | Logic_ptree.PLvar s ->
- let lv = typing_context.Logic_typing.find_var s in
- begin match lv.lv_origin with
- | Some vi when Cil.isPointerType vi.vtype && vi.vformal ->
- make_nullable vi ;
- Logic_const.tvar ~loc lv
- | _ ->
- typing_context.error loc "No pointer: %s" s
- end
- | _ ->
- typing_context.error loc "Illegal expression %a"
- Logic_print.print_lexpr e
-
- let typer typing_context loc l =
- Ext_terms (List.map (type_term typing_context loc) l)
+ let type_term ctxt loc e =
+ match ctxt.Logic_typing.type_term ctxt ctxt.pre_state e with
+ | { term_node = TLval (TVar { lv_origin = Some vi }, TNoOffset) } as term
+ when Cil.isPointerType vi.vtype && vi.vformal ->
+ make_nullable vi ; term
+ | t -> ctxt.error loc "Not a formal pointer: %a" Cil_printer.pp_term t
+
+ let typer ctxt loc l =
+ Ext_terms (List.map (type_term ctxt loc) l)
end
let () =
diff --git a/src/plugins/wp/tests/wp_plugin/nullable_ext.c b/src/plugins/wp/tests/wp_plugin/nullable_ext.c
new file mode 100644
index 0000000000000000000000000000000000000000..a275cb746380c0809ec8d906a7c4db515c198ec6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nullable_ext.c
@@ -0,0 +1,75 @@
+/* run.config
+ OPT: -wp-model Caveat
+ EXIT: 1
+ OPT: -cpp-extra-args="-DFAIL_1"
+ EXIT: 1
+ OPT: -cpp-extra-args="-DFAIL_2"
+ EXIT: 1
+ OPT: -cpp-extra-args="-DFAIL_3"
+ EXIT: 1
+ OPT: -cpp-extra-args="-DFAIL_4"
+*/
+/* run.config_qualif
+ OPT: -wp-model Caveat
+*/
+
+int x;
+int *g;
+
+/*@ assigns *g, *p, x ;
+ wp_nullable_args p ;
+*/
+void nullable_coherence(int *p) {
+ if (p == (void *)0) {
+ //@ check must_fail: \false ;
+ return;
+ }
+ //@ check \valid(p);
+ *p = 42;
+ *g = 24;
+ x = 1;
+}
+
+/*@ assigns *p, *q, *r, *s, *t ;
+ wp_nullable_args p, q, r ;
+*/
+void nullable_in_context(int *p, int *q, int *r, int *s, int *t) {
+ *p = 42;
+ *q = 42;
+ *r = 42;
+ *s = *t = 0;
+}
+
+/*@ assigns *ptr ;
+ wp_nullable_args ptr ;
+*/
+void with_declaration(int *ptr);
+void with_declaration(int *ptr) {}
+
+#ifdef FAIL_1
+/*@ assigns *ptr ;
+ wp_nullable_args unexisting_ptr ;
+*/
+void fails_no_variable(int *ptr) {}
+#endif
+
+#ifdef FAIL_2
+/*@ assigns *ptr ;
+ wp_nullable_args *ptr ;
+*/
+void not_a_variable(int *ptr) {}
+#endif
+
+#ifdef FAIL_3
+/*@ assigns *ptr ;
+ wp_nullable_args g ;
+*/
+void not_a_formal(int *ptr) {}
+#endif
+
+#ifdef FAIL_4
+/*@ assigns x ;
+ wp_nullable_args f ;
+*/
+void not_a_pointer(int f) {}
+#endif
diff --git a/src/plugins/wp/tests/wp_plugin/nullable_ext.i b/src/plugins/wp/tests/wp_plugin/nullable_ext.i
deleted file mode 100644
index 7225aa000f21516ce9c2596b9ff62f4e7245e7ca..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/nullable_ext.i
+++ /dev/null
@@ -1,33 +0,0 @@
-/* run.config
- OPT: -wp-model Caveat
-*/
-/* run.config_qualif
- OPT: -wp-model Caveat
-*/
-
-int x ;
-int *g ;
-
-/*@ assigns *g, *p, x ;
- wp_nullable_args p ;
-*/
-void nullable_coherence(int* p){
- if(p == (void*)0){
- //@ check must_fail: \false ;
- return;
- }
- //@ check \valid(p);
- *p = 42;
- *g = 24;
- x = 1;
-}
-
-/*@ assigns *p, *q, *r, *s, *t ;
- wp_nullable_args p, q, r ;
-*/
-void nullable_in_context(int* p, int* q, int* r, int* s, int* t){
- *p = 42;
- *q = 42;
- *r = 42;
- *s = *t = 0;
-}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dac33ed12fdcfebe2bacb5af61c8cf3927889b98
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.0.res.oracle
@@ -0,0 +1,81 @@
+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In caveat model with nullable arguments, -wp-(no)-rte shall be explicitly positioned.
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function nullable_coherence
+------------------------------------------------------------
+
+Goal Check 'must_fail' (file tests/wp_plugin/nullable_ext.c, line 24):
+Assume { (* Then *) Have: null = pointer_p. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_plugin/nullable_ext.c, line 27):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.c, line 19) in 'nullable_coherence':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function nullable_in_context
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.c, line 33) in 'nullable_in_context' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.c, line 33) in 'nullable_in_context' (2/2):
+Effect at line 40
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function with_declaration
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.c, line 43) in 'with_declaration':
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable_ext.c:22: Warning:
+ Memory model hypotheses for function 'nullable_coherence':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(g);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \separated(g, &x);
+ requires \separated(p, &x);
+ requires p ≢ \null ⇒ \separated(g, p, &x);
+ */
+ void nullable_coherence(int *p /*@ wp_nullable */);
+[wp] tests/wp_plugin/nullable_ext.c:36: Warning:
+ Memory model hypotheses for function 'nullable_in_context':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(s);
+ requires \valid(t);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \valid(q) ∨ q ≡ \null;
+ requires \valid(r) ∨ r ≡ \null;
+ requires p ≢ \null ⇒ \separated(p, s, t);
+ requires q ≢ \null ⇒ \separated(q, s, t);
+ requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
+ requires r ≢ \null ⇒ \separated(r, s, t);
+ requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
+ requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
+ */
+ void nullable_in_context(int *p /*@ wp_nullable */,
+ int *q /*@ wp_nullable */,
+ int *r /*@ wp_nullable */, int *s, int *t);
+[wp] tests/wp_plugin/nullable_ext.c:47: Warning:
+ Memory model hypotheses for function 'with_declaration':
+ /*@ behavior wp_typed_caveat:
+ requires \valid(ptr); */
+ void with_declaration(int *ptr);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0c146cf96b37343b2cd454bd8fcfcefd72797cdd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.1.res.oracle
@@ -0,0 +1,8 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.c (with preprocessing)
+[kernel:annot-error] tests/wp_plugin/nullable_ext.c:51: Warning:
+ unbound logic variable unexisting_ptr. Ignoring logic specification of function fails_no_variable
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] User Error: stopping on file "tests/wp_plugin/nullable_ext.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..819fcbfcd31bcb537c5345b133abd51d6aa4aae1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.2.res.oracle
@@ -0,0 +1,8 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.c (with preprocessing)
+[kernel:annot-error] tests/wp_plugin/nullable_ext.c:58: Warning:
+ Not a formal pointer: *ptr. Ignoring logic specification of function not_a_variable
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] User Error: stopping on file "tests/wp_plugin/nullable_ext.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..285a641420968c41034552a07c095a86b5968c8c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.3.res.oracle
@@ -0,0 +1,8 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.c (with preprocessing)
+[kernel:annot-error] tests/wp_plugin/nullable_ext.c:65: Warning:
+ Not a formal pointer: g. Ignoring logic specification of function not_a_formal
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] User Error: stopping on file "tests/wp_plugin/nullable_ext.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5698598d9ad31ab8834e5f4253b41a1a330264db
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.4.res.oracle
@@ -0,0 +1,8 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.c (with preprocessing)
+[kernel:annot-error] tests/wp_plugin/nullable_ext.c:72: Warning:
+ Not a formal pointer: f. Ignoring logic specification of function not_a_pointer
+[kernel] User Error: warning annot-error treated as fatal error.
+[kernel] User Error: stopping on file "tests/wp_plugin/nullable_ext.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
index 1f2fed4938befc5db60a585320ff3e63bce02d74..7fa4b856bf53f4ff8555ae8e2f4286d3b65ac86b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
@@ -1,23 +1,25 @@
# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing tests/wp_plugin/nullable_ext.i (no preprocessing)
+[kernel] Parsing tests/wp_plugin/nullable_ext.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: In caveat model with nullable arguments, -wp-(no)-rte shall be explicitly positioned.
[wp] Warning: Missing RTE guards
-[wp] 5 goals scheduled
+[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_caveat_nullable_coherence_check_must_fail : Unsuccess
[wp] [Qed] Goal typed_caveat_nullable_coherence_check : Valid
[wp] [Qed] Goal typed_caveat_nullable_coherence_assigns : Valid
[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part1 : Valid
[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part2 : Valid
-[wp] Proved goals: 4 / 5
- Qed: 4
+[wp] [Qed] Goal typed_caveat_with_declaration_assigns : Valid
+[wp] Proved goals: 5 / 6
+ Qed: 5
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
nullable_coherence 2 - 3 66.7%
nullable_in_context 2 - 2 100%
+ with_declaration 1 - 1 100%
------------------------------------------------------------
-[wp] tests/wp_plugin/nullable_ext.i:14: Warning:
+[wp] tests/wp_plugin/nullable_ext.c:22: Warning:
Memory model hypotheses for function 'nullable_coherence':
/*@
behavior wp_typed_caveat:
@@ -28,7 +30,7 @@
requires p ≢ \null ⇒ \separated(g, p, &x);
*/
void nullable_coherence(int *p /*@ wp_nullable */);
-[wp] tests/wp_plugin/nullable_ext.i:28: Warning:
+[wp] tests/wp_plugin/nullable_ext.c:36: Warning:
Memory model hypotheses for function 'nullable_in_context':
/*@
behavior wp_typed_caveat:
@@ -47,3 +49,8 @@
void nullable_in_context(int *p /*@ wp_nullable */,
int *q /*@ wp_nullable */,
int *r /*@ wp_nullable */, int *s, int *t);
+[wp] tests/wp_plugin/nullable_ext.c:47: Warning:
+ Memory model hypotheses for function 'with_declaration':
+ /*@ behavior wp_typed_caveat:
+ requires \valid(ptr); */
+ void with_declaration(int *ptr);