From 424e7898b658ca6d1ef8c5a53e71678266f0a9f3 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 31 Aug 2021 16:30:00 +0200
Subject: [PATCH] [kernel] Fix offsets handling checking logic lvals

---
 .../ast_queries/logic_typing.ml               | 12 ++++++++----
 tests/spec/assignable_location.i              | 19 +++++++++++++++++++
 tests/spec/assigns_const.i                    | 11 +++++++++++
 .../oracle/assignable_location.res.oracle     |  4 ++++
 tests/spec/oracle/assigns_const.res.oracle    | 11 +++++++++++
 5 files changed, 53 insertions(+), 4 deletions(-)

diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f9cfa246d8a..44868650b2f 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2317,6 +2317,13 @@ struct
          - host is memory access -> check if it is a const field access
       *)
       | TLval (lhost,loff) ->
+        let rec offsets = function
+          | TNoOffset -> true
+          | TIndex (_, n) -> offsets n
+          | TModel (_, n) -> m.accept_models && offsets n
+          | TField (f, n) ->
+            (not (Cil.isConstType f.ftype) || m.accept_const) && offsets n
+        in
         (not (isLogicArrayType t.term_type) || m.accept_array) &&
         (match lhost with
          | TVar v -> begin
@@ -2334,10 +2341,7 @@ struct
            end
          | TResult _ -> m.accept_models
          | _ -> true) &&
-        (match snd (Logic_utils.remove_term_offset loff) with
-         | TModel _ -> m.accept_models
-         | TField(f, _) -> not (Cil.isConstType f.ftype) || m.accept_const
-         | _ -> true)
+        offsets loff
       | TAddrOf lv when is_fct_ptr lv -> m.accept_func_ptr
       | TAddrOf lv | TStartOf lv ->
         m.accept_addrs &&
diff --git a/tests/spec/assignable_location.i b/tests/spec/assignable_location.i
index 70968c3735a..eac66f9fe9a 100644
--- a/tests/spec/assignable_location.i
+++ b/tests/spec/assignable_location.i
@@ -53,3 +53,22 @@ int * from_address_to_reject(int f){
   //@ behavior rej_1: assigns l \from &lx ;
   return (void*)0 ;
 }
+
+typedef struct _M {
+  int x;
+} M;
+
+struct N {
+  int y;
+};
+
+//@ model M { struct N z; };
+//@ model M { int t; };
+
+M m;
+
+//@ requires x == &m.t;
+void refuse_address_of_model_field(int* x);
+
+//@ requires x == &m.z.y;
+void refuse_subfield_of_model_field(int* x);
diff --git a/tests/spec/assigns_const.i b/tests/spec/assigns_const.i
index b12e589cd95..add0174e6fe 100644
--- a/tests/spec/assigns_const.i
+++ b/tests/spec/assigns_const.i
@@ -42,3 +42,14 @@ void accept_partial_const_struct(void)
 {
     z.y = 1;
 }
+
+struct T {
+  const struct Z z ;
+};
+struct T t ;
+
+
+//@ assigns t.z.y ; // y is not const but z is
+void refuse_const_path(void){
+
+}
diff --git a/tests/spec/oracle/assignable_location.res.oracle b/tests/spec/oracle/assignable_location.res.oracle
index 775b7573457..572a9b7f591 100644
--- a/tests/spec/oracle/assignable_location.res.oracle
+++ b/tests/spec/oracle/assignable_location.res.oracle
@@ -25,3 +25,7 @@
   unbound logic variable l. Ignoring logic specification of function from_address_to_reject
 [kernel:annot-error] tests/spec/assignable_location.i:53: Warning: 
   not an addressable left value: lx. Ignoring code annotation
+[kernel:annot-error] tests/spec/assignable_location.i:70: Warning: 
+  not an addressable left value: m.t. Ignoring specification of function refuse_address_of_model_field
+[kernel:annot-error] tests/spec/assignable_location.i:73: Warning: 
+  not an addressable left value: m.z.y. Ignoring specification of function refuse_subfield_of_model_field
diff --git a/tests/spec/oracle/assigns_const.res.oracle b/tests/spec/oracle/assigns_const.res.oracle
index 3a2391c45fe..31b54355d13 100644
--- a/tests/spec/oracle/assigns_const.res.oracle
+++ b/tests/spec/oracle/assigns_const.res.oracle
@@ -9,6 +9,8 @@
   not an assignable left value: y.a[4].f. Ignoring specification of function refuse_const_field
 [kernel:annot-error] tests/spec/assigns_const.i:25: Warning: 
   not an assignable left value: ptr->a[4].f. Ignoring specification of function refuse_field_via_pointer
+[kernel:annot-error] tests/spec/assigns_const.i:52: Warning: 
+  not an assignable left value: t.z.y. Ignoring logic specification of function refuse_const_path
 /* Generated by Frama-C */
 struct X {
    int const f ;
@@ -20,6 +22,9 @@ struct Z {
    int const x ;
    int y ;
 };
+struct T {
+   struct Z const z ;
+};
 int i;
 int const c;
 /*@ assigns i; */
@@ -38,4 +43,10 @@ void accept_partial_const_struct(void)
   return;
 }
 
+struct T t;
+void refuse_const_path(void)
+{
+  return;
+}
+
 
-- 
GitLab