Merge branch '744-rte-pb-with-floats-in-expr-to-term-conversion' into 'master'

Resolve "[rte] pb. with floats in expr to term conversion"

Closes #744

See merge request frama-c/frama-c!2598

.Makefile.lint

@@ -10,7 +10,6 @@ ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
 ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
 ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
 ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
-ML_LINT_KO+=src/kernel_internals/typing/asm_contracts.ml
 ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
 ML_LINT_KO+=src/kernel_internals/typing/infer_annotations.ml
 ML_LINT_KO+=src/kernel_internals/typing/mergecil.mli
@@ -144,8 +143,6 @@ ML_LINT_KO+=src/libraries/utils/command.ml
 ML_LINT_KO+=src/libraries/utils/command.mli
 ML_LINT_KO+=src/libraries/utils/escape.mli
 ML_LINT_KO+=src/libraries/utils/filepath.ml
-ML_LINT_KO+=src/libraries/utils/floating_point.ml
-ML_LINT_KO+=src/libraries/utils/floating_point.mli
 ML_LINT_KO+=src/libraries/utils/hook.ml
 ML_LINT_KO+=src/libraries/utils/hook.mli
 ML_LINT_KO+=src/libraries/utils/hptmap.ml

share/libc/netinet/in.h

@@ -25,7 +25,7 @@
 
 #ifndef __FC_NETINET_IN
 #define __FC_NETINET_IN
-#include "features.h"
+#include "../features.h"
 __PUSH_FC_STDLIB
 #include "../__fc_inet.h"
 __POP_FC_STDLIB

share/libc/sys/socket.h

@@ -46,7 +46,7 @@ struct sockaddr_storage {
   sa_family_t   ss_family;
 };
 
