From ddee95a46a2542a3693ff615fa30e7f956e38a6b Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 15 Nov 2019 09:02:55 +0100
Subject: [PATCH] test for conversion issue
---
tests/spec/expr_to_term.i | 9 +++++++--
tests/spec/expr_to_term.ml | 7 +++++--
2 files changed, 12 insertions(+), 4 deletions(-)
diff --git a/tests/spec/expr_to_term.i b/tests/spec/expr_to_term.i
index 12078604eca..5320e071398 100644
--- a/tests/spec/expr_to_term.i
+++ b/tests/spec/expr_to_term.i
@@ -1,6 +1,6 @@
/* run.config
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print
+MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -print
*/
int x[10];
@@ -28,3 +28,8 @@ int main() {
s.z = 3;
t = 4;
}
+
+/*@ ensures int_eq((int)!t,(int)5); */
+int g() {
+ if (!t) return 2; else return 3;
+}
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index 87798a466f2..70f83babb9c 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -6,6 +6,7 @@ let check_expr_term check fct s e =
let exp =
match s.skind with
| Instr (Set (lv,_,loc)) -> Cil.new_exp ~loc (Lval lv)
+ | If (c,_,_,_) -> c
| _ -> Kernel.fatal "Unexpected statement %a" Printer.pp_stmt s
in
let term =
@@ -23,7 +24,6 @@ let check_expr_term check fct s e =
let post = Logic_const.new_predicate app in
Annotations.add_ensures emitter fct [Normal,post]
-
let treat_fct check fct =
let stmts = (Kernel_function.get_definition fct).sbody.bstmts in
let stmts =
@@ -31,6 +31,7 @@ let treat_fct check fct =
(function
{ skind = Instr (Set (lv,_,_)) } ->
(match lv with (Var v,_) -> v.vglob | _ -> true)
+ | { skind = If _ } -> true
| _ -> false)
stmts
in
@@ -49,8 +50,10 @@ let treat_fct check fct =
let compute () =
let main = Globals.Functions.find_by_name "main" in
let f = Globals.Functions.find_by_name "f" in
+ let g = Globals.Functions.find_by_name "g" in
treat_fct true main;
- treat_fct false f
+ treat_fct false f;
+ treat_fct true g
let () = Db.Main.extend compute
--
GitLab