From 7777a62c190f62076a75e28929a4a7f9d37f0ce1 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 23 Nov 2011 17:19:31 +0000
Subject: [PATCH] [e-acsl] document compilation scheme of \at
---
src/plugins/e-acsl/TODO | 5 +++++
src/plugins/e-acsl/visit.ml | 20 ++++++++++++++++----
2 files changed, 21 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 75d5f9ed022..07935b4b05f 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -21,6 +21,11 @@
- introduire feature wishes Bernard (voir mail du 9 juin)
- arithmetic overflows
+##############
+# KNOWN BUGS #
+##############
+- \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
+
#########
# TESTS #
#########
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 09b8d2b7bdf..84de17b01a6 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -299,22 +299,32 @@ and context_insensitive_term_to_exp env t =
| Tif _ -> Misc.not_yet "conditional"
| Tat(t', label) ->
let stmt = Env.stmt_of_label env label in
- (* Options.feedback "proceeding term %a" Term.pretty t;*)
let ty = t'.term_type in
+ (* convert [t'] to [e] in a separated local env *)
let e, env = term_to_exp (Env.push env) ty t' in
let new_v = ref None in
+ (* generate a new variable denoting [\at(t',label)].
+ That is this variable which is the resulting expression.
+ ACSL typing rule ensures that the type of this variable is the same as
+ the one of [e]. *)
let res, env =
Env.new_var ~global:true env
(Some t) (typeOf e)
- (fun lv' e' -> new_v := Some (lv', e'); [])
+ (fun lv' e' ->
+ (* store the corresponding left value and expression corresponding to
+ the new variable. Will be used in the visitor in order to
+ initialize it. *)
+ new_v := Some (lv', e'); [])
in
let env_ref = ref env in
+ (* visitor modifying in place the labeled statement in order to store [e] in
+ the resulting variable at this location which is the only correct one. *)
let o = object
inherit Visitor.frama_c_inplace
method vstmt_aux stmt =
-(* Options.feedback "labeled stmt sid %d (%a) = %a"
- stmt.sid Project.pretty (Project.current ()) Stmt.pretty stmt;*)
let new_lv, new_e = Extlib.the !new_v in
+ (* either a standard C affectation or an mpz one according to type of
+ [e] *)
let new_stmt =
if Mpz.is_t (typeOf new_e) then
Mpz.init_set new_e e
@@ -323,6 +333,8 @@ and context_insensitive_term_to_exp env t =
(Set((Var new_lv, NoOffset), e, Location.unknown))
in
assert (!env_ref == env);
+ (* generate the new block of code for the labeled statement and the
+ corresponding environment *)
let block, env =
Env.pop_and_get env new_stmt ~global_clear:false Env.Middle
in
--
GitLab