From a756e6d8229752d1e9d6425992b37c09e62a2d5a Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 27 Mar 2014 08:51:11 +0100
Subject: [PATCH] [tests] fix oracles
---
.../e-acsl-runtime/oracle/bts1307.1.res.oracle | 13 +++++++++++--
.../e-acsl-runtime/oracle/bts1307.res.oracle | 9 +++++++--
.../e-acsl-runtime/oracle/bts1399.1.res.oracle | 16 +++++++++++++---
.../e-acsl-runtime/oracle/bts1399.res.oracle | 6 ++++--
.../e-acsl-runtime/oracle/call.1.res.oracle | 6 +++++-
.../e-acsl-runtime/oracle/localvar.1.res.oracle | 6 +++++-
.../e-acsl-runtime/oracle/ptr_init.1.res.oracle | 6 +++++-
.../e-acsl-runtime/oracle/valid.1.res.oracle | 16 +++++++++++++---
.../tests/e-acsl-runtime/oracle/valid.res.oracle | 6 ++++--
.../oracle/valid_alias.1.res.oracle | 16 +++++++++++++---
.../e-acsl-runtime/oracle/valid_alias.res.oracle | 6 ++++--
.../e-acsl-runtime/oracle/vector.1.res.oracle | 16 +++++++++++++---
.../e-acsl-runtime/oracle/vector.res.oracle | 6 ++++--
13 files changed, 101 insertions(+), 27 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index dbac98aa3b3..4e035d9a764 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -6,8 +6,17 @@
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index d731b1b8de1..e67c07e6cc1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -6,8 +6,13 @@
[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
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 d85b2df5421..4eb0732f08e 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint b
Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
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 06b169791c4..559617682a2 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
@@ -17,8 +17,10 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns cl
Ignoring annotation.
tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 5d253de0e95..637bbe76910 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -13,7 +13,11 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `disjoint beha
Ignoring annotation.
tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
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 0c526698fa8..30e78595460 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
@@ -13,7 +13,11 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `disjoint
Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at 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 329eb373e48..b1f418a638d 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
@@ -13,7 +13,11 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint
Ignoring annotation.
tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at 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 19712b1068e..8a86bcbbb7c 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `disjoint beh
Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
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 19712b1068e..5bd8feeb868 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
@@ -17,8 +17,10 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clau
Ignoring annotation.
tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
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 6e31a395467..53dc62141a3 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `disjoi
Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
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 ddf93884ad6..9c16ed4acb6 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
@@ -17,8 +17,10 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assign
Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
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 9b558f7f59e..8709e2eece6 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `disjoint be
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.
+FRAMAC_SHARE/libc/stdlib.h:144:[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.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
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 8c9800244d1..35d750d9442 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
@@ -17,8 +17,10 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns cla
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.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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
--
GitLab