-#include "sys/uio.h"
+#include "./uio.h"
 
 struct cmsghdr {
   socklen_t  cmsg_len;

src/kernel_internals/typing/asm_contracts.ml

@@ -33,24 +33,24 @@ let emitter =
 
 let find_out_lval l =
   let treat_one_lval (output, input) (_,constr, lv) =
-    let tlv = Logic_utils.lval_to_term_lval ~cast:false lv in
+    let tlv = Logic_utils.lval_to_term_lval lv in
     match constr with
-      | "" -> tlv :: output, input
-      | _ ->
-        (* '+' indicates that the lval is used both as input and as output. 
-           GNU syntax allows it only at the beginning of the constraint, but
-           actual implementation is more liberal and emits only a warning.
-        *)
-        if String.contains constr '+' then begin
-          if constr.[0] <> '+' then
-            Kernel.warning
-              "output constraint '+' is not at the beginning in output operand";
-          tlv::output,
-          (* avoid sharing ids *)
-          Visitor.visitFramacTermLval
-            (new Visitor.frama_c_refresh(Project.current())) tlv
-          :: input
-        end else tlv::output, input
+    | "" -> tlv :: output, input
+    | _ ->
+      (* '+' indicates that the lval is used both as input and as output.
+         GNU syntax allows it only at the beginning of the constraint, but
+         actual implementation is more liberal and emits only a warning.
+      *)
+      if String.contains constr '+' then begin
+        if constr.[0] <> '+' then
+          Kernel.warning
+            "output constraint '+' is not at the beginning in output operand";
+        tlv::output,
+        (* avoid sharing ids *)
+        Visitor.visitFramacTermLval
+          (new Visitor.frama_c_refresh(Project.current())) tlv
+        :: input
+      end else tlv::output, input
   in
   let output, input =
     List.fold_left treat_one_lval ([],[]) l
@@ -63,7 +63,7 @@ let extract_term_lval acc (_,_,e) =
     object
       inherit Visitor.frama_c_inplace
       method! vlval lv =
-        res := Logic_utils.lval_to_term_lval ~cast:false lv :: !res;
+        res := Logic_utils.lval_to_term_lval lv :: !res;
         Cil.SkipChildren
     end
   in
@@ -112,123 +112,123 @@ let extract_mem_terms ~loc l =
   List.rev (List.fold_left (extract_mem_term ~loc) [] l)
 
 class visit_assembly =
-object(self)
-  inherit Visitor.frama_c_inplace
+  object(self)
+    inherit Visitor.frama_c_inplace
 
-  method! vinst i =
-    let stmt = Extlib.the self#current_stmt in
-    let kf = Extlib.the self#current_kf in
-    match i with
+    method! vinst i =
+      let stmt = Extlib.the self#current_stmt in
+      let kf = Extlib.the self#current_kf in
+      match i with
       | Asm(_, _, Some { asm_outputs; asm_inputs; asm_clobbers }, loc) ->
-          let lv_out, lv_from = find_out_lval asm_outputs in
-          let lv_from = lv_from @ find_input_lval asm_inputs in
-          let mem_output = extract_mem_terms ~loc lv_from in
-          let lv_out = lv_out @ mem_output in
-          let lv_from = lv_from @ mem_output in
-          let lv_from =
-            List.filter
-              (fun lv ->
-                 not (Logic_utils.isLogicArrayType (Cil.typeOfTermLval lv)))
-              lv_from
+        let lv_out, lv_from = find_out_lval asm_outputs in
+        let lv_from = lv_from @ find_input_lval asm_inputs in
+        let mem_output = extract_mem_terms ~loc lv_from in
+        let lv_out = lv_out @ mem_output in
+        let lv_from = lv_from @ mem_output in
+        let lv_from =
+          List.filter
+            (fun lv ->
+               not (Logic_utils.isLogicArrayType (Cil.typeOfTermLval lv)))
+            lv_from
+        in
+        (* the only interesting information for clobbers is the
+           presence of the "memory" keyword, which indicates that
+           memory may have been accessed (read or write) outside of
+           the locations explicitly referred to as output or
+           input. We can't do much more than emitting a warning and
+           considering that nothing is touched beyond normally
+           specified outputs and inputs. *)
+        let mem_clobbered = List.mem "memory" asm_clobbers in
+        if  mem_clobbered then begin
+          let source = fst (Cil_datatype.Instr.loc i) in
+          let once = true in
+          Kernel.warning
+            ~once ~source
+            "Clobber list contains \"memory\" argument. Assuming no \
+             side effects beyond those mentioned in operands."
+        end;
+        let to_id_term lv =
+          Logic_const.new_identified_term
+            (Logic_const.term ~loc (TLval lv) (Cil.typeOfTermLval lv))
+        in
+        let to_id_from lv =
+          let typ = Cil.typeOfTermLval lv in
+          let base_term = Logic_const.term ~loc (TLval lv) typ in
+          let term =
+            if Logic_utils.isLogicPointerType typ ||
+               Logic_utils.isLogicArrayType typ
+            then { base_term with term_name = ["indirect"] }
+            else base_term
           in
-          (* the only interesting information for clobbers is the
-             presence of the "memory" keyword, which indicates that
-             memory may have been accessed (read or write) outside of
-             the locations explicitly referred to as output or
-             input. We can't do much more than emitting a warning and
-             considering that nothing is touched beyond normally
-             specified outputs and inputs. *)
-          let mem_clobbered = List.mem "memory" asm_clobbers in
-          if  mem_clobbered then begin
-            let source = fst (Cil_datatype.Instr.loc i) in
-            let once = true in
-            Kernel.warning
-              ~once ~source
-              "Clobber list contains \"memory\" argument. Assuming no \
-               side effects beyond those mentioned in operands."
-          end;
-          let to_id_term lv =
-            Logic_const.new_identified_term
-              (Logic_const.term ~loc (TLval lv) (Cil.typeOfTermLval lv))
-          in
-          let to_id_from lv =
-            let typ = Cil.typeOfTermLval lv in
-            let base_term = Logic_const.term ~loc (TLval lv) typ in
-            let term =
-              if Logic_utils.isLogicPointerType typ ||
-                 Logic_utils.isLogicArrayType typ
-              then { base_term with term_name = ["indirect"] }
-              else base_term
-            in
-            Logic_const.new_identified_term term
-          in
-          let assigns () =
-            Writes
-              (List.map
-                 (fun x -> (to_id_term x, From (List.map to_id_from lv_from)))
-                 lv_out)
-          in
-          let filter ca =
-            match ca.annot_content with
-                (* search for a statement contract that applies to all cases. *)
-              | AStmtSpec ([],_) -> true
-              | _ -> false
-          in
-          let contracts = Annotations.code_annot ~filter stmt in
-          (match contracts with
-           | [] ->
-                let assigns = assigns () in
-                let bhv = Cil.mk_behavior ~assigns () in
-                let spec = Cil.empty_funspec () in
-                spec.spec_behavior <- [ bhv ];
-                let ca =
-                  Logic_const.new_code_annotation (AStmtSpec ([],spec))
-                in
-                Annotations.add_code_annot emitter ~kf stmt ca;
-                if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
-                then begin
-                  let active = [] in
-                  let ip_assigns =
-                    Property.ip_assigns_of_behavior kf (Kstmt stmt) ~active bhv in
-                  let ip_from =
-                    Property.ip_from_of_behavior kf (Kstmt stmt) ~active bhv in
-                  List.iter
-                    Property_status.(
-                      fun x -> emit emitter ~hyps:[] x True)
-                    (Extlib.list_of_opt ip_assigns @ ip_from)
-                end
-           | [ { annot_content = AStmtSpec ([], spec) } ] ->
-                (* Already existing contracts. Just add assigns clause for
-                   behaviors that do not already have one. *)
+          Logic_const.new_identified_term term
+        in
+        let assigns () =
+          Writes
+            (List.map
+               (fun x -> (to_id_term x, From (List.map to_id_from lv_from)))
+               lv_out)
+        in
+        let filter ca =
+          match ca.annot_content with
+          (* search for a statement contract that applies to all cases. *)
+          | AStmtSpec ([],_) -> true
+          | _ -> false
+        in
+        let contracts = Annotations.code_annot ~filter stmt in
+        (match contracts with
+         | [] ->
+           let assigns = assigns () in
+           let bhv = Cil.mk_behavior ~assigns () in
+           let spec = Cil.empty_funspec () in
+           spec.spec_behavior <- [ bhv ];
+           let ca =
+             Logic_const.new_code_annotation (AStmtSpec ([],spec))
+           in
+           Annotations.add_code_annot emitter ~kf stmt ca;
+           if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
+           then begin
+             let active = [] in
+             let ip_assigns =
+               Property.ip_assigns_of_behavior kf (Kstmt stmt) ~active bhv in
+             let ip_from =
+               Property.ip_from_of_behavior kf (Kstmt stmt) ~active bhv in
              List.iter
-               (fun bhv ->
-                  match bhv.b_assigns with
-                  | WritesAny ->
-                    let behavior = bhv.b_name in
-                    let assigns = assigns () in
-                    let keep_empty = false in
-                    Annotations.add_assigns
-                      ~keep_empty emitter kf ~stmt ~behavior assigns;
-                  | Writes _ -> ())
-               spec.spec_behavior
-           | _ ->
-             Kernel.fatal "Several contracts found for the same statement %a"
-               Printer.pp_stmt stmt
-          );
-          Cil.SkipChildren
+               Property_status.(
+                 fun x -> emit emitter ~hyps:[] x True)
+               (Extlib.list_of_opt ip_assigns @ ip_from)
+           end
+         | [ { annot_content = AStmtSpec ([], spec) } ] ->
+           (* Already existing contracts. Just add assigns clause for
+              behaviors that do not already have one. *)
+           List.iter
+             (fun bhv ->
+                match bhv.b_assigns with
+                | WritesAny ->
+                  let behavior = bhv.b_name in
+                  let assigns = assigns () in
+                  let keep_empty = false in
+                  Annotations.add_assigns
+                    ~keep_empty emitter kf ~stmt ~behavior assigns;
+                | Writes _ -> ())
+             spec.spec_behavior
+         | _ ->
+           Kernel.fatal "Several contracts found for the same statement %a"
+             Printer.pp_stmt stmt
+        );
+        Cil.SkipChildren
       | Asm(_,_,None,_) ->
         Kernel.feedback
           ~dkey:Kernel.dkey_asm_contracts "Ignoring basic assembly instruction";
         Cil.SkipChildren
       | _ -> Cil.SkipChildren
-end
+  end
 
 let transform file =
   if Kernel.AsmContractsGenerate.get() then
     Visitor.visitFramacFileSameGlobals (new visit_assembly) file
 
 let () =
-  File.add_code_transformation_after_cleanup 
+  File.add_code_transformation_after_cleanup
     ~deps:[(module Kernel.AsmContractsGenerate);
            (module Kernel.AsmContractsAutoValidate) ]
     category

src/kernel_internals/typing/cabs2cil.ml

@@ -8858,9 +8858,9 @@ and createLocal ghost ((_, sto, _, _) as specs)
           (se0 +++ (
               let castloc = CurrentLoc.get () in
               let talloca_size =
-                let telt_size = Logic_utils.expr_to_term ~cast:false elt_size in
-                let tlen = Logic_utils.expr_to_term ~cast:false len in
-                Logic_const.term (TBinOp (Mult,telt_size,tlen)) telt_size.term_type
+                let size = Logic_utils.expr_to_term ~coerce:true elt_size in
+                let tlen = Logic_utils.expr_to_term ~coerce:true len in
+                Logic_const.term (TBinOp (Mult,size,tlen)) Linteger
               in
               let pos_size =
                 let zero =  Logic_const.tinteger ~loc:castloc 0 in

src/kernel_internals/typing/logic_builtin.ml

@@ -293,6 +293,18 @@ let init =
             (*"\\round_quad", [],
                ["m",  rounding_mode; "x", Lreal], long_double_type;*)
 
+            "\\neg_float",[],["x",float_type], float_type;
+            "\\add_float",[],["x",float_type;"y",float_type], float_type;
+            "\\sub_float",[],["x",float_type;"y",float_type], float_type;
+            "\\mul_float",[],["x",float_type;"y",float_type], float_type;
+            "\\div_float",[],["x",float_type;"y",float_type], float_type;
+
+            "\\neg_double",[],["x",double_type], double_type;
+            "\\add_double",[],["x",double_type;"y",double_type], double_type;
+            "\\sub_double",[],["x",double_type;"y",double_type], double_type;
+            "\\mul_double",[],["x",double_type;"y",double_type], double_type;
+            "\\div_double",[],["x",double_type;"y",double_type], double_type;
+
             "\\min", [], ["s", set_of_integer], Linteger;
             "\\max", [], ["s", set_of_integer], Linteger;
 

src/kernel_services/analysis/logic_interp.ml

@@ -200,7 +200,7 @@ let rec logic_type_to_typ = function
   | Ctype typ -> typ
   | Linteger -> TInt(ILongLong,[]) (*TODO: to have an unlimited integer type
                                     in the logic interpretation*)
-  | Lreal -> TFloat(FLongDouble,[]) (* TODO: handle reals, not floats... *)
+  | Lreal -> TFloat(FDouble,[]) (* TODO: handle reals, not floats... *)
   | Ltype({lt_name = name},[]) when name = Utf8_logic.boolean  ->
       TInt(ILongLong,[])
   | Ltype({lt_name = "set"},[t]) -> logic_type_to_typ t

src/kernel_services/ast_data/alarms.ml

@@ -451,21 +451,21 @@ let overflowed_expr_to_term ~loc e =
   let loc = best_loc ~loc e.eloc in
   match e.enode with
   | UnOp(op, e, ty) ->
-    let t = Logic_utils.expr_to_term ~cast:true e in
-    let ty = Logic_utils.typ_to_logic_type ty in
-    Logic_const.term ~loc (TUnOp(op, t)) ty
+    let t = Logic_utils.expr_to_term ~coerce:true e in
+    let lty = Logic_utils.coerce_type ty in
+    Logic_const.term ~loc (TUnOp(op, t)) lty
   | BinOp(op, e1, e2, ty) ->
-    let t1 = Logic_utils.expr_to_term ~cast:true e1 in
-    let t2 = Logic_utils.expr_to_term ~cast:true e2 in
-    let ty = Logic_utils.typ_to_logic_type ty in
-    Logic_const.term ~loc (TBinOp(op, t1, t2)) ty
-  | _ -> Logic_utils.expr_to_term ~cast:true e
+    let t1 = Logic_utils.expr_to_term ~coerce:true e1 in
+    let t2 = Logic_utils.expr_to_term ~coerce:true e2 in
+    let lty = Logic_utils.coerce_type ty in
+    Logic_const.term ~loc (TBinOp(op, t1, t2)) lty
+  | _ -> Logic_utils.expr_to_term ~coerce:true e
 
 (* Creates \is_finite((fkind)e) or \is_nan((fkind)e) according to
    [predicate]. *)
 let create_special_float_predicate ~loc e fkind predicate =
   let loc = best_loc ~loc e.eloc in
-  let t = Logic_utils.expr_to_term ~cast:true e in
+  let t = Logic_utils.expr_to_term e in
   let typ = match fkind with
     | FFloat -> Cil.floatType
     | FDouble -> Cil.doubleType
@@ -490,7 +490,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
     | Division_by_zero e ->
       (* e != 0 *)
       let loc = best_loc ~loc e.eloc in
-      let t = Logic_utils.expr_to_term ~cast:true e in
+      let t = Logic_utils.expr_to_term ~coerce:true e in
       Logic_const.prel ~loc (Rneq, t, Cil.lzero ())
 
     | Memory_access(lv, read) ->
@@ -500,22 +500,23 @@ let create_predicate ?(loc=Location.unknown) alarm =
         | For_writing -> Logic_const.pvalid
       in
       let e = Cil.mkAddrOrStartOf ~loc lv in
-      let t = Logic_utils.expr_to_term ~cast:true e in
+      let t = Logic_utils.expr_to_term e in
       valid ~loc (Logic_const.here_label, t)
 
     | Index_out_of_bound(e1, e2) ->
       (* 0 <= e1 < e2, left part if None, right part if Some e *)
       let loc = best_loc ~loc e1.eloc in
-      let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+      let t1 = Logic_utils.expr_to_term ~coerce:true e1 in
       (match e2 with
-       | None -> Logic_const.prel ~loc (Rle, Cil.lzero (), t1)
+       | None ->
+         Logic_const.prel ~loc (Rle, Cil.lzero (), t1)
        | Some e2 ->
-         let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+         let t2 = Logic_utils.expr_to_term ~coerce:true e2 in
          Logic_const.prel ~loc (Rlt, t1, t2))
 
     | Invalid_pointer e ->
       let loc = best_loc ~loc e.eloc in
-      let t = Logic_utils.expr_to_term ~cast:true e in
+      let t = Logic_utils.expr_to_term e in
       if Cil.isFunPtrType (Cil.typeOf e)
       then Logic_const.pvalid_function ~loc t
       else Logic_const.pobject_pointer ~loc (Logic_const.here_label, t)
@@ -523,12 +524,12 @@ let create_predicate ?(loc=Location.unknown) alarm =
     | Invalid_shift(e, n) ->
       (* 0 <= e < n *)
       let loc = best_loc ~loc e.eloc in
-      let t = Logic_utils.expr_to_term ~cast:true e in
+      let t = Logic_utils.expr_to_term ~coerce:true e in
       let low_cmp = Logic_const.prel ~loc (Rle, Cil.lzero (), t) in
       (match n with
        | None -> low_cmp
        | Some n ->
-         let tn = Logic_const.tint ~loc (Integer.of_int n) in
+         let tn = Logic_const.tinteger ~loc n in
          let up_cmp = Logic_const.prel ~loc (Rlt, t, tn) in
          Logic_const.pand ~loc (low_cmp, up_cmp))
 
@@ -544,21 +545,21 @@ let create_predicate ?(loc=Location.unknown) alarm =
             let zero = Cil.lzero () in
             Logic_const.term (TCastE (typ, zero)) (Ctype typ)
           end
-        | Some e -> Logic_utils.expr_to_term ~cast:true e
+        | Some e -> Logic_utils.expr_to_term e
       in
-      let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+      let t2 = Logic_utils.expr_to_term e2 in
       Logic_utils.pointer_comparable ~loc t1 t2
 
     | Differing_blocks(e1, e2) ->
       (* \base_addr(e1) == \base_addr(e2) *)
       let loc = best_loc ~loc e1.eloc in
-      let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+      let t1 = Logic_utils.expr_to_term e1 in
       let here = Logic_const.here_label in
       let typ = Ctype Cil.charPtrType in
       let t1 =
         Logic_const.term ~loc:(best_loc loc e1.eloc) (Tbase_addr(here, t1)) typ
       in
-      let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+      let t2 = Logic_utils.expr_to_term e2 in
       let t2 =
         Logic_const.term ~loc:(best_loc loc e2.eloc) (Tbase_addr(here, t2)) typ
       in
@@ -569,10 +570,10 @@ let create_predicate ?(loc=Location.unknown) alarm =
       let loc = best_loc ~loc e.eloc in
       let t = match kind with
         | Pointer_downcast ->
-          let t = Logic_utils.expr_to_term ~cast:true e in
+          let t = Logic_utils.expr_to_term e in
           Logic_const.tcast ~loc t Cil.theMachine.upointType
         | Signed_downcast | Unsigned_downcast ->
-          Logic_utils.expr_to_term ~cast:true e
+          Logic_utils.expr_to_term ~coerce:true e
         | _ ->
           (* For overflows, the computation must be done on mathematical types,
              else the value is necessarily in bounds. *)
@@ -580,7 +581,9 @@ let create_predicate ?(loc=Location.unknown) alarm =
       in
       let tn = Logic_const.tint ~loc n in
       Logic_const.prel ~loc
-        (match bound with Lower_bound -> Rle, tn, t | Upper_bound -> Rle, t, tn)
+        (match bound with
+         | Lower_bound -> Rle, tn, t
+         | Upper_bound -> Rle, t, tn)
 
     | Float_to_int(e, n, bound) ->
       (* n < e or e < n according to bound *)
@@ -588,27 +591,31 @@ let create_predicate ?(loc=Location.unknown) alarm =
       let te = overflowed_expr_to_term ~loc e in
       let t = Logic_const.tlogic_coerce ~loc te Lreal in
       let n =
-        (match bound with Lower_bound -> Integer.sub | Upper_bound -> Integer.add)
+        (match bound with
+         | Lower_bound -> Integer.sub
+         | Upper_bound -> Integer.add)
           n Integer.one
       in
       let tn = Logic_const.tlogic_coerce ~loc (Logic_const.tint ~loc n) Lreal in
       Logic_const.prel ~loc
-        (match bound with Lower_bound -> Rlt, tn, t | Upper_bound -> Rlt, t, tn)
+        (match bound with
+         | Lower_bound -> Rlt, tn, t
+         | Upper_bound -> Rlt, t, tn)
 
     | Not_separated(lv1, lv2) ->
       (* \separated(lv1, lv2) *)
       let e1 = Cil.mkAddrOf ~loc lv1 in
-      let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+      let t1 = Logic_utils.expr_to_term e1 in
       let e2 = Cil.mkAddrOf ~loc lv2 in
-      let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+      let t2 = Logic_utils.expr_to_term e2 in
       Logic_const.pseparated ~loc [ t1; t2 ]
 
     | Overlap(lv1, lv2) ->
       (* (lv1 == lv2) || \separated(lv1, lv2) *)
       let e1 = Cil.mkAddrOf ~loc lv1 in
-      let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+      let t1 = Logic_utils.expr_to_term e1 in
       let e2 = Cil.mkAddrOf ~loc lv2 in
-      let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+      let t2 = Logic_utils.expr_to_term e2 in
       let eq = Logic_const.prel ~loc (Req, t1, t2) in
       let sep = Logic_const.pseparated ~loc [ t1; t2 ] in
       Logic_const.por ~loc (eq, sep)
@@ -616,13 +623,13 @@ let create_predicate ?(loc=Location.unknown) alarm =
     | Uninitialized lv ->
       (* \initialized(lv) *)
       let e = Cil.mkAddrOrStartOf ~loc lv in
-      let t = Logic_utils.expr_to_term ~cast:false e in
+      let t = Logic_utils.expr_to_term e in
       Logic_const.pinitialized ~loc (Logic_const.here_label, t)
 
     | Dangling lv ->
       (* !\dangling(lv) *)
       let e = Cil.mkAddrOrStartOf ~loc lv in
-      let t = Logic_utils.expr_to_term ~cast:false e in
+      let t = Logic_utils.expr_to_term e in
       Logic_const.(pnot ~loc (pdangling ~loc (Logic_const.here_label, t)))
 
     | Is_nan_or_infinite (e, fkind) ->
@@ -648,14 +655,14 @@ let create_predicate ?(loc=Location.unknown) alarm =
              that has unexpected type %a (unrolled as %a)"
             Printer.pp_exp e Printer.pp_typ t Printer.pp_typ t'
       in
-      let t = Logic_utils.expr_to_term ~cast:true e in
+      let t = Logic_utils.expr_to_term e in
       Logic_const.(pvalid_function ~loc t)
 
     | Uninitialized_union llv ->
       (* \initialized(lv_1) || ... || \initialized(lv_n) *)
       let make_lval_predicate lv =
         let e = Cil.mkAddrOrStartOf ~loc lv in
-        let t = Logic_utils.expr_to_term ~cast:false e in
+        let t = Logic_utils.expr_to_term e in
         Logic_const.pinitialized ~loc (Logic_const.here_label, t)
       in
       List.fold_left (fun acc lv ->
@@ -666,7 +673,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
 
     | Invalid_bool lv ->
       let e = Cil.new_exp ~loc (Lval lv) in
-      let t = Logic_utils.expr_to_term ~cast:false e in
+      let t = Logic_utils.expr_to_term ~coerce:true e in
       let zero = Logic_const.prel ~loc (Req, t, Cil.lzero ()) in
       let one = Logic_const.prel ~loc (Req, t, Cil.lone ()) in
       Logic_const.por ~loc (zero, one)

src/kernel_services/ast_data/statuses_by_call.ml

@@ -160,7 +160,7 @@ let rec associate acc ~formals ~concretes =
   | [], _ -> acc
   | _, [] -> raise Non_Transposable
   | formal :: formals, concrete :: concretes ->
-    let term = Logic_utils.expr_to_term ~cast:true concrete in
+    let term = Logic_utils.expr_to_term concrete in
     associate ((formal, term) :: acc) ~formals ~concretes
 
 let transpose_pred_at_callsite ~formals ~concretes pred =

src/kernel_services/ast_printing/cil_printer.ml

@@ -2432,7 +2432,14 @@ class cil_printer () = object (self)
     | TBinOp (op,l,r) ->
       fprintf fmt "@[%a@ %a@ %a@]" term l self#term_binop op term r