From d9c0c7041e1708afdb9bc045d1e204de24381e16 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 15 Nov 2019 17:57:16 +0100
Subject: [PATCH] [logic] make mk_cast aware of logic coercions
---
src/kernel_services/ast_queries/logic_utils.ml | 15 +++++++++++----
tests/spec/expr_to_term.ml | 5 +++--
tests/spec/oracle/expr_to_term.res.oracle | 17 +++++++++++++++++
3 files changed, 31 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 11fa533ea14..0b919947228 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -230,7 +230,8 @@ let mk_cast ?(loc=Cil_datatype.Location.unknown) ?(force=false) newt t =
let typ = Cil.type_remove_attributes_for_logic_type newt
in term ~loc (TCastE (typ, t)) (Ctype typ)
in
- let rec aux1 = function
+ let rec aux1 typ t =
+ match typ with
| Ctype oldt ->
if not (need_logic_cast oldt newt) && not force then t
else begin
@@ -246,15 +247,21 @@ let mk_cast ?(loc=Cil_datatype.Location.unknown) ?(force=false) newt t =
| _, TConst (Integer (i,_)) when Integer.is_zero i -> mk_cast t'
| _ -> mk_cast t
)
- | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef -> aux2 (unroll_ltdef ty)
+ | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
+ aux2 (unroll_ltdef ty)
| _ -> mk_cast t
in aux2 t'.term_type
| _ -> (* Do not remove old cast because they are conversions !!! *)
mk_cast t
end
- | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef -> aux1 (unroll_ltdef ty)
+ | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
+ aux1 (unroll_ltdef ty) t
+ | Linteger | Lreal ->
+ (match t.term_node with
+ | TLogic_coerce (_,t') -> aux1 t'.term_type t'
+ | _ -> mk_cast t)
| _ -> mk_cast t
- in aux1 t.term_type
+ in aux1 t.term_type t
let real_of_float s f =
{ r_literal = s ; r_nearest = f ; r_upper = f ; r_lower = f }
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index 70f83babb9c..17478ac46f1 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -15,10 +15,11 @@ let check_expr_term check fct s e =
| _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond e
in
let term' = Logic_utils.expr_to_term ~cast:false exp in
+ let term' = Logic_utils.mk_cast Cil.intType term' in
if check && not (Cil_datatype.Term.equal term term') then
Kernel.fatal
- "translation of C expression %a inconsistent with logic term %a"
- Printer.pp_exp exp Printer.pp_term term;
+ "translation of C expression %a is %a, inconsistent with logic term %a"
+ Printer.pp_exp exp Printer.pp_term term' Printer.pp_term term;
let p = List.hd (Logic_env.find_all_logic_functions "int_eq") in
let app = Logic_const.papp (p,[],[term;term']) in
let post = Logic_const.new_predicate app in
diff --git a/tests/spec/oracle/expr_to_term.res.oracle b/tests/spec/oracle/expr_to_term.res.oracle
index ed2717ba97a..a378207a1b9 100644
--- a/tests/spec/oracle/expr_to_term.res.oracle
+++ b/tests/spec/oracle/expr_to_term.res.oracle
@@ -40,4 +40,21 @@ int main(void)
return __retres;
}
+/*@ ensures int_eq((int)(!(t ≢ 0)), (int)(!(t ≢ 0)));
+ ensures int_eq((int)(!(t ≢ 0)), (int)5);
+ */
+int g(void)
+{
+ int __retres;
+ if (! t) {
+ __retres = 2;
+ goto return_label;
+ }
+ else {
+ __retres = 3;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
--
GitLab