[logic] make mk_cast aware of logic coercions

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 }

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

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;
+}
+