From 860fd6a88ace82f50235240f2c54e531c08af6da Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 26 Nov 2012 09:06:59 +0000
Subject: [PATCH] [E-ACSL] update according to kernel's change. Still remain to
fix GP's invalid commit r20854
---
src/plugins/e-acsl/pre_analysis.ml | 4 +---
.../e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle | 3 +--
.../e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle | 3 +--
.../tests/e-acsl-runtime/oracle/literal_string.1.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/literal_string.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/localvar.1.res.oracle | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle | 4 ++--
.../tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle | 6 +++---
.../tests/e-acsl-runtime/oracle/valid_alias.res.oracle | 6 +++---
10 files changed, 19 insertions(+), 23 deletions(-)
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index b9b703500a4..8f2368d634f 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -41,8 +41,7 @@ module Env: sig
val clear: unit -> unit
val add: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t -> unit
val find: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t
- module StartData: Dataflow.StmtStartData with type key = stmt
- and type data = Varinfo.Set.t option
+ module StartData: Dataflow.StmtStartData with type data = Varinfo.Set.t option
val is_consolidated: unit -> bool
val consolidate: Varinfo.Set.t -> unit
val consolidated_mem: varinfo -> bool
@@ -104,7 +103,6 @@ let reset = Env.clear
module rec Transfer
: Dataflow.BackwardsTransfer with type t = Varinfo.Set.t option
- and type StmtStartData.key = stmt
= struct
let name = "E_ACSL.Pre_analysis"
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index c1e242e49a2..ffe00ca28e0 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -77,7 +77,7 @@ void _free(void* ptr) {
/* resize the block starting at ptr to fit its new size,
* for further information, see realloc */
void* _realloc(void* ptr, size_t size) {
- struct _block * tmp, * next;
+ struct _block * tmp;
void * new_ptr;
if(ptr == NULL) return _malloc(size);
if(size <= 0) {
@@ -99,7 +99,7 @@ void* _realloc(void* ptr, size_t size) {
tmp->init_cpt = size;
/* realloc bigger larger block */
else {
- int i, nb = needed_bytes(size);
+ int nb = needed_bytes(size);
tmp->init_ptr = malloc(nb);
memset(tmp->init_ptr, 0xFF, nb);
if(size%8 != 0)
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 bcab71e5a5d..35ae99fd497 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
@@ -198,8 +198,7 @@ tests/e-acsl-runtime/bts1307.i:13:[value] warning: converting value to float: as
[value] computing for function __gmpz_clear <- foo <- main.
Called from tests/e-acsl-runtime/bts1307.i:13.
[value] Done for function __gmpz_clear
-tests/e-acsl-runtime/bts1307.i:17:[value] warning: converting value to float: assert(Ook)
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status unknown.
+tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] Recording results for foo
[value] Done for function foo
[value] computing for function bar <- main.
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 1fa6df12114..5e00a8753fa 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
@@ -140,8 +140,7 @@ tests/e-acsl-runtime/bts1307.i:13:[value] warning: converting value to float: as
[value] computing for function _delete_block <- foo <- main.
Called from tests/e-acsl-runtime/bts1307.i:15.
[value] Done for function _delete_block
-tests/e-acsl-runtime/bts1307.i:17:[value] warning: converting value to float: assert(Ook)
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status unknown.
+tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] Recording results for foo
[value] Done for function foo
[value] computing for function bar <- main.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index 312f7e53905..155a286ac5d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -112,8 +112,8 @@ tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/literal_string.i:25.
[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
[value] Done for function _initialized
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/literal_string.i:25.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index 8dea4c78dfa..543300f7810 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -90,8 +90,8 @@ tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/literal_string.i:25.
[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
[value] Done for function _initialized
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/literal_string.i:25.
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 56eeebe5710..0946a130432 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
@@ -40,8 +40,8 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
[value] computing for function _initialized <- add <- main.
Called from tests/e-acsl-runtime/localvar.c:20.
[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
[value] Done for function _initialized
[value] computing for function _valid <- add <- main.
Called from tests/e-acsl-runtime/localvar.c:20.
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 56eeebe5710..0946a130432 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
@@ -40,8 +40,8 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
[value] computing for function _initialized <- add <- main.
Called from tests/e-acsl-runtime/localvar.c:20.
[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
[value] Done for function _initialized
[value] computing for function _valid <- add <- main.
Called from tests/e-acsl-runtime/localvar.c:20.
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 f4880654869..9e384cf660a 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
@@ -46,8 +46,8 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/valid_alias.c:12.
[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
[value] Done for function _initialized
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
@@ -78,7 +78,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/valid_alias.c:16.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
[value] Done for function _initialized
[value] computing for function _valid <- main.
Called from tests/e-acsl-runtime/valid_alias.c:16.
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 de38f7f5a09..ab2d470262f 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
@@ -45,8 +45,8 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/valid_alias.c:12.
[value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
[value] Done for function _initialized
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
@@ -77,7 +77,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
[value] computing for function _initialized <- main.
Called from tests/e-acsl-runtime/valid_alias.c:16.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
[value] Done for function _initialized
[value] computing for function _valid <- main.
Called from tests/e-acsl-runtime/valid_alias.c:16.
--
GitLab