From 3c49bbfcc90c61a8d7c9b096f8fc79ccfb12fa93 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 24 Nov 2011 12:41:54 +0000
Subject: [PATCH] [e-acsl] minor changes
---
src/plugins/e-acsl/env.mli | 4 ++++
.../tests/e-acsl-runtime/oracle/result.res.oracle | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/result.i | 3 +--
src/plugins/e-acsl/visit.ml | 11 ++++-------
4 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index ac510497cf2..a5ff820a2d7 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -60,6 +60,10 @@ val add_stmt: t -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s] *)
val extend_stmt_in_place: t -> stmt -> pre:bool -> block -> t
+(** [extend_stmt_in_place env stmt ~pre b] modifies [stmt] in place in order to
+ add the given [block]. If [pre] is [true], then this block is guaranteed
+ to be at the first place of the resulting [stmt] whatever modification
+ will be done by the visitor later. *)
val push: t -> t
(** Push a new local context in the environment *)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 42f8891516e..e678905c8aa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -1,4 +1,4 @@
-tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+tests/e-acsl-runtime/result.i:6:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
index b18c3c412ae..2e7e3c16023 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/result.i
@@ -1,9 +1,8 @@
/* run.config
COMMENT: \result
- EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp
+ EXECNOW: LOG gen_result.c BIN gen_result.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/result.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_result.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_result.out ./tests/e-acsl-runtime/result/gen_result.c -lgmp && ./tests/e-acsl-runtime/result/gen_result.out
*/
-// && ./tests/e-acsl-runtime/result/gen_result.out
/*@ ensures \result == (int)(x - x); */
int f(int x) {
x = 0;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 1d852dd77cc..9fabddae6f6 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -363,8 +363,8 @@ and context_insensitive_term_to_exp env t =
| Tbase_addr _ -> Misc.not_yet "\\base_addr"
| Tblock_length _ -> Misc.not_yet "\\block_length"
| Tnull -> mkCast (zero ~loc) (TPtr(TVoid [], [])), env, false
- | TCoerce _ -> Misc.not_yet "coercion"
- | TCoerceE _ -> Misc.not_yet "expression coercion"
+ | TCoerce _ -> Misc.not_yet "coercion" (* Jessie specific *)
+ | TCoerceE _ -> Misc.not_yet "expression coercion" (* Jessie specific *)
| TUpdate _ -> Misc.not_yet "functional update"
| Ttypeof _ -> Misc.not_yet "typeof"
| Ttype _ -> Misc.not_yet "C type"
@@ -480,7 +480,7 @@ let rec named_predicate_to_exp env p =
| Pvalid_index _ -> Misc.not_yet "\\valid_index"
| Pvalid_range _ -> Misc.not_yet "\\valid_range"
| Pfresh _ -> Misc.not_yet "\\fresh"
- | Psubtype _ -> Misc.not_yet "subtyping relation"
+ | Psubtype _ -> Misc.not_yet "subtyping relation" (* Jessie specific? *)
| Pinitialized _ -> Misc.not_yet "\\initialized"
(* ************************************************************************** *)
@@ -706,11 +706,8 @@ class e_acsl_visitor prj generate = object (self)
(* must generate [pre_block] which includes [stmt] before generating
[post_block] *)
let pre_block, env =
-(* Options.feedback "HERE";*)
- (*Project.on prj*) (fun () -> Env.pop_and_get env stmt
- ~global_clear:false Env.After ) ()
+ Env.pop_and_get env stmt ~global_clear:false Env.After
in
-(* Options.feedback "DONE";*)
let env = mk_post_env (Env.push env) in
let post_block, env =
Env.pop_and_get
--
GitLab