From 3e0535e46f582de841a707b4ecaba50c292015f2 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 19 Apr 2013 07:06:45 +0000
Subject: [PATCH] [E-ACSL] do not monitor anymore memory locations involved in
constructs not yet supported like \freeable
---
src/plugins/e-acsl/pre_analysis.ml | 6 +++---
.../e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c | 6 ------
.../tests/e-acsl-runtime/oracle/gen_localvar2.c | 6 ------
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c | 11 -----------
.../e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c | 11 -----------
.../tests/e-acsl-runtime/oracle/gen_valid_alias.c | 11 -----------
.../tests/e-acsl-runtime/oracle/gen_valid_alias2.c | 11 -----------
.../tests/e-acsl-runtime/oracle/localvar.1.res.oracle | 3 ++-
.../tests/e-acsl-runtime/oracle/localvar.res.oracle | 3 ++-
.../tests/e-acsl-runtime/oracle/valid.1.res.oracle | 4 +++-
.../tests/e-acsl-runtime/oracle/valid.res.oracle | 4 +++-
.../e-acsl-runtime/oracle/valid_alias.1.res.oracle | 4 +++-
.../e-acsl-runtime/oracle/valid_alias.res.oracle | 4 +++-
13 files changed, 19 insertions(+), 65 deletions(-)
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 62ead90ba0d..15f5e1afbc6 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -197,12 +197,12 @@ module rec Transfer
let register_object kf state_ref = object
inherit Visitor.frama_c_inplace
method vpredicate = function
- | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t)
- | Pallocable(_, t) | Pfreeable(_, t) | Pfresh(_, _, t, _) ->
+ | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t) ->
(* Options.feedback "REGISTER %a" Cil.d_term t;*)
state_ref := register_term kf !state_ref t;
Cil.SkipChildren
- | Pseparated _ -> Error.not_yet "\\separated"
+ | Pallocable _ | Pfreeable _ | Pfresh _ | Pseparated _ ->
+ Error.not_yet "\\separated"
| Ptrue | Pfalse | Papp _ | Prel _
| Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
| Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
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 c0e4a2236dc..e7008617266 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,13 +106,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
- __full_init((void *)(& size));
- __full_init((void *)(& __retres));
__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 c0e4a2236dc..e7008617266 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,13 +106,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
- __full_init((void *)(& size));
- __full_init((void *)(& __retres));
__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 a0e70b6a201..c70a5764fbc 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,13 +123,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
- __full_init((void *)(& size));
- __full_init((void *)(& __retres));
__retres = __malloc(size);
- __delete_block((void *)(& size));
- __delete_block((void *)(& __retres));
return __retres;
}
@@ -155,13 +149,8 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
- __full_init((void *)(& p));
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
__e_acsl_at = p != (void *)0;
__free(p);
- __delete_block((void *)(& p));
return;
}
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 a0e70b6a201..c70a5764fbc 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,13 +123,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
- __full_init((void *)(& size));
- __full_init((void *)(& __retres));
__retres = __malloc(size);
- __delete_block((void *)(& size));
- __delete_block((void *)(& __retres));
return __retres;
}
@@ -155,13 +149,8 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
- __full_init((void *)(& p));
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
__e_acsl_at = p != (void *)0;
__free(p);
- __delete_block((void *)(& p));
return;
}
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 38faaee0ab1..24e4989e046 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,13 +131,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
- __full_init((void *)(& size));
- __full_init((void *)(& __retres));
__retres = __malloc(size);
- __delete_block((void *)(& size));
- __delete_block((void *)(& __retres));
return __retres;
}
@@ -163,13 +157,8 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
- __full_init((void *)(& p));
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
__e_acsl_at = p != (void *)0;
__free(p);
- __delete_block((void *)(& p));
return;
}
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 7eee2538328..a30b844cdf0 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,13 +147,7 @@ extern size_t __memory_size;
void *__e_acsl_malloc(size_t size)
{
void *__retres;
- __store_block((void *)(& __retres),4U);
- __store_block((void *)(& size),4U);
- __full_init((void *)(& size));
- __full_init((void *)(& __retres));
__retres = __malloc(size);
- __delete_block((void *)(& size));
- __delete_block((void *)(& __retres));
return __retres;
}
@@ -179,13 +173,8 @@ void *__e_acsl_malloc(size_t size)
void __e_acsl_free(void *p)
{
int __e_acsl_at;
- __store_block((void *)(& p),4U);
- __full_init((void *)(& p));
- __store_block((void *)(& __e_acsl_at),4U);
- __full_init((void *)(& __e_acsl_at));
__e_acsl_at = p != (void *)0;
__free(p);
- __delete_block((void *)(& p));
return;
}
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 b17d517d4bd..fc472694b93 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
@@ -5,6 +5,7 @@
[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/localvar.c"
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -21,7 +22,6 @@ 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.
@@ -31,6 +31,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __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 b17d517d4bd..fc472694b93 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
@@ -5,6 +5,7 @@
[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/localvar.c"
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -21,7 +22,6 @@ 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.
@@ -31,6 +31,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: pos
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __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 9aa29eb4fc9..2c35495b377 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
@@ -5,6 +5,8 @@
[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/valid.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -39,7 +41,6 @@ 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.
@@ -62,6 +63,7 @@ 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.
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 9aa29eb4fc9..2c35495b377 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
@@ -5,6 +5,8 @@
[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/valid.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -39,7 +41,6 @@ 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.
@@ -62,6 +63,7 @@ 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.
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 fb5483dc3c1..15a9312057f 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
@@ -5,6 +5,8 @@
[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/valid_alias.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -37,7 +39,6 @@ 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
@@ -58,6 +59,7 @@ tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value tha
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
(void *)b
+[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_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 58e7ac14f2b..28f2de34d0c 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
@@ -5,6 +5,8 @@
[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/valid_alias.c"
+FRAMAC_SHARE/libc/stdlib.h:152:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:136:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behavior' is not yet supported.
Ignoring annotation.
tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -37,7 +39,6 @@ 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
@@ -66,6 +67,7 @@ tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value tha
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: completely indeterminate value in b.
tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for function call argument
(void *)b
+[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
--
GitLab