[E-ACSL] analysis: fixed bug in presence of an alias with an explicit address

src/plugins/e-acsl/known_bugs/taking_address.i

-int main(){
-  int m, *u, *p;
-  u = &m;
-  p = u;
-  m = 123;
-  //@ assert \initialized(p);
-}

src/plugins/e-acsl/pre_analysis.ml

@@ -367,7 +367,22 @@ module rec Transfer
 	| Some vi -> add_vi state vi
     in
     match instr with
-    | Set((lhost, _), e, _) -> 
+    | Set((lhost, _) as lv, e, _) -> 
+      (* if [e]  contains an address from a base to be monitored, then also
+	 monitor the host *)
+      let rec extend_from_addr state e = match e.enode with
+	| AddrOf(lhost, _) -> 
+	  extend_to_expr state lhost (Cil.new_exp ~loc:e.eloc (Lval lv))
+	| BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) -> 
+	  if is_ptr_or_array_exp e1 then extend_from_addr state e1
+	  else begin
+	    assert (is_ptr_or_array_exp e2);
+	    extend_from_addr state e2
+	  end
+	| CastE(_, e) | Info(e, _) -> extend_from_addr state e
+	| _ -> state
+      in
+      let state = extend_from_addr state e in
       Dataflow.Done (Some (extend_to_expr state lhost e))
     | Call(result, f_exp, l, _) -> 
       (match f_exp.enode with
@@ -526,11 +541,15 @@ instrumentation.";
   end
 
 let must_model_vi ?kf ?stmt vi =
-  let kf = match kf, stmt with
+  let _kf = match kf, stmt with
     | None, None | Some _, _ -> kf
     | None, Some stmt -> Some (Kernel_function.find_englobing_kf stmt)
   in
-  match stmt, kf with
+  (* [JS 2013/05/07] that is unsound to take the env from the given stmt in
+     presence of aliasing with an address (see tests address.i).
+     TODO: could be optimized though *)
+  consolidated_must_model_vi vi
+(*  match stmt, kf with
   | None, _ -> consolidated_must_model_vi vi
   | Some _, None ->
     assert false
@@ -548,7 +567,7 @@ let must_model_vi ?kf ?stmt vi =
     with Not_found -> 
       (* [kf] is dead code *)
       false
-
+ *)
 let rec must_model_lval ?kf ?stmt = function
   | Var vi, _ -> must_model_vi ?kf ?stmt vi
   | Mem e, _ -> must_model_exp ?kf ?stmt e

src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i

@@ -4,8 +4,17 @@
    EXECNOW: LOG gen_addrOf2.c BIN gen_addrOf2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/addrOf.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_addrOf2.c > /dev/null && ./gcc_test.sh addrOf2
 */
 
+void f(){
+  int m, *u, *p;
+  u = &m;
+  p = u;
+  m = 123;
+  //@ assert \initialized(p);
+}
+
 int main(void) {
   int x = 0;
+  f();
   /*@ assert &x == &x; */ ;
   return 0;
 }

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle

@@ -14,13 +14,25 @@
   __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __memory_size ∈ [--..--]
-tests/e-acsl-runtime/addrOf.i:9:[value] Assertion got status valid.
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
+[value] using specification for function __initialized
+share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __delete_block
+tests/e-acsl-runtime/addrOf.i:18:[value] Assertion got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
+[value] Values at end of function f:
+  m ∈ {123}
+  u ∈ {{ &m }}
+  p ∈ {{ &m }}
 [value] Values at end of function main:
   x ∈ {0}
   __retres ∈ {0}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle

@@ -14,13 +14,25 @@
   __fc_rand_max ∈ {32767}
   __fc_heap_status ∈ [--..--]
   __memory_size ∈ [--..--]
-tests/e-acsl-runtime/addrOf.i:9:[value] Assertion got status valid.
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
+[value] using specification for function __initialized
+share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __delete_block
+tests/e-acsl-runtime/addrOf.i:18:[value] Assertion got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
+[value] Values at end of function f:
+  m ∈ {123}
+  u ∈ {{ &m }}
+  p ∈ {{ &m }}
 [value] Values at end of function main:
   x ∈ {0}
   __retres ∈ {0}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c

@@ -30,6 +30,24 @@ axiomatic
   
   }
  */
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+                                                            size_t size);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+    ensures
+      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
+    assigns \nothing;
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+                                                          size_t size);
+
 extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
 
 extern size_t __memory_size;
