From 02306a1ea4a89890a4a4ea7d565251e27a144235 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 31 Oct 2019 15:20:23 +0100
Subject: [PATCH] [kernel/volatile] better handling of const
---
.../ast_queries/logic_typing.ml | 46 ++++++++++---------
tests/spec/oracle/volatile_const.res.oracle | 24 ++++++++++
tests/spec/volatile_const.i | 18 ++++++++
3 files changed, 67 insertions(+), 21 deletions(-)
create mode 100644 tests/spec/oracle/volatile_const.res.oracle
create mode 100644 tests/spec/volatile_const.i
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 44868650b2f..5b964ffa994 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4216,33 +4216,39 @@ struct
List.map
(term_lval_assignable ctxt ~accept_formal ~accept_const env) tsets
in
- let checks_tsets_type fct ctyp =
+ let checks_tsets_type ~reads fct ctyp =
List.iter
- (fun t ->
- let check t = match Logic_utils.unroll_type t with
- | Ctype ctyp' -> Cil_datatype.Typ.equal ctyp ctyp'
- | _ -> false
- in
- if not (Logic_const.plain_or_set check t.term_type) then
- C.error t.term_loc "incompatible prototype of '%s' with %a"
- fct Cil_printer.pp_term t )
- tsets
+ begin fun t ->
+ let check t = match Logic_utils.unroll_type t with
+ | Ctype ctyp' ->
+ ( reads || not (Cil.isConstType ctyp') )
+ && Cil_datatype.Typ.equal ctyp
+ (Cil.type_remove_qualifier_attributes ctyp')
+ | _ -> false
+ in
+ if not (Logic_const.plain_or_set check t.term_type) then
+ C.error t.term_loc
+ "@[<hov 0>can not use '%s' to %s volatile @[<hov 2>'%a'@]"
+ fct (if reads then "read" else "write")
+ Cil_printer.pp_term t
+ end tsets
in
let prototype_error s fct =
C.error loc
"incompatible prototype of '%s' with volatile %s declaration"
fct s
in
- let volatile_type ret_typ arg1 error =
+ let volatile_type ~reads ret_typ arg1 error =
(* note: type pointed to by arg1 may differ from the
return type with respect to qualifiers *)
if not (isPointerType arg1) then error ();
let vol_typ = typeOf_pointed arg1 in
- if not (Cil.isVolatileType vol_typ
- && Cil_datatype.Typ.equal ret_typ
- (Cil.type_remove_qualifier_attributes vol_typ))
+ let base_typ = Cil.type_remove_qualifier_attributes vol_typ in
+ if not (Cil.isVolatileType vol_typ &&
+ ( reads || not (Cil.isConstType vol_typ) ) &&
+ Cil_datatype.Typ.equal ret_typ base_typ)
then error ();
- vol_typ
+ base_typ
in
let checks_reads_fct fct ty =
let error () = prototype_error "reads" fct
@@ -4254,10 +4260,8 @@ struct
| Some [_,arg1,_] when
(not (isVoidType ret || is_varg_arg))
-> (* matching prototype: T fct (volatile T *arg1) *)
- let vol_typ = volatile_type ret arg1 error in
- if Cil.isConstType vol_typ then
- Kernel.warning ~current:true "Access function '%s' writes to volatile const locations" fct;
- checks_tsets_type fct vol_typ (* tsets should have type: volatile T *)
+ let vol_typ = volatile_type ~reads:true ret arg1 error in
+ checks_tsets_type ~reads:true fct vol_typ (* tsets should have type: volatile T *)
| _ ->
error ()
in
@@ -4272,8 +4276,8 @@ struct
(not (isVoidType ret || is_varg_arg))
&& Cil_datatype.Typ.equal ret (Cil.type_remove_qualifier_attributes arg2)
-> (* matching prototype: T fct (volatile T *arg1, T arg2) *)
- let vol_typ = volatile_type ret arg1 error in
- checks_tsets_type fct vol_typ (* tsets should have type: volatile T *)
+ let vol_typ = volatile_type ~reads:false ret arg1 error in
+ checks_tsets_type ~reads:false fct vol_typ (* tsets should have type: volatile T *)
| _ ->
error ()
in
diff --git a/tests/spec/oracle/volatile_const.res.oracle b/tests/spec/oracle/volatile_const.res.oracle
new file mode 100644
index 00000000000..26c96973298
--- /dev/null
+++ b/tests/spec/oracle/volatile_const.res.oracle
@@ -0,0 +1,24 @@
+[kernel] Parsing tests/spec/volatile_const.i (no preprocessing)
+[kernel:annot-error] tests/spec/volatile_const.i:16: Warning:
+ incompatible prototype of 'wr_const' with volatile writes declaration. Ignoring global annotation
+[kernel:annot-error] tests/spec/volatile_const.i:17: Warning:
+ incompatible prototype of 'wr_const' with volatile writes declaration. Ignoring global annotation
+[kernel:annot-error] tests/spec/volatile_const.i:18: Warning:
+ can not use 'wr' to write volatile 'd_ro'. Ignoring global annotation
+/* Generated by Frama-C */
+int volatile a_rw;
+int volatile b_rw;
+int const volatile c_ro;
+int const volatile d_ro;
+int rd(int volatile *p);
+
+int rd_const(int const volatile *p);
+
+int wr(int volatile *p, int v);
+
+/*@ volatile a_rw reads rd; */
+/*@ volatile b_rw reads rd_const; */
+/*@ volatile c_ro reads rd_const; */
+/*@ volatile d_ro reads rd; */
+/*@ volatile a_rw writes wr; */
+
diff --git a/tests/spec/volatile_const.i b/tests/spec/volatile_const.i
new file mode 100644
index 00000000000..e6ecc39b5a8
--- /dev/null
+++ b/tests/spec/volatile_const.i
@@ -0,0 +1,18 @@
+volatile int a_rw,b_rw ;
+volatile const int c_ro,d_ro ;
+
+int rd(volatile int *p);
+int rd_const(volatile const int *p);
+
+int wr(volatile int *p,int v);
+int wr_const(volatile const int *p,int v);
+
+//@ volatile a_rw reads rd ; // OK
+//@ volatile b_rw reads rd_const ; // OK
+//@ volatile c_ro reads rd_const ; // OK
+//@ volatile d_ro reads rd ; // OK
+
+//@ volatile a_rw writes wr ; // OK
+//@ volatile b_rw writes wr_const ; // KO
+//@ volatile c_ro writes wr_const ; // KO
+//@ volatile d_ro writes wr ; // KO
--
GitLab