From 6caa32f5475615ac9985d5a508666a5b185935f0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 31 Aug 2021 10:38:29 +0200
Subject: [PATCH] [kernel] accept non const field assigns
---
src/kernel_services/ast_queries/logic_typing.ml | 6 +++++-
tests/spec/assigns_const.i | 13 +++++++++++++
tests/spec/oracle/assigns_const.res.oracle | 12 ++++++++++++
3 files changed, 30 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index a1b0106a435..f9cfa246d8a 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2312,6 +2312,10 @@ struct
let check_lval_kind m t =
let rec aux t = match t.term_node with
| Tempty_set -> m.accept_empty
+ (* Be careful with const lval, cases are:
+ - *host* is variable -> the assigned *lval* must not be const
+ - host is memory access -> check if it is a const field access
+ *)
| TLval (lhost,loff) ->
(not (isLogicArrayType t.term_type) || m.accept_array) &&
(match lhost with
@@ -2326,7 +2330,7 @@ struct
model variables are not supported. *)
| Some v ->
(not v.vformal || m.accept_formal) &&
- (not (Cil.isConstType v.vtype) || m.accept_const)
+ (not (isConstType @@ logicCType t.term_type) || m.accept_const)
end
| TResult _ -> m.accept_models
| _ -> true) &&
diff --git a/tests/spec/assigns_const.i b/tests/spec/assigns_const.i
index 6aedfe366b9..b12e589cd95 100644
--- a/tests/spec/assigns_const.i
+++ b/tests/spec/assigns_const.i
@@ -29,3 +29,16 @@ void refuse_field_via_pointer(struct Y * ptr);
//@ assigns *ptr ;
void accept_const_via_pointer(int const * ptr);
+
+struct Z {
+ const int x;
+ int y;
+};
+
+static struct Z z;
+
+//@ assigns z.y;
+void accept_partial_const_struct(void)
+{
+ z.y = 1;
+}
diff --git a/tests/spec/oracle/assigns_const.res.oracle b/tests/spec/oracle/assigns_const.res.oracle
index 9279fd42e10..3a2391c45fe 100644
--- a/tests/spec/oracle/assigns_const.res.oracle
+++ b/tests/spec/oracle/assigns_const.res.oracle
@@ -16,6 +16,10 @@ struct X {
struct Y {
struct X a[10] ;
};
+struct Z {
+ int const x ;
+ int y ;
+};
int i;
int const c;
/*@ assigns i; */
@@ -26,4 +30,12 @@ struct Y y;
/*@ assigns *ptr; */
void accept_const_via_pointer(int const *ptr);
+static struct Z z;
+/*@ assigns z.y; */
+void accept_partial_const_struct(void)
+{
+ z.y = 1;
+ return;
+}
+
--
GitLab