@@ -38,14 +56,42 @@ extern size_t __memory_size;
 predicate diffSize{L1, L2}(ℤ i) =
   \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
  */
+void f(void)
+{
+  int m;
+  int *u;
+  int *p;
+  __store_block((void *)(& p),4U);
+  __store_block((void *)(& u),4U);
+  __store_block((void *)(& m),4U);
+  __full_init((void *)(& u));
+  u = & m;
+  __full_init((void *)(& p));
+  p = u;
+  __full_init((void *)(& m));
+  m = 123;
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized;
+    __e_acsl_initialized = __initialized((void *)p,sizeof(int));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"f",
+                  (char *)"\\initialized(p)",12);
+  }
+  __delete_block((void *)(& p));
+  __delete_block((void *)(& u));
+  __delete_block((void *)(& m));
+  return;
+}
+
 int main(void)
 {
   int __retres;
   int x;
   x = 0;
+  f();
   /*@ assert &x ≡ &x; */
   e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
-                (char *)"&x == &x",9);
+                (char *)"&x == &x",18);
   __retres = 0;
   __clean();
   return __retres;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c

@@ -30,6 +30,24 @@ axiomatic
   
   }
  */
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+                                                            size_t size);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+    ensures
+      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
+    assigns \nothing;
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+                                                          size_t size);
+
 extern  __attribute__((__FC_BUILTIN__)) void __clean(void);
 
 extern size_t __memory_size;
@@ -38,14 +56,42 @@ extern size_t __memory_size;
 predicate diffSize{L1, L2}(ℤ i) =
   \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
  */
+void f(void)
+{
+  int m;
+  int *u;
+  int *p;
+  __store_block((void *)(& p),4U);
+  __store_block((void *)(& u),4U);
+  __store_block((void *)(& m),4U);
+  __full_init((void *)(& u));
+  u = & m;
+  __full_init((void *)(& p));
+  p = u;
+  __full_init((void *)(& m));
+  m = 123;
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized;
+    __e_acsl_initialized = __initialized((void *)p,sizeof(int));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"f",
+                  (char *)"\\initialized(p)",12);
+  }
+  __delete_block((void *)(& p));
+  __delete_block((void *)(& u));
+  __delete_block((void *)(& m));
+  return;
+}
+
 int main(void)
 {
   int __retres;
   int x;
   x = 0;
+  f();
   /*@ assert &x ≡ &x; */
   e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
-                (char *)"&x == &x",9);
+                (char *)"&x == &x",18);
   __retres = 0;
   __clean();
   return __retres;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c

@@ -64,6 +64,10 @@ extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+                                                          size_t size);
+
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 
@@ -138,7 +142,9 @@ struct list *add(struct list *l, int i)
     e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"add",
                   (char *)"\\valid(new)",20);
   }
+  __initialize((void *)(& new->element),sizeof(int));
   new->element = i;
+  __initialize((void *)(& new->next),sizeof(struct list *));
   new->next = l;
   __delete_block((void *)(& new));
   return new;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c

@@ -64,6 +64,10 @@ extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
+                                                          size_t size);
+
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
 
@@ -138,7 +142,9 @@ struct list *add(struct list *l, int i)
     e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"add",
                   (char *)"\\valid(new)",20);
   }
+  __initialize((void *)(& new->element),sizeof(int));
   new->element = i;
+  __initialize((void *)(& new->next),sizeof(struct list *));
   new->next = l;
   __delete_block((void *)(& new));
   return new;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c

@@ -148,6 +148,7 @@ int main(void)
   }
   __full_init((void *)(& p));
   p = & t[2];
+  __initialize((void *)(& t[2]),sizeof(int));
   t[2] = 5;
   /*@ assert *p ≡ 5; */
   {

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c

@@ -313,6 +313,7 @@ int main(void)
   }
   __full_init((void *)(& p));
   p = & t[2];
+  __initialize((void *)(& t[2]),sizeof(int));
   t[2] = 5;
   /*@ assert *p ≡ 5; */
   {

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle

@@ -34,6 +34,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __initialize
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] using specification for function __clean
 [value] done for function main

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle

@@ -34,6 +34,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __initialize
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] using specification for function __clean
 [value] done for function main