diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 5f0767c667b169e7b5eff49b5007636e14a92a0b..869a3f3915845f8bf290cc1f736ed76c918ad304 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -709,15 +709,22 @@ struct
obj , domain , seq , loc
let cc_stored lv seq loc obj expr =
- if Cil.isVolatileLval lv &&
- Cvalues.volatile ~warn:"unsafe write-access to volatile l-value" ()
- then None
+ let intercept_volatile kind lv =
+ let warn = "unsafe " ^ kind ^ "-access to volatile l-value" in
+ Cil.isVolatileLval lv && Cvalues.volatile ~warn ()
+ in
+ if intercept_volatile "write" lv then None
else
let value = match expr.enode with
- | Lval lv -> M.copied seq obj loc (C.lval seq.pre lv)
- | _ -> M.stored seq obj loc (C.val_of_exp seq.pre expr)
+ | Lval lv when not @@ intercept_volatile "read" lv ->
+ M.copied seq obj loc (C.lval seq.pre lv)
+ | _ ->
+ (* Note: a volatile lval will be compiled to an unknown value *)
+ M.stored seq obj loc (C.val_of_exp seq.pre expr)
in
let init = match expr.enode with
+ | Lval lv when intercept_volatile "read" lv ->
+ M.stored_init seq obj loc (Cvalues.initialized_obj obj)
| Lval lv when Cil.(isStructOrUnionType @@ typeOfLval lv) ->
M.copied_init seq obj loc (C.lval seq.pre lv)
| _ ->
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
index 2df04eb693e0221ae001c0fbd615d432dec4cd3c..b24ccc3ce53c9991dc222d4927c9798cd922f55a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle
@@ -2,11 +2,24 @@
[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function default_init
+------------------------------------------------------------
+
+Goal Check 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 46):
+Assume {
+ Type: is_sint8(ClientId_0) /\ is_sint32(R1_0).
+ (* Pre-condition *)
+ Have: (0 <= ClientId_0) /\ (ClientId_0 <= 15).
+}
+Prove: R1_0 = 0.
+
+------------------------------------------------------------
------------------------------------------------------------
Function job_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 15):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 16):
Prove: w = 0.
------------------------------------------------------------
@@ -14,7 +27,7 @@ Prove: w = 0.
Function job_read
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 21):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 22):
Assume { Type: is_sint32(x). }
Prove: x = w.
@@ -23,7 +36,7 @@ Prove: x = w.
Function job_struct
------------------------------------------------------------
-Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 29):
+Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 30):
Prove: true.
------------------------------------------------------------
@@ -31,11 +44,11 @@ Prove: true.
Function job_struct_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 36):
Prove: EqS1_st_v(w, w_1).
------------------------------------------------------------
-[wp] tests/wp_plugin/volatile.i:32: Warning:
+[wp] tests/wp_plugin/volatile.i:33: Warning:
Memory model hypotheses for function 'job_struct_assigns':
/*@ behavior wp_typed:
requires \separated(p, &sv); */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
index 63e2b65a2c49a5ca6bf4edcaf5f179a9121e0b6d..c93f2248bbf30e4332b712a26b366f59212dc1d7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle
@@ -2,29 +2,54 @@
[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/volatile.i:15: Warning:
+[wp] tests/wp_plugin/volatile.i:16: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:14: Warning:
+[wp] tests/wp_plugin/volatile.i:15: Warning:
unsafe write-access to volatile l-value
-[wp] tests/wp_plugin/volatile.i:21: Warning:
+[wp] tests/wp_plugin/volatile.i:22: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:20: Warning:
+[wp] tests/wp_plugin/volatile.i:21: Warning:
unsafe read-access to volatile l-value
-[wp] tests/wp_plugin/volatile.i:35: Warning:
+[wp] tests/wp_plugin/volatile.i:36: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:35: Warning:
+[wp] tests/wp_plugin/volatile.i:36: Warning:
unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:34: Warning:
+[wp] tests/wp_plugin/volatile.i:35: Warning:
unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning:
+ unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:45: Warning:
+ unsafe read-access to volatile l-value
+------------------------------------------------------------
+ Function default_init
+------------------------------------------------------------
+
+Goal Check 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 46):
+tests/wp_plugin/volatile.i:45: warning from wp:
+ - Warning: ignore volatile attribute
+ Reason: unsafe read-access to volatile l-value
+Let x = GlobalConst_0[ClientId_0].
+Assume {
+ Type: is_sint8(ClientId_0) /\ is_sint32(x).
+ (* Heap *)
+ Type: IsArray_sint32(GlobalConst_0).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 15) -> (GlobalConst_0[i] = 0))).
+ (* Pre-condition *)
+ Have: (0 <= ClientId_0) /\ (ClientId_0 <= 15).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
------------------------------------------------------------
Function job_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 15):
-tests/wp_plugin/volatile.i:14: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 16):
+tests/wp_plugin/volatile.i:15: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe write-access to volatile l-value
-tests/wp_plugin/volatile.i:15: warning from wp:
+tests/wp_plugin/volatile.i:16: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
Prove: true.
@@ -34,11 +59,11 @@ Prove: true.
Function job_read
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 21):
-tests/wp_plugin/volatile.i:20: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 22):
+tests/wp_plugin/volatile.i:21: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe read-access to volatile l-value
-tests/wp_plugin/volatile.i:21: warning from wp:
+tests/wp_plugin/volatile.i:22: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
Prove: true.
@@ -48,7 +73,7 @@ Prove: true.
Function job_struct
------------------------------------------------------------
-Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 29):
+Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 30):
Prove: true.
------------------------------------------------------------
@@ -56,20 +81,23 @@ Prove: true.
Function job_struct_assigns
------------------------------------------------------------
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
-tests/wp_plugin/volatile.i:34: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 36):
+tests/wp_plugin/volatile.i:35: warning from wp:
- Warning: ignore volatile attribute
- Reason: unsafe write-access to volatile l-value
+ Reason: unsafe read-access to volatile l-value
tests/wp_plugin/volatile.i:35: warning from wp:
+ - Warning: ignore volatile attribute
+ Reason: unsafe write-access to volatile l-value
+tests/wp_plugin/volatile.i:36: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
-tests/wp_plugin/volatile.i:35: warning from wp:
+tests/wp_plugin/volatile.i:36: warning from wp:
- Warning: ignore volatile attribute
Reason: unsafe volatile access to (term) l-value
Prove: true.
------------------------------------------------------------
-[wp] tests/wp_plugin/volatile.i:32: Warning:
+[wp] tests/wp_plugin/volatile.i:33: Warning:
Memory model hypotheses for function 'job_struct_assigns':
/*@ behavior wp_typed:
requires \separated(p, &sv); */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..51ab2374303a31162f49c5cba1909d674157fb7a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.0.res.oracle
@@ -0,0 +1,26 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal typed_job_assigns_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_read_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Qed] Goal typed_job_struct_assert_ok_dead_code : Valid
+[wp] [Alt-Ergo] Goal typed_job_struct_assigns_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Alt-Ergo] Goal typed_default_init_check_KO_WHEN_VOLATILE : Unsuccess
+[wp] Proved goals: 1 / 5
+ Qed: 1
+ Alt-Ergo: 0 (unsuccess: 4)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job_assigns - - 1 0.0%
+ job_read - - 1 0.0%
+ job_struct 1 - 1 100%
+ job_struct_assigns - - 1 0.0%
+ default_init - - 1 0.0%
+------------------------------------------------------------
+[wp] tests/wp_plugin/volatile.i:33: Warning:
+ Memory model hypotheses for function 'job_struct_assigns':
+ /*@ behavior wp_typed:
+ requires \separated(p, &sv); */
+ void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bfc0ecc2ae39d06cb58566862af0fc0f9a0c2ceb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.1.res.oracle
@@ -0,0 +1,44 @@
+# frama-c -wp -wp-no-volatile [...]
+[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_plugin/volatile.i:16: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:15: Warning:
+ unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:22: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:21: Warning:
+ unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:36: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:36: Warning:
+ unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning:
+ unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning:
+ unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:45: Warning:
+ unsafe read-access to volatile l-value
+[wp] 5 goals scheduled
+[wp] [Qed] Goal typed_job_assigns_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Qed] Goal typed_job_read_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Qed] Goal typed_job_struct_assert_ok_dead_code : Valid
+[wp] [Qed] Goal typed_job_struct_assigns_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Alt-Ergo] Goal typed_default_init_check_KO_WHEN_VOLATILE : Valid
+[wp] Proved goals: 5 / 5
+ Qed: 4
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job_assigns 1 - 1 100%
+ job_read 1 - 1 100%
+ job_struct 1 - 1 100%
+ job_struct_assigns 1 - 1 100%
+ default_init - 1 1 100%
+------------------------------------------------------------
+[wp] tests/wp_plugin/volatile.i:33: Warning:
+ Memory model hypotheses for function 'job_struct_assigns':
+ /*@ behavior wp_typed:
+ requires \separated(p, &sv); */
+ void job_struct_assigns(struct st_v *p);
diff --git a/src/plugins/wp/tests/wp_plugin/volatile.i b/src/plugins/wp/tests/wp_plugin/volatile.i
index 81be3c130b37e940d99c901af4ad44c1a8a1bd9c..49c337571ffbf7ee91e6a35cccc053fc33bce4d3 100644
--- a/src/plugins/wp/tests/wp_plugin/volatile.i
+++ b/src/plugins/wp/tests/wp_plugin/volatile.i
@@ -2,11 +2,12 @@
OPT:
OPT: -wp-no-volatile
*/
-
/* run.config_qualif
- DONTRUN:
+ OPT:
+ OPT: -wp-no-volatile
*/
+
volatile int v ;
void job_assigns(void)
@@ -34,3 +35,13 @@ void job_struct_assigns(struct st_v *p)
*p = sv;
/*@ assert KO_WHEN_VOLATILE: *p == sv ; */ ;
}
+
+int const volatile GlobalConst[16];
+
+/*@ requires 0 ≤ ClientId < 16; */
+void default_init(char const ClientId)
+{
+ int R1;
+ R1 = GlobalConst[ClientId];
+ //@ check KO_WHEN_VOLATILE: R1 == 0 ;
+}