From ba4b24ab8e033c0a6ec857bb2aca066cfc0b2ccd Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 2 Mar 2011 15:01:55 +0000
Subject: [PATCH] binop (untested) and string literals
---
.../oracle/string_literal.err.oracle | 0
.../oracle/string_literal.res.oracle | 35 +++++++++++
.../tests/e-acsl-runtime/string_literal.i | 5 ++
src/plugins/e-acsl/visit.ml | 61 ++++++++++++++++++-
4 files changed, 100 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
new file mode 100644
index 00000000000..f3e787e5154
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle
@@ -0,0 +1,35 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+PROJECT_FILE:13:[value] Assertion got status valid.
+[value] Recording results for main
+[value] done for function main
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function main:
+/* Generated by Frama-C */
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status ) ;
+/*@ assigns \nothing; */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg )
+{
+ eprintf(msg);
+ exit(1);
+ return;
+}
+
+void main(void)
+{
+ /*@ assert ("toto" ≢ "titi"); */ ;
+ if ("toto" == "titi") {
+ e_acsl_fail((char *)"((\"toto\" \342\211\242 \"titi\"))");
+ }
+ return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i b/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
new file mode 100644
index 00000000000..8320e9dc7e0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/string_literal.i
@@ -0,0 +1,5 @@
+/* run.config
+ COMMENT: string literal */
+void main() {
+ /*@ assert "toto" != "titi"; */
+}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index f7c0f46efa6..d4d36a171cc 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -56,6 +56,61 @@ let mk_if acc e p =
let s = Instr(Call(None, f, [ mkString unknown_loc msg ], unknown_loc))in
mkStmt(If(e, mkBlock [ mkStmt s ], mkBlock [], unknown_loc)) :: acc
+(* ************************************************************************** *)
+(* transforming terms and predicates into C expressions (if any) *)
+(* ************************************************************************** *)
+
+let constant_to_exp = function
+ | CInt64 _ -> not_yet "integer"
+ | CStr _ as c -> new_exp unknown_loc (Const c)
+ | CWStr _ -> not_yet "wide character string constant"
+ | CChr _ -> not_yet "character constant"
+ | CReal _ -> not_yet "floating point constant"
+ | CEnum _ -> not_yet "enum constant"
+
+let rec term_to_exp t = match t.term_node with
+ | TConst c -> constant_to_exp c
+ | TLval _ -> not_yet "left value"
+ | TSizeOf _ -> not_yet "sizeof"
+ | TSizeOfE _ -> not_yet "sizeof(expr)"
+ | TSizeOfStr _ -> not_yet "sizeof(string constant)"
+ | TAlignOf _ -> not_yet "alignof"
+ | TAlignOfE _ -> not_yet "alignof(expr)"
+ | TUnOp _ -> not_yet "unary operator"
+ | TBinOp _ -> not_yet "binary operator"
+ | TCastE _ -> not_yet "cast"
+ | TAddrOf _ -> not_yet "taking address"
+ | TStartOf _ -> not_yet "beginning of an array"
+ | Tapp _ -> not_yet "applying logic function"
+ | Tlambda _ -> not_yet "functional"
+ | TDataCons _ -> not_yet "constructor"
+ | Tif _ -> not_yet "conditional"
+ | Told _ -> not_yet "\\old"
+ | Tat _ -> not_yet "\\at"
+ | Tbase_addr _ -> not_yet "base address"
+ | Tblock_length _ -> not_yet "block length"
+ | Tnull -> not_yet "NULL"
+ | TCoerce _ -> not_yet "coercion"
+ | TCoerceE _ -> not_yet "expression coercion"
+ | TUpdate _ -> not_yet "functional update"
+ | Ttypeof _ -> not_yet "typeof"
+ | Ttype _ -> not_yet "C type"
+ | Tempty_set -> not_yet "empty tset"
+ | Tunion _ -> not_yet "union of tsets"
+ | Tinter _ -> not_yet "intersection of tsets"
+ | Tcomprehension _ -> not_yet "tset comprehension"
+ | Trange _ -> not_yet "range"
+ | Tlet _ -> not_yet "let binding"
+
+(* untested *)
+let relation_to_revbinop = function
+ | Rlt -> Ge
+ | Rgt -> Le
+ | Rle -> Gt
+ | Rge -> Lt
+ | Req -> Ne
+ | Rneq -> Eq
+
(* convert an ACSL named predicate into the opposite C expression (if any).
E.g. \true is converted into 0. *)
let rec named_predicate_to_revexp p = match p.content with
@@ -63,7 +118,11 @@ let rec named_predicate_to_revexp p = match p.content with
| Ptrue -> zero ~loc:unknown_loc
| Papp _ -> not_yet "logic function application"
| Pseparated _ -> not_yet "separated"
- | Prel _ -> not_yet "relation"
+ | Prel(rel, t1, t2) -> (* untested *)
+ let bop = relation_to_revbinop rel in
+ let e1 = term_to_exp t1 in
+ let e2 = term_to_exp t2 in
+ new_exp unknown_loc (BinOp(bop, e1, e2, intType))
| Pand _ -> not_yet "&&"
| Por _ -> not_yet "||"
| Pxor _ -> not_yet "xor"
--
GitLab