From a13c858f467196ba952fe985755c3cf6eeed6228 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 25 Apr 2013 19:35:27 +0000
Subject: [PATCH] [E-ACSL] dataflow: fixed bug with function call when the
returned value must be monitored
---
src/plugins/e-acsl/TODO | 3 +
src/plugins/e-acsl/pre_analysis.ml | 17 +-
.../e-acsl-runtime/oracle/at.1.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/at.res.oracle | 2 +-
.../oracle/bts1399.1.res.oracle | 2 +-
.../e-acsl-runtime/oracle/bts1399.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/gen_at.c | 7 +
.../tests/e-acsl-runtime/oracle/gen_at2.c | 7 +
.../tests/e-acsl-runtime/oracle/gen_bts1390.c | 8 +
.../e-acsl-runtime/oracle/gen_bts13902.c | 8 +
.../tests/e-acsl-runtime/oracle/gen_bts1399.c | 4 +
.../e-acsl-runtime/oracle/gen_bts13992.c | 4 +
.../e-acsl-runtime/oracle/gen_localvar.c | 4 +
.../e-acsl-runtime/oracle/gen_localvar2.c | 4 +
.../e-acsl-runtime/oracle/gen_ptr_init.c | 4 +
.../e-acsl-runtime/oracle/gen_ptr_init2.c | 4 +
.../tests/e-acsl-runtime/oracle/gen_valid.c | 5 +
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 5 +
.../e-acsl-runtime/oracle/gen_valid_alias.c | 4 +
.../e-acsl-runtime/oracle/gen_valid_alias2.c | 4 +
.../tests/e-acsl-runtime/oracle/gen_vector.c | 229 +++++++++++++++
.../tests/e-acsl-runtime/oracle/gen_vector2.c | 261 ++++++++++++++++++
.../oracle/localvar.1.res.oracle | 2 +-
.../e-acsl-runtime/oracle/localvar.res.oracle | 2 +-
.../oracle/ptr_init.1.res.oracle | 2 +-
.../e-acsl-runtime/oracle/ptr_init.res.oracle | 2 +-
.../e-acsl-runtime/oracle/valid.1.res.oracle | 6 +-
.../e-acsl-runtime/oracle/valid.res.oracle | 6 +-
.../oracle/valid_alias.1.res.oracle | 6 +-
.../oracle/valid_alias.res.oracle | 6 +-
.../e-acsl-runtime/oracle/vector.1.err.oracle | 0
.../e-acsl-runtime/oracle/vector.1.res.oracle | 70 +++++
.../e-acsl-runtime/oracle/vector.err.oracle | 0
.../e-acsl-runtime/oracle/vector.res.oracle | 79 ++++++
.../e-acsl/tests/e-acsl-runtime/vector.c | 32 +++
src/plugins/e-acsl/visit.ml | 4 +-
36 files changed, 782 insertions(+), 25 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 723b7598160..c7d62398e69 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -55,12 +55,15 @@
- \valid (or other memory-model constructs) in ensures of functions without code
- function pointers
(in case of the pointing function has a behavior like in test ptr_init.c)
+- ne pas remplacer tous les appels à malloc/free par des
+ __e_acsl_malloc/__eacsl_free. Ne le faire uniquement pour ceux monitorer.
#######
# DOC #
#######
- write user manual
+- update according to the latest version of ACSL
#########
# TESTS #
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index b0e13ff81d6..2519fb0064d 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -318,7 +318,7 @@ module rec Transfer
in
Some state)
- let rec base_addr e = match e.enode with
+ let rec base_addr_node = function
| Lval lv | AddrOf lv | StartOf lv ->
(match lv with
| Var vi, _ -> Some vi
@@ -337,6 +337,8 @@ module rec Transfer
| AlignOfE _ ->
None
+ and base_addr e = base_addr_node e.enode
+
(** The (backwards) transfer function for an instruction. The
[(Cil.CurrentLoc.get ())] is set before calling this. If it returns
None, then we have some default handling. Otherwise, the returned data is
@@ -376,13 +378,22 @@ module rec Transfer
(fun acc p a -> match base_addr a with
| None -> acc
| Some vi ->
- if Varinfo.Set.mem vi state
- then Varinfo.Set.add p acc
+ if Varinfo.Set.mem vi state then Varinfo.Set.add p acc
else acc)
state
params
l
in
+ let init = match result with
+ | None -> init
+ | Some lv ->
+ match base_addr_node (Lval lv) with
+ | None -> init
+ | Some vi ->
+ if Varinfo.Set.mem vi state
+ then Varinfo.Set.add (Misc.result_vi kf) init
+ else init
+ in
let state = Compute.get ~init kf in
(* compute the resulting state by keeping arguments whenever the
corresponding formals must be kept *)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index 9ad3ada267a..6eb5c8cef36 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -17,6 +17,7 @@
A ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
+[value] using specification for function __delete_block
tests/e-acsl-runtime/at.i:40:[value] Function h: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
@@ -61,7 +62,6 @@ tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, \at() on a C lab
tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown.
tests/e-acsl-runtime/at.i:34:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
-[value] using specification for function __delete_block
[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/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index cb483122ae0..1a3ae9e6a50 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -17,6 +17,7 @@
A ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
+[value] using specification for function __delete_block
tests/e-acsl-runtime/at.i:40:[value] Function h: 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 valid.
@@ -42,7 +43,6 @@ tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, \at() on a C lab
tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown.
:0:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
-[value] using specification for function __delete_block
[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/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index 63e1e86ff01..dc39920f806 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
@@ -28,6 +28,7 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\allocate'
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
@@ -41,7 +42,6 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-[value] using specification for function __delete_block
[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/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 7596ab57dd6..2f4606d2f20 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -29,6 +29,7 @@ tests/e-acsl-runtime/bts1399.c:24:[e-acsl] warning: missing guard for ensuring t
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
@@ -63,7 +64,6 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-[value] using specification for function __delete_block
[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/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index 9fb7ca4b2d2..acbb22b8db2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -167,6 +167,8 @@ void g(int *p, int *q)
/*@ ensures \result ≡ \old(x); */
int h(int x)
{
+ __store_block((void *)(& x),4U);
+ __delete_block((void *)(& x));
return x;
}
@@ -175,10 +177,15 @@ int __e_acsl_h(int x)
{
int __e_acsl_at;
int __retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& x),4U);
+ __store_block((void *)(& __e_acsl_at),4U);
__e_acsl_at = x;
__retres = h(x);
e_acsl_assert(__retres == __e_acsl_at,(char *)"Postcondition",(char *)"h",
(char *)"\\result == \\old(x)",40);
+ __delete_block((void *)(& x));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index 50d46822a02..ef1d71ea6fb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
@@ -284,6 +284,8 @@ void g(int *p, int *q)
/*@ ensures \result ≡ \old(x); */
int h(int x)
{
+ __store_block((void *)(& x),4U);
+ __delete_block((void *)(& x));
return x;
}
@@ -292,6 +294,9 @@ int __e_acsl_h(int x)
{
int __e_acsl_at;
int __retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& x),4U);
+ __store_block((void *)(& __e_acsl_at),4U);
__e_acsl_at = x;
__retres = h(x);
{
@@ -304,8 +309,10 @@ int __e_acsl_h(int x)
(__mpz_struct const *)(__e_acsl));
e_acsl_assert(__e_acsl_eq == 0,(char *)"Postcondition",(char *)"h",
(char *)"\\result == \\old(x)",40);
+ __delete_block((void *)(& x));
__gmpz_clear(__e_acsl_result);
__gmpz_clear(__e_acsl);
+ __delete_block((void *)(& __retres));
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index 4dba459bf13..b627514fc2b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -74,20 +74,28 @@ void *memchr(void const *buf, int c, size_t n)
void *__retres;
int i;
char *s;
+ __store_block((void *)(& s),4U);
+ __store_block((void *)(& __retres),4U);
__store_block((void *)(& buf),4U);
+ __full_init((void *)(& s));
s = (char *)buf;
i = 0;
while ((size_t)i < n) {
if ((int)*s == c) {
+ __full_init((void *)(& __retres));
__retres = (void *)s;
goto return_label;
}
+ __full_init((void *)(& s));
s ++;
i ++;
}
+ __full_init((void *)(& __retres));
__retres = (void *)0;
return_label: /* internal */
__delete_block((void *)(& buf));
+ __delete_block((void *)(& s));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index 42e5579def6..94bb2b9325d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -129,20 +129,28 @@ void *memchr(void const *buf, int c, size_t n)
void *__retres;
int i;
char *s;
+ __store_block((void *)(& s),4U);
+ __store_block((void *)(& __retres),4U);
__store_block((void *)(& buf),4U);
+ __full_init((void *)(& s));
s = (char *)buf;
i = 0;
while ((size_t)i < n) {
if ((int)*s == c) {
+ __full_init((void *)(& __retres));
__retres = (void *)s;
goto return_label;
}
+ __full_init((void *)(& s));
s ++;
i ++;
}
+ __full_init((void *)(& __retres));
__retres = (void *)0;
return_label: /* internal */
__delete_block((void *)(& buf));
+ __delete_block((void *)(& s));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index 8590eef9867..c272c755172 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -134,7 +134,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 4a663720ce8..92292d85014 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -181,7 +181,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
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 2055aa4fcae..9908ad514ec 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
@@ -106,7 +106,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
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 2055aa4fcae..9908ad514ec 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
@@ -106,7 +106,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index a31cc8a9cd6..8f6be093616 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -99,7 +99,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index a31cc8a9cd6..8f6be093616 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -99,7 +99,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 3e41d532718..81f667be94f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -123,7 +123,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
@@ -184,6 +188,7 @@ int *f(int *x)
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"f",
(char *)"!\\valid(y)",19);
}
+ __full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 3e41d532718..81f667be94f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -123,7 +123,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
@@ -184,6 +188,7 @@ int *f(int *x)
e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"f",
(char *)"!\\valid(y)",19);
}
+ __full_init((void *)(& y));
y = x;
/*@ assert \valid(x); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index cc6a94742a4..c2f4f1fbc07 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -131,7 +131,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 8ff7080af77..6365593033b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -147,7 +147,11 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
__retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
new file mode 100644
index 00000000000..2b9123b2a6a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -0,0 +1,229 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@
+model __mpz_struct { ℤ n };
+*/
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+extern int __fc_heap_status;
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+extern void *__malloc(size_t size);
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+extern void __free(void *p);
+
+/*@ 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 __initialize(void *ptr,
+ size_t size);
+
+/*@ 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;
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
+ __retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+void __e_acsl_free(void *p)
+{
+ int __e_acsl_at;
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ return;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+int LAST;
+int *new_inversed(int len, int *v)
+{
+ int i;
+ int *p;
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& v),4U);
+ __full_init((void *)(& p));
+ p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned int)len);
+ i = 0;
+ while (i < len) {
+ __initialize((void *)(p + i),sizeof(int));
+ *(p + i) = *(v + ((len - i) - 1));
+ i ++;
+ }
+ __delete_block((void *)(& v));
+ __delete_block((void *)(& p));
+ return p;
+}
+
+int main(void)
+{
+ int __retres;
+ int v1[3];
+ int *v2;
+ __store_block((void *)(& v2),4U);
+ __store_block((void *)(v1),12U);
+ __initialize((void *)(v1),sizeof(int));
+ v1[0] = 1;
+ __initialize((void *)(& v1[1]),sizeof(int));
+ v1[1] = 2;
+ __initialize((void *)(& v1[2]),sizeof(int));
+ v1[2] = 3;
+ LAST = v1[2];
+ /*@ assert \initialized(&v1[2]); */
+ {
+ int __e_acsl_initialized;
+ __e_acsl_initialized = __initialized((void *)(& v1[2]),sizeof(int));
+ e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+ (char *)"\\initialized(&v1[2])",25);
+ }
+ __full_init((void *)(& v2));
+ v2 = new_inversed(3,v1);
+ LAST = *(v2 + 2);
+ /*@ assert \initialized(v2+2); */
+ {
+ int __e_acsl_initialized_2;
+ __e_acsl_initialized_2 = __initialized((void *)(v2 + 2),sizeof(int));
+ e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\initialized(v2+2)",28);
+ }
+ /*@ assert LAST ≡ 1; */
+ e_acsl_assert(LAST == 1,(char *)"Assertion",(char *)"main",
+ (char *)"LAST == 1",29);
+ __e_acsl_free((void *)v2);
+ __retres = 0;
+ __delete_block((void *)(& v2));
+ __delete_block((void *)(v1));
+ __clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
new file mode 100644
index 00000000000..abb78f1e956
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -0,0 +1,261 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@
+model __mpz_struct { ℤ n };
+*/
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+
+/*@ requires \valid(x);
+ assigns *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+extern int __fc_heap_status;
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+extern void *__malloc(size_t size);
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+extern void __free(void *p);
+
+/*@ 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 __initialize(void *ptr,
+ size_t size);
+
+/*@ 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;
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
+ behavior allocation:
+ assumes is_allocable(size);
+ ensures \fresh{Old, Here}(\result,\old(size));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+
+ behavior no_allocation:
+ assumes ¬is_allocable(size);
+ ensures \result ≡ \null;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void *__e_acsl_malloc(size_t size)
+{
+ void *__retres;
+ __store_block((void *)(& __retres),4U);
+ __store_block((void *)(& size),4U);
+ __retres = __malloc(size);
+ __delete_block((void *)(& size));
+ __delete_block((void *)(& __retres));
+ return __retres;
+}
+
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
+
+ behavior deallocation:
+ assumes p ≢ \null;
+ requires \freeable(p);
+ ensures \allocable(\old(p));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+
+ behavior no_deallocation:
+ assumes p ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_deallocation, deallocation;
+ disjoint behaviors no_deallocation, deallocation;
+ */
+void __e_acsl_free(void *p)
+{
+ int __e_acsl_at;
+ __e_acsl_at = p != (void *)0;
+ __free(p);
+ return;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+
+*/
+int LAST;
+int *new_inversed(int len, int *v)
+{
+ int i;
+ int *p;
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& v),4U);
+ __full_init((void *)(& p));
+ p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned int)len);
+ i = 0;
+ while (i < len) {
+ __initialize((void *)(p + i),sizeof(int));
+ *(p + i) = *(v + ((len - i) - 1));
+ i ++;
+ }
+ __delete_block((void *)(& v));
+ __delete_block((void *)(& p));
+ return p;
+}
+
+int main(void)
+{
+ int __retres;
+ int v1[3];
+ int *v2;
+ __store_block((void *)(& v2),4U);
+ __store_block((void *)(v1),12U);
+ __initialize((void *)(v1),sizeof(int));
+ v1[0] = 1;
+ __initialize((void *)(& v1[1]),sizeof(int));
+ v1[1] = 2;
+ __initialize((void *)(& v1[2]),sizeof(int));
+ v1[2] = 3;
+ LAST = v1[2];
+ /*@ assert \initialized(&v1[2]); */
+ {
+ int __e_acsl_initialized;
+ __e_acsl_initialized = __initialized((void *)(& v1[2]),sizeof(int));
+ e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+ (char *)"\\initialized(&v1[2])",25);
+ }
+ __full_init((void *)(& v2));
+ v2 = new_inversed(3,v1);
+ LAST = *(v2 + 2);
+ /*@ assert \initialized(v2+2); */
+ {
+ int __e_acsl_initialized_2;
+ __e_acsl_initialized_2 = __initialized((void *)(v2 + (long)2),
+ sizeof(int));
+ e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\initialized(v2+2)",28);
+ }
+ /*@ assert LAST ≡ 1; */
+ {
+ mpz_t __e_acsl_LAST;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl_LAST,(long)LAST);
+ __gmpz_init_set_si(__e_acsl,(long)1);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_LAST),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"LAST == 1",29);
+ __gmpz_clear(__e_acsl_LAST);
+ __gmpz_clear(__e_acsl);
+ }
+ __e_acsl_free((void *)v2);
+ __retres = 0;
+ __delete_block((void *)(& v2));
+ __delete_block((void *)(v1));
+ __clean();
+ return __retres;
+}
+
+
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 c2614d571b0..caa274be3c9 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
@@ -24,6 +24,7 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
@@ -33,7 +34,6 @@ 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 __delete_block
[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 c2614d571b0..caa274be3c9 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
@@ -24,6 +24,7 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
@@ -33,7 +34,6 @@ 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 __delete_block
[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/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 565340036bf..d7bfa1f6e03 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -28,6 +28,7 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
[value] using specification for function __malloc
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __full_init
@@ -40,7 +41,6 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: pos
share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
-[value] using specification for function __delete_block
[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/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 565340036bf..d7bfa1f6e03 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -28,6 +28,7 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
[value] using specification for function __malloc
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __full_init
@@ -40,7 +41,6 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: pos
share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
-[value] using specification for function __delete_block
[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/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index a02305847c1..8a2718b7566 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -44,6 +44,7 @@ tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function
[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 __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
@@ -66,7 +67,6 @@ tests/e-acsl-runtime/valid.c:19:[value] all evaluations are invalid for function
(void *)y
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
-[value] using specification for function __delete_block
tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.
@@ -82,11 +82,11 @@ tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function
[value] using specification for function __clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_free:
+ __fc_heap_status ∈ [--..--]
[value] Values at end of function __e_acsl_malloc:
__fc_heap_status ∈ [--..--]
__retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
[value] Values at end of function e_acsl_global_init:
[value] Values at end of function f:
y ∈ {{ &n }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index a02305847c1..8a2718b7566 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -44,6 +44,7 @@ tests/e-acsl-runtime/valid.c:27:[value] all evaluations are invalid for function
[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 __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/valid.c:29:[value] Assertion got status valid.
@@ -66,7 +67,6 @@ tests/e-acsl-runtime/valid.c:19:[value] all evaluations are invalid for function
(void *)y
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
-[value] using specification for function __delete_block
tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
tests/e-acsl-runtime/valid.c:33:[value] Assertion got status valid.
@@ -82,11 +82,11 @@ tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function
[value] using specification for function __clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_free:
+ __fc_heap_status ∈ [--..--]
[value] Values at end of function __e_acsl_malloc:
__fc_heap_status ∈ [--..--]
__retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
[value] Values at end of function e_acsl_global_init:
[value] Values at end of function f:
y ∈ {{ &n }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 00ec6bbb803..fa36eac9c68 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -42,6 +42,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
(void *)b
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
@@ -52,7 +53,6 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
[value] using specification for function __valid_read
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
-[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
@@ -67,11 +67,11 @@ tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for fu
[value] using specification for function __clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_free:
+ __fc_heap_status ∈ [--..--]
[value] Values at end of function __e_acsl_malloc:
__fc_heap_status ∈ [--..--]
__retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
[value] Values at end of function main:
__fc_heap_status ∈ [--..--]
a ∈ ESCAPINGADDR
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index a7b0d3f91dc..8dda7f0f775 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -42,6 +42,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
(void *)b
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
@@ -60,7 +61,6 @@ share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got stat
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
-[value] using specification for function __delete_block
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
@@ -75,11 +75,11 @@ tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for fu
[value] using specification for function __clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_free:
+ __fc_heap_status ∈ [--..--]
[value] Values at end of function __e_acsl_malloc:
__fc_heap_status ∈ [--..--]
__retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
[value] Values at end of function main:
__fc_heap_status ∈ [--..--]
a ∈ ESCAPINGADDR
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
new file mode 100644
index 00000000000..4cbe715e4e6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -0,0 +1,70 @@
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/vector.c"
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __memory_size ∈ [--..--]
+ LAST ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __initialize
+tests/e-acsl-runtime/vector.c:25:[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 __full_init
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
+tests/e-acsl-runtime/vector.c:28:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+[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 __e_acsl_free:
+ __fc_heap_status ∈ [--..--]
+[value] Values at end of function __e_acsl_malloc:
+ __fc_heap_status ∈ [--..--]
+ __retres ∈ {{ &Frama_C_alloc }}
+[value] Values at end of function new_inversed:
+ __fc_heap_status ∈ [--..--]
+ i ∈ {3}
+ p ∈ {{ &Frama_C_alloc }}
+ Frama_C_alloc[bits 0 to 95]# ∈ {1; 2; 3} or UNINITIALIZED repeated %32
+[value] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ LAST ∈ {1; 2; 3} or UNINITIALIZED
+ v1[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ v2 ∈ ESCAPINGADDR
+ __retres ∈ {0}
+ Frama_C_alloc[0..11] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
new file mode 100644
index 00000000000..1d5f127b3f4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -0,0 +1,79 @@
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -Ishare/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/vector.c"
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __memory_size ∈ [--..--]
+ LAST ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __initialize
+tests/e-acsl-runtime/vector.c:25:[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 __full_init
+[value] using specification for function __delete_block
+FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
+tests/e-acsl-runtime/vector.c:28:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+[value] using specification for function __gmpz_init_set_si
+share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
+share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
+share/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: postcondition got status unknown.
+[value] using specification for function __gmpz_cmp
+share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
+share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
+[value] using specification for function __gmpz_clear
+share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+[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 __e_acsl_free:
+ __fc_heap_status ∈ [--..--]
+[value] Values at end of function __e_acsl_malloc:
+ __fc_heap_status ∈ [--..--]
+ __retres ∈ {{ &Frama_C_alloc }}
+[value] Values at end of function new_inversed:
+ __fc_heap_status ∈ [--..--]
+ i ∈ {3}
+ p ∈ {{ &Frama_C_alloc }}
+ Frama_C_alloc[bits 0 to 95]# ∈ {1; 2; 3} or UNINITIALIZED repeated %32
+[value] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ LAST ∈ {1; 2; 3} or UNINITIALIZED
+ v1[0] ∈ {1}
+ [1] ∈ {2}
+ [2] ∈ {3}
+ v2 ∈ ESCAPINGADDR
+ __retres ∈ {0}
+ Frama_C_alloc[0..11] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
new file mode 100644
index 00000000000..a2870eb277c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
@@ -0,0 +1,32 @@
+/* run.config
+ COMMENT: function call + initialized
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
+ EXECNOW: LOG gen_vector.c BIN gen_vector.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/vector.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_vector.c > /dev/null && ./gcc_test.sh vector
+ EXECNOW: LOG gen_vector2.c BIN gen_vector2.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/vector.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_vector2.c > /dev/null && ./gcc_test.sh vector2
+*/
+
+#include<stdlib.h>
+
+int LAST;
+
+int* new_inversed(int len, int *v) {
+ int i, *p;
+ // @ assert \valid(v) && \offset(v)+len*sizeof(int) <= \block_length(v);
+ p = malloc(sizeof(int)*len);
+ for(i=0; i<len; i++)
+ p[i] = v[len-i-1];
+ return p;
+}
+
+int main(void) {
+ int v1[3]= { 1, 2, 3}, *v2;
+ // @ assert \valid(&v1[2]);
+ LAST = v1[2];
+ //@ assert \initialized(v1+2);
+ v2 = new_inversed(3, v1);
+ LAST = v2[2];
+ //@ assert \initialized(v2+2);
+ //@ assert LAST == 1;
+ free(v2);
+ return 0;
+}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 31288e58c16..1434b01c5d2 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -401,7 +401,7 @@ you must call function `%s' by yourself"
e, !env_ref
method vstmt_aux stmt =
- Options.debug ~level:3 "proceeding stmt (sid %d) %a@."
+ Options.debug ~level:4 "proceeding stmt (sid %d) %a@."
stmt.sid Stmt.pretty stmt;
let kf = Extlib.the self#current_kf in
let is_main = self#is_main kf in
@@ -544,7 +544,7 @@ you must call function `%s' by yourself"
mk_block post_block, env
in
function_env := env;
- Options.debug ~level:3
+ Options.debug ~level:4
"@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt;
new_stmt
in
--
GitLab