From bfb9f650f030fe8dfffa09683dd821b40a586c19 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 7 May 2013 13:24:32 +0000
Subject: [PATCH] [E-ACSL] analysis: fixed bug in presence of an alias with an
explicit address
---
.../e-acsl/known_bugs/taking_address.i | 7 ---
src/plugins/e-acsl/pre_analysis.ml | 27 +++++++++--
.../e-acsl/tests/e-acsl-runtime/addrOf.i | 9 ++++
.../e-acsl-runtime/oracle/addrOf.1.res.oracle | 14 +++++-
.../e-acsl-runtime/oracle/addrOf.res.oracle | 14 +++++-
.../tests/e-acsl-runtime/oracle/gen_addrOf.c | 48 ++++++++++++++++++-
.../tests/e-acsl-runtime/oracle/gen_addrOf2.c | 48 ++++++++++++++++++-
.../e-acsl-runtime/oracle/gen_localvar.c | 6 +++
.../e-acsl-runtime/oracle/gen_localvar2.c | 6 +++
.../tests/e-acsl-runtime/oracle/gen_ptr.c | 1 +
.../tests/e-acsl-runtime/oracle/gen_ptr2.c | 1 +
.../oracle/localvar.1.res.oracle | 1 +
.../e-acsl-runtime/oracle/localvar.res.oracle | 1 +
13 files changed, 168 insertions(+), 15 deletions(-)
delete mode 100644 src/plugins/e-acsl/known_bugs/taking_address.i
diff --git a/src/plugins/e-acsl/known_bugs/taking_address.i b/src/plugins/e-acsl/known_bugs/taking_address.i
deleted file mode 100644
index 4122f697546..00000000000
--- a/src/plugins/e-acsl/known_bugs/taking_address.i
+++ /dev/null
@@ -1,7 +0,0 @@
-int main(){
- int m, *u, *p;
- u = &m;
- p = u;
- m = 123;
- //@ assert \initialized(p);
-}
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index f2b9c3db37f..68594cbad3b 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i b/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
index 60fd3c341f8..8436ac41c09 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/addrOf.i
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index 710876048c4..28d84b4bdc5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/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}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index 710876048c4..28d84b4bdc5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/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}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index 831b7db83a0..eb348beab5c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
index 831b7db83a0..eb348beab5c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 3e5483cb4c3..61a4f0a1f7f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 3e5483cb4c3..61a4f0a1f7f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index 176208d82ad..2e767773d5d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/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; */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index c97a4938d67..126ae683f42 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
+++ b/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; */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 2aca7b0bf65..2a590db1377 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index 2aca7b0bf65..2a590db1377 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/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
--
GitLab