From bf8d5cb5830e5257a24a2d8c416bb3949e436b94 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 15 Mar 2011 15:21:33 +0000
Subject: [PATCH] [E-ACSL] UseUnicode --> Unicode [E-ACSL] use -e-acsl-check
for all tests [E-ACSL] prepare guarding division and module (commented code
yet)
---
.../e-acsl/tests/e-acsl-reject/test_config | 3 ++-
.../e-acsl/tests/e-acsl-runtime/test_config | 2 +-
src/plugins/e-acsl/tests/test_config.in | 1 +
src/plugins/e-acsl/visit.ml | 15 ++++++++++++---
4 files changed, 16 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/test_config b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
index 61e3a7b0e53..475ef57bff2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/test_config
@@ -1 +1,2 @@
-OPT: -e-acsl-check
+COMMENT: -e-acsl-check set by default
+STDOPT:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index 807e22c9203..3e7ab96b05c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1 +1 @@
-OPT: -e-acsl-project p -then-on p -print -val
+STDOPT: +"-e-acsl-project p" +"-then-on p" +"-print" +"-val"
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
index f15e29fb6c1..899f3ec34cf 100644
--- a/src/plugins/e-acsl/tests/test_config.in
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -1,2 +1,3 @@
CMD: FRAMAC_SHARE=./share @frama-c@ -cpp-command="gcc -C -E -I. -I${FRAMAC_SHARE}"
+OPT: -e-acsl-check
FILTER:@SEDCMD@ -e '/^#[^\n]*/d' -e "s|${FRAMAC_SHARE}|FRAMAC_SHARE|g" -e "s|[a-zA-Z/\\]\+frama_c_project_p_[a-z0-9]*|PROJECT_FILE|"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a5df3eccacd..03c5f2bfb2f 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -51,10 +51,10 @@ let mk_if e p =
let msg =
let b = Buffer.create 97 in
let fmt = Format.formatter_of_buffer b in
- let no_uni = Parameters.UseUnicode.get () in
- Parameters.UseUnicode.off ();
+ let no_uni = Parameters.Unicode.get () in
+ Parameters.Unicode.off ();
Format.fprintf fmt "%a@?" Cil.d_predicate_named p;
- Parameters.UseUnicode.set no_uni;
+ Parameters.Unicode.set no_uni;
Buffer.contents b
in
let s = mk_call "e_acsl_fail" [ mkString unknown_loc msg ] in
@@ -262,6 +262,15 @@ let rec term_to_exp t = match t.term_node with
let e2 = term_to_exp t2 in
assert (Cil_datatype.Typ.equal (typeOf e1) (typeOf e2));
let name = name_of_mpz_arith_bop bop in
+(* (* guarding divisions and modulos *)
+ (match bop with
+ | Div | Mod ->
+ let e =
+ if Mpz.e_got_t e2 then
+ New_vars.push_and_mpz_init (fun _ e -> mk_call "mpz_cmp"
+ New_block.push (mk_if e2 t2
+ (mkStmt ~valid_sid:true (If(e2, , mlBlock [], unknown_loc))
+ | _ -> assert false);*)
New_vars.push_and_mpz_init (fun _ e -> mk_call name [ e; e1; e2 ])
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
--
GitLab