From e8045ac9dd03dba81abb476c4c10767ad5d873e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Virgile=20Pr=C3=A9vosto?= <virgile.prevosto@cea.fr>
Date: Tue, 30 Jul 2013 07:39:19 +0000
Subject: [PATCH] update oracles against changes in kernel+value
---
.../e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle | 2 +-
20 files changed, 28 insertions(+), 28 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index 633eebb1b80..2a4d0d22d42 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -41,7 +41,7 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
[value] ====== VALUES COMPUTED ======
[value] Values at end of function memchr:
i ∈ {0; 1; 2; 3; 4}
- s ∈ {{ "toto" + {0; 1} ; "toto" + [0..15] }}
+ s ∈ {{ "toto" + {0; 1} ; "toto" + [0..--] }}
__retres ∈ {{ NULL ; "toto" + {1} }}
[value] Values at end of function __e_acsl_memchr:
__retres ∈ {{ NULL ; "toto" + {1} }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index 121482b5954..985d45972db 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -71,7 +71,7 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
[value] ====== VALUES COMPUTED ======
[value] Values at end of function memchr:
i ∈ {0; 1; 2; 3; 4}
- s ∈ {{ "toto" + {0; 1} ; "toto" + [0..15] }}
+ s ∈ {{ "toto" + {0; 1} ; "toto" + [0..--] }}
__retres ∈ {{ NULL ; "toto" + {1} }}
[value] Values at end of function __e_acsl_memchr:
__retres ∈ {{ NULL ; "toto" + {1} }}
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 26fdbdf56a1..e448dafe1d0 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
@@ -40,7 +40,7 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
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:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' 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 __e_acsl_memory_clean, generating default assigns from the prototype
[value] using specification for function __e_acsl_memory_clean
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 2ae61370575..ff089a32e68 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
@@ -62,7 +62,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: po
share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:114:[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:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' 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 __e_acsl_memory_clean, generating default assigns from the prototype
[value] using specification for function __e_acsl_memory_clean
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 6a5b3db26ea..1080142ed78 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
@@ -65,7 +65,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -146,7 +146,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
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 81e2086b6cc..acea4fddfbd 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
@@ -65,7 +65,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -193,7 +193,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
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 24c1900f45f..000231885ae 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -139,7 +139,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
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 24c1900f45f..000231885ae 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -139,7 +139,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
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 9029158b5ae..e7016652779 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -143,7 +143,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
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 b3a6ea3eefb..53c782d1394 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -159,7 +159,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
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
index 30361464f2f..2705a2df7ac 100644
--- 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -136,7 +136,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
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
index f2a1b12677d..569d289872a 100644
--- 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
@@ -156,7 +156,7 @@ void *__e_acsl_malloc(size_t size)
behavior deallocation:
assumes p ≢ \null;
- requires \freeable(p);
+ requires freeable: \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index 98c9c6605c9..e1dd3b1281f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -31,5 +31,5 @@ tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
- x ∈ [--..--]
+ x ∈ [0..2147483647]
__retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
index 9c7cd1c0da7..61bdef82340 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
@@ -22,5 +22,5 @@ tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
- x ∈ [--..--]
+ x ∈ [0..2147483647]
__retres ∈ {0}
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 a611a506443..a283dc7d548 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
@@ -75,7 +75,7 @@ tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
[value] using specification for function __valid_read
tests/e-acsl-runtime/valid.c:47:[value] Assertion 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:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
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 a611a506443..a283dc7d548 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
@@ -75,7 +75,7 @@ tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
[value] using specification for function __valid_read
tests/e-acsl-runtime/valid.c:47:[value] Assertion 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:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses; assert(\defined(&a))
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 56f011916a1..948d6ce7ca8 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
@@ -52,7 +52,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: po
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
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.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
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))
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 6bbb1e532ed..23e4a547c91 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
@@ -60,7 +60,7 @@ share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got stat
share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:114:[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:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
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))
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
index 3a62b0c363a..6f80ef172d8 100644
--- 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
@@ -43,7 +43,7 @@ tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[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:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' 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 __e_acsl_memory_clean, generating default assigns from the prototype
[value] using specification for function __e_acsl_memory_clean
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
index d1cf5ba1df8..2ef572ab807 100644
--- 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
@@ -52,7 +52,7 @@ share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got stat
share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
share/e-acsl/e_acsl_gmp.h:114:[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:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' 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 __e_acsl_memory_clean, generating default assigns from the prototype
[value] using specification for function __e_acsl_memory_clean
--
GitLab