diff --git a/.Makefile.lint b/.Makefile.lint
index e0d284e28cba44c25e03d3d265e07c5c821f0ecb..6e0882bf1a1d2ba676649676b13ac90e70dd4f2d 100644
--- a/.Makefile.lint
+++ b/.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
diff --git a/share/libc/netinet/in.h b/share/libc/netinet/in.h
index e63125c56782773020ffb3920bc72c4b7a2ac62c..6eb54f02eb08689f98c9de89298b8ca1535510dc 100644
--- a/share/libc/netinet/in.h
+++ b/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
diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index bc155eeb8e795caced45889391d7ee5f04daf9d1..4a6e6c21f4f0c90c4f9038e42b47340ad1a7ab38 100644
--- a/share/libc/sys/socket.h
+++ b/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;
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 45ea1252e59071429ba0eb614cef30c7c1351b8e..d87771d648f135516e46dbb69a3eb2c97856afb8 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/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
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 59bf19445ebf5ab7ae5c84c774aa3af77098cf5b..0a59dd7ea6ba6a9a85bf4300dd8a304a1d7995ee 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/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
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index 02d4a73809ef420d1086071a9ec7a73b68321e04..961fc5b3aacdbcb9e60074a996e1238af8389697 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/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;
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 99fd4b2c8a73673792b1a5a65a350c05e0668827..ca8044ead8db1d5b6bb9cfb3459f5aca44692aa4 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/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
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index f251a750c849edc79be4311c941c9d7bad3aa717..a0845e815040b754587d15eca7cf150ba0911b25 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/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)
diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index d5deb1ab1080d98665b68da7e4abbb9d5e9be657..2487ade6c495aebf89aeec1b7caa4891017410ce 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/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 =
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 9acb7457ad8d26e613282077bee4c300cfb1a8bf..fbfc904dc2a8963412e321eaa01982d36048325e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/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
| TCastE (ty,e) ->
- fprintf fmt "(%a)%a" (self#typ None) ty term e
+ begin match ty, t.term_node with
+ | TFloat(fk,_) , TConst(LReal r as cst) when
+ not Kernel.(is_debug_key_enabled dkey_print_logic_coercions) &&
+ Floating_point.has_suffix fk r.r_literal ->
+ self#logic_constant fmt cst
+ | _ ->
+ fprintf fmt "(%a)%a" (self#typ None) ty term e
+ end
| TAddrOf lv ->
fprintf fmt "&%a" (self#term_lval_prec Precedence.addrOfLevel) lv
| TStartOf lv -> fprintf fmt "(%a)%a"
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 1a2e39284a84cb0930db031a8a4c5600771d39a2..e8ae6d486057747ea1dcc2ea5e5b18d52fd7756c 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3072,6 +3072,17 @@ let intKindForValue i (unsigned: bool) =
else if fitsInInt ILongLong i then ILongLong
else raise Not_representable
+(* True is an double constant is finite for a kind *)
+let isFiniteFloat fk v =
+ Floating_point.isfinite @@
+ match fk with
+ | FFloat -> Floating_point.round_to_single_precision_float v
+ | _ -> v
+
+
+let isExactFloat fk r =
+ r.r_upper = r.r_lower && isFiniteFloat fk r.r_nearest
+
(* Construct an integer constant with possible truncation if the kind is not
specified *)
let kinteger64 ~loc ?repr ?kind i =
@@ -3640,7 +3651,7 @@ let typeOf_array_elem t =
let no_op_coerce typ t =
match typ with
- | Lreal -> true
+ | Lreal -> isLogicArithmeticType t.term_type
| Linteger -> isLogicIntegralType t.term_type
| Ltype _ when Logic_const.is_boolean_type typ ->
isLogicPureBooleanType t.term_type
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index c372bb6514cbf4c28bddf8fd90896f0cfe3ea916..b3c39a06f89a8f23c6fc991a3fb449799192a548 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2136,6 +2136,12 @@ val max_unsigned_number: int -> Integer.t
(** True if the integer fits within the kind's range *)
val fitsInInt: ikind -> Integer.t -> bool
+(** True if the float is finite for the kind's range *)
+val isFiniteFloat: fkind -> float -> bool
+
+(** True if the real constant is an exact float for the given type *)
+val isExactFloat: fkind -> logic_real -> bool
+
exception Not_representable
(** raised by {!intKindForValue}. *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 95ca68ae35624037993cf44cc6ceec390dde3ce4..c9f743a32f6e55252fbed085583b467a45c07492 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -386,12 +386,11 @@ let index_typ = function
| TEnum _ -> 8
| TBuiltin_va_list _ -> 9
-let constfoldtoint = ref (fun _ -> failwith "constfoldtoint not yet defined")
-let punrollType =
- ref (fun _ -> failwith "punrollType not yet defined")
+let constfoldtoint = Extlib.mk_fun "constfoldtoint"
+let punrollType = Extlib.mk_fun "punrollType"
+let punrollLogicType = Extlib.mk_fun "punrollLogicType"
let drop_non_logic_attributes = ref (fun a -> a)
-let compare_exp_struct_eq =
- ref (fun _ -> failwith "compare_exp_struct_eq not yet defined")
+let compare_exp_struct_eq = Extlib.mk_fun "compare_exp_struct_eq"
type type_compare_config =
{ by_name : bool;
@@ -1320,17 +1319,15 @@ let rec compare_logic_type config v1 v2 =
| Ltype _ -> 4
| Larrow _ -> 5
in
+ let v1 = if config.unroll then !punrollLogicType v1 else v1 in
+ let v2 = if config.unroll then !punrollLogicType v2 else v2 in
let k1 = rank v1 in
let k2 = rank v2 in
- if k1 <> k2 then k1-k2
+ if k1 <> k2 then
+ k1-k2
else
match v1,v2 with
| Ctype t1 , Ctype t2 -> compare_type config t1 t2
- | Ltype ({lt_def = Some (LTsyn t1)},ts1),
- Ltype ({lt_def = Some (LTsyn t2)},ts2) when config.unroll ->
- let c = compare_logic_type config t1 t2 in
- if c <> 0 then c
- else compare_list (compare_logic_type config) ts1 ts2
| Ltype(a,ts1), Ltype(b,ts2) ->
let c = Logic_type_info.compare a b in
if c <> 0 then c
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index f1cf95ac20963f9d3ac071ca535292e309375c5d..52f914d8ebe394785d5d998afbe9cf7e640a7e0b 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -310,11 +310,11 @@ module Lexpr: S with type t = Logic_ptree.lexpr
(** {2 Internal API} *)
(* ****************************************************************************)
-(* Forward declarations from Cil *)
+(* Forward declarations from Cil et al. *)
val drop_non_logic_attributes : (attributes -> attributes) ref
val constfoldtoint : (exp -> Integer.t option) ref
val punrollType: (typ -> typ) ref
-
+val punrollLogicType: (logic_type -> logic_type) ref
val clear_caches: unit -> unit
(**/**)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f6a1c015fb927e32d3da67b28201a434314b48f7..d0298228e25e382a6a140398d4a14ec0fd524f7b 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -801,7 +801,7 @@ struct
let attrs = Cil.filter_qualifier_attributes attrs in
let field = C.find_comp_field comp f in
let typ = Cil.typeOffset ty field in
- Logic_utils.offset_to_term_offset ~cast:false field,
+ Logic_utils.offset_to_term_offset field,
Ctype (Cil.typeAddAttributes attrs typ)
with Not_found -> C.error loc "cannot find field %s" f)
| _ ->
@@ -2537,8 +2537,9 @@ struct
TConst c, Linteger
| _ -> assert false
end
- | PLconstant (FloatConstant str) ->
- TConst (Logic_utils.string_to_float_lconstant str), Lreal
+ | PLconstant (FloatConstant s) ->
+ let t = Logic_utils.parse_float ~loc s in
+ t.term_node , t.term_type
| PLconstant (StringConstant s) ->
TConst (LStr (unescape s)), Ctype Cil.charPtrType
| PLconstant (WStringConstant s) ->
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index ea652d98361c8868f61b4ba6454c76db096fbb98..242feb6c6a054e09f4016d0168be57a3e4a9c38f 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -123,11 +123,11 @@ let plain_array_to_ptr ty =
let array_to_ptr = plain_or_set plain_array_to_ptr
-let typ_to_logic_type e_typ =
- let ty = Cil.unrollType e_typ in
+let coerce_type typ =
+ let ty = Cil.unrollType typ in
if Cil.isIntegralType ty then Linteger
else if Cil.isFloatingType ty then Lreal
- else Ctype e_typ
+ else Ctype typ
let predicate_of_identified_predicate ip = ip.ip_content
@@ -221,58 +221,52 @@ let mk_logic_pointer_or_StartOf t =
Kernel.fatal ~source:(fst t.term_loc)
"%a is neither a pointer nor a C array" Cil_printer.pp_term t
-let need_logic_cast oldt newt =
- not (Cil_datatype.Logic_type.equal (Ctype oldt) (Ctype newt))
+let equal_ltype = Cil_datatype.Logic_type.equal
(* Does the same kind of optimization than [Cil.mkCastT] for [Ctype]. *)
-let mk_cast ?(loc=Cil_datatype.Location.unknown) ?(force=false) newt t =
- let mk_cast t = (* to new type [newt] *)
- let typ = Cil.type_remove_attributes_for_logic_type newt
- in term ~loc (TCastE (typ, t)) (Ctype typ)
- in
- let rec aux1 typ t =
- match typ with
- | Ctype oldt ->
- if not (need_logic_cast oldt newt) && not force then t
- else begin
- match Cil.unrollType newt, t.term_node with
- | TPtr _, TCastE (_, t') ->
- let rec aux2 = function
- | Ctype typ' ->
- (match unrollType typ', t'.term_node with
- | (TPtr _ as typ''), _ ->
- (* Old cast can be removed...*)
- if need_logic_cast newt typ'' then mk_cast t'
- else (* In fact, both casts can be removed. *) 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)
- | _ -> 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) 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 t
+let mk_cast ?loc ?(force=false) newt t =
+ let newt = Cil.type_remove_attributes_for_logic_type newt in
+ if equal_ltype (Ctype newt) t.term_type then t else
+ let rec unroll_cast e = match e.term_node with
+ | TCastE(oldt,e)
+ when (Cil.isPointerType newt && Cil.isPointerType oldt)
+ || equal_ltype (Ctype oldt) (Ctype newt)
+ -> unroll_cast e
+ | TLogic_coerce(Linteger,e)
+ when Cil.isArithmeticOrPointerType newt
+ -> unroll_cast e
+ | TLogic_coerce(Lreal,e)
+ when Cil.isFloatingType newt
+ -> unroll_cast e
+ | _ -> e
+ in
+ let tres = if force then t else unroll_cast t in
+ let loc = match loc with None -> t.term_loc | Some loc -> loc in
+ Logic_const.term ~loc (TCastE (newt, tres)) (Ctype newt)
+
+
+(* -------------------------------------------------------------------------- *)
+(* --- Constant Conversions --- *)
+(* -------------------------------------------------------------------------- *)
let real_of_float s f =
{ r_literal = s ; r_nearest = f ; r_upper = f ; r_lower = f }
+let real_of_parsed s p =
+ let open Floating_point in
+ {
+ r_literal = s ; r_nearest = p.f_nearest ;
+ r_upper = p.f_upper ;
+ r_lower = p.f_lower ;
+ }
+
let constant_to_lconstant c = match c with
| CInt64(i,_,s) -> Integer (i,s)
| CStr s -> LStr s
| CWStr s -> LWStr s
| CChr s -> LChr s
- | CReal (f,_,Some s) -> LReal (real_of_float s f)
| CEnum e -> LEnum e
+ | CReal (f,_,Some s) -> LReal (real_of_float s f)
| CReal (f,fkind,None) ->
let s = match fkind with
| FFloat -> Format.sprintf "%.8ef" f
@@ -288,49 +282,75 @@ let lconstant_to_constant c = match c with
| LReal r -> CReal (r.r_nearest,FDouble,Some r.r_literal)
| LEnum e -> CEnum e
-
-let string_to_float_lconstant string =
- let f = snd (Floating_point.parse string) in
+let parse_float ?loc literal =
+ let fk,v = Floating_point.parse literal in
(* If the string has suffix 'F' or 'D', then it represents a single or double
constant and the nearest parsed float is exact. Otherwise, use the upper
and lower float computed by [parse]. *)
- let l = String.length string - 1 in
- let last = Char.uppercase_ascii string.[l] in
- let exact = last = 'F' || last = 'D' in
- if exact
- then LReal (real_of_float string f.Floating_point.f_nearest)
- else
- let open Floating_point in
- LReal { r_nearest = f.f_nearest; r_upper = f.f_upper; r_lower = f.f_lower;
- r_literal = string }
-
-let numeric_coerce ltyp t =
- let coerce t =
- Logic_const.term ~loc:t.term_loc (TLogic_coerce(ltyp, t)) ltyp
+ let is_flt =
+ let len = String.length literal in
+ let last = Char.uppercase_ascii literal.[len-1] in
+ last = 'F' || last = 'D'
in
+ let creal =
+ if is_flt
+ then real_of_float literal v.Floating_point.f_nearest
+ else real_of_parsed literal v in
+ let vreal = Logic_const.term ?loc (TConst(LReal creal)) Lreal in
+ if is_flt then
+ let ty = TFloat(fk,[]) in
+ Logic_const.term ?loc (TCastE(ty,vreal)) (Ctype ty)
+ else vreal
+
+let mk_coerce ltyp t =
+ Logic_const.term ~loc:t.term_loc (TLogic_coerce(ltyp, t)) ltyp
+
+let rec numeric_coerce ltyp t =
let oldt = unroll_type t.term_type in
- if Cil_datatype.Logic_type.equal oldt ltyp then t
- else match t.term_node with
- | TLogic_coerce(t,e) when Cil.no_op_coerce t e -> coerce e
- | TConst(Integer(i,_)) ->
- (match oldt, ltyp with
- | Ctype (TInt(ikind,_)), Linteger when Cil.fitsInInt ikind i ->
- { t with term_type = Linteger }
- | _ -> coerce t)
- | TCastE(typ, ({ term_node = TConst(Integer(i,_))} as t')) ->
- (match unrollType typ with
- | TInt (ikind,_) when Cil.fitsInInt ikind i ->
- (match unroll_type t'.term_type with
- | Linteger -> t'
- | Ctype (TInt (ikind,_)) when Cil.fitsInInt ikind i ->
- { t' with term_type = Linteger }
- | _ -> coerce t')
- | _ -> coerce t)
- | _ -> coerce t
+ match t.term_node with
+ | TLogic_coerce(lt,e) when Cil.no_op_coerce lt e ->
+ (* coercion hidden by the printer, but still present *)
+ numeric_coerce ltyp e
+ | TConst(LEnum _) | TConst(Integer _) when ltyp = Linteger
+ -> { t with term_type = Linteger }
+ | TConst(LReal _ ) when ltyp = Lreal ->
+ { t with term_type = Lreal }
+ | TCastE(ty,e) ->
+ begin match ltyp, Cil.unrollType ty, e.term_node with
+ | Linteger, TInt(ik,_), TConst(Integer(v,_))
+ when Cil.fitsInInt ik v -> { e with term_type = Linteger }
+ | Lreal, TFloat(fk,_), TConst(LReal r)
+ when Cil.isExactFloat fk r -> { e with term_type = Lreal }
+ | Linteger, TInt(ik,_), TConst(LEnum { eival }) ->
+ ( match Cil.constFoldToInt eival with
+ | Some i when Cil.fitsInInt ik i -> { e with term_type = Linteger }
+ | _ -> mk_coerce ltyp t )
+ | _ -> mk_coerce ltyp t
+ end
+ | Trange(a,b) ->
+ let ra = numeric_bound ltyp a in
+ let rb = numeric_bound ltyp b in
+ { t with term_node = Trange(ra,rb) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | Tunion ts ->
+ { t with term_node = Tunion (List.map (numeric_coerce ltyp) ts) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | Tinter ts ->
+ { t with term_node = Tinter (List.map (numeric_coerce ltyp) ts) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | Tcomprehension(t,qs,cond) ->
+ { t with term_node = Tcomprehension (numeric_coerce ltyp t,qs,cond) ;
+ term_type = Logic_const.make_set_type ltyp }
+ | _ ->
+ if Cil_datatype.Logic_type.equal oldt ltyp then t
+ else mk_coerce ltyp t
+
+and numeric_bound ltyp = function
+ | None -> None
+ | Some a -> Some (numeric_coerce ltyp a)
(* Don't forget to keep is_zero_comparable
- and scalar_term_to_predicate in sync.
-*)
+ and scalar_term_to_predicate in sync. *)
let is_zero_comparable t =
match unroll_type t.term_type with
@@ -343,24 +363,27 @@ let is_zero_comparable t =
let scalar_term_conversion conversion t =
let loc = t.term_loc in
- let arith_conversion () = conversion ~loc false t (Cil.lzero ~loc ()) in
- let ptr_conversion () =
- conversion ~loc false t (Logic_const.term ~loc Tnull t.term_type)
- in
+ let int_conversion t =
+ conversion ~loc false t (Cil.lzero ~loc ()) in
+ let real_conversion ?ltyp t =
+ conversion ~loc false t (Logic_const.treal_zero ~loc ?ltyp ()) in
+ let ptr_conversion t =
+ conversion ~loc false t (Logic_const.term ~loc Tnull t.term_type) in
+ let bool_conversion t =
+ let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
+ conversion ~loc true t (term ~loc (TDataCons(ctrue,[])) boolean_type) in
match unroll_type t.term_type with
- | Ctype (TInt _) -> arith_conversion ()
- | Ctype (TFloat _) ->
- conversion ~loc false t (Logic_const.treal_zero ~loc ~ltyp:t.term_type ())
- | Ctype (TPtr _) -> ptr_conversion ()
- | Ctype (TArray _) -> ptr_conversion ()
+ | Ctype (TInt _) -> int_conversion t
+ | Ctype (TFloat _) as ltyp -> real_conversion ~ltyp t
+ | Ctype (TPtr _) -> ptr_conversion t
+ | Ctype (TArray _) -> ptr_conversion t
(* Could be transformed to \true: an array is never \null *)
- | Ctype (TFun _) -> ptr_conversion ()
+ | Ctype (TFun _) -> ptr_conversion t
(* decay as pointer *)
- | Linteger -> arith_conversion ()
- | Lreal -> conversion ~loc false t (Logic_const.treal_zero ~loc ())
+ | Linteger -> int_conversion t
+ | Lreal -> real_conversion t
| Ltype ({lt_name = name},[]) when name = Utf8_logic.boolean ->
- let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
- conversion ~loc true t (term ~loc (TDataCons(ctrue,[])) boolean_type)
+ bool_conversion t
| Ltype _ | Lvar _ | Larrow _
| Ctype (TVoid _ | TNamed _ | TComp _ | TEnum _ | TBuiltin_va_list _)
-> Kernel.fatal
@@ -379,131 +402,178 @@ let scalar_term_to_boolean =
in
scalar_term_conversion conversion
-let rec expr_to_term ~cast e =
- let e_typ = unrollType (Cil.typeOf e) in
+(* -------------------------------------------------------------------------- *)
+(* --- Expr Conversion --- *)
+(* -------------------------------------------------------------------------- *)
+
+let is_boolean_binop op =
+ let open Cil_types in
+ match op with
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> true
+ | PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP
+ | Mult | Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr -> false
+
+let float_builtin prefix fkind =
+ let name = match fkind with
+ | FFloat -> Printf.sprintf "\\%s_float" prefix
+ | FDouble -> Printf.sprintf "\\%s_double" prefix
+ | FLongDouble -> Kernel.not_yet_implemented "Builtins for long double type"
+ in match Logic_env.find_all_logic_functions name with
+ | [ lf ] -> Some lf
+ | _ -> Kernel.fatal "Missing or ambiguous builtin %S" name
+
+let get_float_binop op typ =
+ match Cil.unrollType typ, op with
+ | TFloat(fkind,_) , PlusA -> float_builtin "add" fkind
+ | TFloat(fkind,_) , MinusA -> float_builtin "sub" fkind
+ | TFloat(fkind,_) , Mult -> float_builtin "mul" fkind
+ | TFloat(fkind,_) , Div -> float_builtin "div" fkind
+ | _ -> None
+
+let get_float_unop op typ =
+ match Cil.unrollType typ, op with
+ | TFloat(fkind,_) , Neg -> float_builtin "neg" fkind
+ | _ -> None
+
+let rec expr_to_term ?(coerce=false) e =
let loc = e.eloc in
- let result = match e.enode with
- | Const c -> TConst (constant_to_lconstant c)
- | SizeOf t -> TSizeOf t
- | SizeOfE e -> TSizeOfE (expr_to_term ~cast e)
- | SizeOfStr s -> TSizeOfStr s
- | StartOf lv -> TStartOf (lval_to_term_lval ~cast lv)
- | AddrOf lv -> TAddrOf (lval_to_term_lval ~cast lv)
- | CastE (ty,e) -> (mk_cast (unrollType ty) (expr_to_term ~cast e)).term_node
- | BinOp (op, l, r, _) ->
- let l' = expr_to_term_coerce ~cast l in
- let r' = expr_to_term_coerce ~cast r in
- (* type of the conversion of e in the logic. Beware that boolean
- operators have boolean type. *)
- let tcast =
- match op, cast with
- | ( Cil_types.Lt | Cil_types.Gt | Cil_types.Le | Cil_types.Ge
- | Cil_types.Eq | Cil_types.Ne| Cil_types.LAnd | Cil_types.LOr),
- _ -> Some Logic_const.boolean_type
- | _, true -> Some (typ_to_logic_type e_typ)
- | _, false -> None
- in
- let tnode = TBinOp (op,l',r') in
- (* if [cast], we add a cast. Otherwise, when [op] is an operator
- returning a boolean, we need to cast the whole expression as an
- integral type, because (1) the recursive subcalls expect an
- integer/float/pointer here, and (2) there is no implicit conversion
- Boolean -> integer. *)
- begin match tcast with
- | Some lt -> (mk_cast e_typ (Logic_const.term tnode lt)).term_node
- | None -> tnode
+ let typ = Cil.typeOf e in
+ let ctyp = Ctype typ in
+ let node,ltyp =
+ match e.enode with
+ | Const c -> TConst (constant_to_lconstant c) , coerce_type typ
+ | StartOf lv -> TStartOf (lval_to_term_lval lv) , ctyp
+ | AddrOf lv -> TAddrOf (lval_to_term_lval lv) , ctyp
+ | BinOp (op, a, b, _) ->
+ if is_boolean_binop op then
+ let tc = expr_to_boolean e in
+ Tif( tc , Cil.lone ~loc () , Cil.lzero ~loc () ),
+ Linteger
+ else begin match get_float_binop op typ with
+ | Some phi ->
+ let va = expr_to_term a in
+ let vb = expr_to_term b in
+ Tapp(phi,[],[va;vb]) , ctyp
+ | None ->
+ let va = expr_to_term ~coerce:true a in
+ let vb = expr_to_term ~coerce:true b in
+ TBinOp(op,va,vb) , coerce_type typ
end
- | UnOp (op, u, _) ->
- let u' = expr_to_term_coerce ~cast u in
- let u' =
- match op with
- | Cil_types.LNot ->
- (match u'.term_node with
- | TCastE(_, t) when is_boolean_type t.term_type -> t
- | _ when is_boolean_type u'.term_type -> u'
- | _ when is_zero_comparable u' ->
- scalar_term_to_boolean u'
- | _ ->
- Kernel.fatal
- "expr_to_term: unexpected argument of ! operator %a, \
- converted to %a"
- Cil_printer.pp_exp u Cil_printer.pp_term u')
- | _ -> u'
- in
- (* See comments for binop case above. *)
- let tcast = match op, cast with
- | Cil_types.LNot, _ -> Some Logic_const.boolean_type
- | _, true -> Some (typ_to_logic_type e_typ)
- | _, false -> None
- in
- let tnode = TUnOp (op, u') in
- begin match tcast with
- | Some lt -> (mk_cast e_typ (Logic_const.term tnode lt)).term_node
- | None -> tnode
+ | UnOp (LNot, c, _) ->
+ let tc = expr_to_boolean c in
+ Tif( tc , Cil.lzero ~loc () , Cil.lone ~loc () ),
+ Linteger
+ | UnOp(op, a, _) ->
+ begin match get_float_unop op typ with
+ | Some phi ->
+ let va = expr_to_term ~coerce:true a in
+ Tapp(phi,[],[va]) , ctyp
+ | None ->
+ let va = expr_to_term ~coerce:true a in
+ TUnOp(op,va) , coerce_type typ
end
- | AlignOfE e -> TAlignOfE (expr_to_term ~cast e)
- | AlignOf typ -> TAlignOf typ
- | Lval lv -> TLval (lval_to_term_lval ~cast lv)
- | Info (e,_) -> (expr_to_term ~cast e).term_node
+ | SizeOf t -> TSizeOf t, ctyp
+ | SizeOfE e -> TSizeOf (Cil.typeOf e), ctyp
+ | SizeOfStr s -> TSizeOfStr s, ctyp
+ | AlignOf typ -> TAlignOf typ, ctyp
+ | AlignOfE e -> TAlignOf (Cil.typeOf e), ctyp
+ | Lval lv -> TLval (lval_to_term_lval lv), ctyp
+ | CastE (ty,e) ->
+ let coerce = Cil.isIntegralType (Cil.typeOf e) in
+ let t = mk_cast ~loc ty (expr_to_term ~coerce e) in
+ t.term_node , t.term_type
+ | Info (e,_) ->
+ let t = expr_to_term ~coerce e in
+ t.term_node , t.term_type
in
- let tres = Logic_const.term ~loc result (Ctype e_typ) in
- if cast then tres
- else
- match e.enode with
- (* all immediate values keep their C type by default, and are only lifted
- to integer/real if needed. *)
- | Const _ | Lval _ | CastE _ -> tres
- | _ -> numeric_coerce (typ_to_logic_type e_typ) tres
-
-and expr_to_term_coerce ~cast e =
- let t = expr_to_term ~cast e in
- match Logic_const.unroll_ltdef t.term_type with
- | Ctype typ when Cil.isIntegralType typ || Cil.isFloatingType typ ->
- let ltyp = typ_to_logic_type typ in
- numeric_coerce ltyp t
- | _ -> t
-
-and lval_to_term_lval ~cast (host,offset) =
- host_to_term_host ~cast host, offset_to_term_offset ~cast offset
-
-and host_to_term_host ~cast = function
+ let v = mk_cast ~loc typ @@ Logic_const.term ~loc node ltyp in
+ if coerce then
+ match Cil.unrollType typ with
+ | TInt _ -> numeric_coerce Linteger v
+ | TFloat _ -> numeric_coerce Lreal v
+ | _ -> v
+ else v
+
+and lval_to_term_lval (host,offset) =
+ host_to_term_lhost host, offset_to_term_offset offset
+
+and host_to_term_lhost = function
| Var s -> TVar (Cil.cvar_to_lvar s)
- | Mem e -> TMem (expr_to_term ~cast e) (*no need of numeric coercion - pointer *)
+ | Mem e -> TMem (expr_to_term e)
-and offset_to_term_offset ~cast:cast = function
+and offset_to_term_offset = function
| NoOffset -> TNoOffset
+ | Field (fi,off) ->
+ TField(fi,offset_to_term_offset off)
| Index (e,off) ->
- TIndex (expr_to_term_coerce ~cast e,offset_to_term_offset ~cast off)
- | Field (fi,off) -> TField(fi,offset_to_term_offset ~cast off)
+ TIndex (expr_to_term ~coerce:true e,offset_to_term_offset off)
-and expr_to_predicate ~cast e =
+and expr_to_boolean e =
let open Cil_types in
+ let tbool n = Logic_const.term n Logic_const.boolean_type in
match e.enode with
- | BinOp ((Lt | Gt | Le | Ge | Eq | Ne as op), l, r, _) ->
- let tl = expr_to_term ~cast l in
- let tr = expr_to_term ~cast r in
- let rel = match op with
- | Lt -> Rlt | Gt -> Rgt | Le -> Rle | Ge -> Rge | Eq -> Req | Ne -> Rneq
- | _ -> assert false
- in
- let pred = Prel (rel, tl, tr) in
- Logic_const.new_predicate (Logic_const.unamed ~loc:e.eloc pred)
+ | UnOp(BNot, a,_) ->
+ tbool @@ TUnOp(BNot, expr_to_boolean a)
+ | BinOp((BAnd|BOr) as op,a,b,_) ->
+ let va = expr_to_boolean a in
+ let vb = expr_to_boolean b in
+ tbool @@ TBinOp(op,va,vb)
+ | BinOp(op, a, b, _) when is_boolean_binop op ->
+ let va = expr_to_term ~coerce:true a in
+ let vb = expr_to_term ~coerce:true b in
+ tbool @@ TBinOp(op,va,vb)
| _ ->
- let t = expr_to_term ~cast e in
+ let t = expr_to_term ~coerce:true e in
if is_zero_comparable t then
- Logic_const.new_predicate (scalar_term_to_predicate t)
+ scalar_term_to_boolean t
else
Kernel.fatal
"Cannot convert into predicate the C expression %a"
Cil_printer.pp_exp e
+and expr_to_predicate e =
+ let open Cil_types in
+ let unamed = Logic_const.unamed ~loc:e.eloc in
+ let prel r a b =
+ let va = expr_to_term ~coerce:true a in
+ let vb = expr_to_term ~coerce:true b in
+ unamed @@ Prel(r,va,vb)
+ in match e.enode with
+ | BinOp(Lt, a, b, _) -> prel Rlt a b
+ | BinOp(Le, a, b, _) -> prel Rle a b
+ | BinOp(Gt, a, b, _) -> prel Rgt a b
+ | BinOp(Ge, a, b, _) -> prel Rge a b
+ | BinOp(Eq, a, b, _) -> prel Req a b
+ | BinOp(Ne, a, b, _) -> prel Rneq a b
+ | BinOp(BAnd, a, b, _) ->
+ unamed @@ Pand(expr_to_predicate a,expr_to_predicate b)
+ | BinOp(BOr, a, b, _) ->
+ unamed @@ Por(expr_to_predicate a,expr_to_predicate b)
+ | UnOp(BNot, a, _) ->
+ unamed @@ Pnot(expr_to_predicate a)
+ | _ ->
+ let t = expr_to_term ~coerce:true e in
+ if is_zero_comparable t then
+ scalar_term_to_predicate t
+ else
+ Kernel.fatal
+ "Cannot convert into predicate the C expression %a"
+ Cil_printer.pp_exp e
+
+and expr_to_ipredicate e =
+ Logic_const.new_predicate (expr_to_predicate e)
+
+(* ************************************************************************* *)
+(** {1 Various utilities} *)
+(* ************************************************************************* *)
+
let array_with_range arr size =
let loc = arr.eloc in
let arr = Cil.stripCasts arr in
let typ_arr = typeOf arr in
let no_cast = isAnyCharPtrType typ_arr || isAnyCharArrayType typ_arr in
- let char_ptr = typ_to_logic_type Cil.charPtrType in
- let arr = expr_to_term ~cast:true arr in
+ let char_ptr = Ctype Cil.charPtrType in
+ let arr = expr_to_term arr in
let arr =
if no_cast then arr
else mk_cast ~loc Cil.charPtrType arr
@@ -521,10 +591,6 @@ let remove_logic_coerce t =
| TLogic_coerce(_,t) -> t
| _ -> t
-(* ************************************************************************* *)
-(** {1 Various utilities} *)
-(* ************************************************************************* *)
-
let rec remove_term_offset o =
match o with
TNoOffset -> TNoOffset, TNoOffset
@@ -2592,6 +2658,8 @@ class simplify_const_lval global_find_init = object (self)
| _ -> Cil.DoChildren
end
+let () = Cil_datatype.punrollLogicType := unroll_type
+
(* ************************************************************************** *)
(** {1 Deprecated} *)
let instantiate = Logic_const.instantiate
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index b3a51cdf016276f06e81b7305fa266f6e1598e06..c147282eea5371d8178b2db61c985ce64e3da945 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -29,7 +29,7 @@ open Cil_types
(** exception raised when a parsed logic expression is
syntactically not well-formed. *)
-exception Not_well_formed of Cil_types.location * string
+exception Not_well_formed of location * string
(** basic utilities for logic terms and predicates. See also {! Logic_const}
to build terms and predicates.
@@ -85,8 +85,10 @@ val logicCType : logic_type -> typ
(** transforms an array into pointer. *)
val array_to_ptr : logic_type -> logic_type
-(** C type to logic type, with implicit conversion for arithmetic types. *)
-val typ_to_logic_type : typ -> logic_type
+(** C type to logic type, with implicit conversion for arithmetic types.
+ @since Frama-C+dev
+*)
+val coerce_type : typ -> logic_type
(** {2 Predicates} *)
@@ -109,7 +111,7 @@ val mk_logic_StartOf : term -> term
(** creates an AddrOf from a TLval. The given logic type is the
type of the lval.
@since Neon-20140301 *)
-val mk_logic_AddrOf: ?loc:Cil_types.location -> term_lval -> logic_type -> term
+val mk_logic_AddrOf: ?loc:location -> term_lval -> logic_type -> term
(** [true] if the term is a pointer. *)
val isLogicPointer : term -> bool
@@ -122,9 +124,7 @@ val mk_logic_pointer_or_StartOf : term -> term
be inserted. Otherwise (which is the default), [mk_cast typ t] will return
[t] if it is already of type [typ]
- @modify Aluminium-20160501 added [force] optional argument
-
-*)
+ @modify Aluminium-20160501 added [force] optional argument *)
val mk_cast: ?loc:location -> ?force:bool -> typ -> term -> term
@@ -141,7 +141,12 @@ val remove_logic_coerce: term -> term
in [t]. In particular, [numeric_coerce (int)cst Linteger], where [cst]
fits in int will be directly [cst], without any coercion.
+ Also coerce recursively the sub-terms of t-set expressions
+ (range, union, inter and comprehension) and lift the associated
+ set type.
+
@since Magnesium-20151001
+ @modify Frama-C+dev
*)
val numeric_coerce: logic_type -> term -> term
@@ -157,41 +162,77 @@ val pointer_comparable: ?loc:location -> term -> term -> predicate
(** \pointer_comparable
@since Fluorine-20130401 *)
-(** {3 Conversion from exp to term}*)
-(** translates a C expression into an "equivalent" logical term.
- [cast] specifies how C arithmetic operators are translated.
- When [cast] is [true], the translation returns a logic [term] having the
- same semantics of the C [expr] by introducing casts (i.e. the C expr [a+b]
- can be translated as [(char)(((char)a)+(char)b)] to preserve the modulo
- feature of the C addition).
- Otherwise, no such casts are introduced and the C arithmetic operators are
- translated into perfect mathematical operators (i.e. a floating point
- addition is translated into an addition of [real] numbers).
- @plugin development guide *)
-val expr_to_term : cast:bool -> exp -> term
-(** same as {!expr_to_term}, except that if the new term has an arithmetic
- type, it is automatically coerced into real (or integer for integral types).
+(** {2 Conversion from exp to term} *)
- @since Magnesium-20151001
+val expr_to_term : ?coerce:bool -> exp -> term
+(** Returns a logic term that has exactly the same semantics as the
+ original C-expression. The type of the resulting term is determined
+ by the [~coerce] flag as follows:
+ - when [~coerce:false] is given (the default) the term has the same
+ c-type as the original expression.
+ - when [~coerce:true] is given, if the original expression has an int or
+ float type, then the returned term is coerced into the integer or real
+ logic type, respectively.
+
+ Remark: when the original expression is a comparison, it is evaluated as
+ an [int] or an [integer] depending on the [~coerce] flag.
+ To obtain a boolean or predicate, use [expr_to_boolean] or
+ [expr_to_predicate] instead.
+
+ @modify Frama-C+dev
*)
-val expr_to_term_coerce: cast:bool -> exp -> term
-val is_zero_comparable: term -> bool
-(** [true] if the given term has a type for which a comparison to 0 exists
- (i.e. scalar C types, logic integers and reals).
+val expr_to_predicate: exp -> predicate
+(** Returns a predicate semantically equivalent to the condition
+ of the original C-expression.
+
+ This is different from [expr_to_term e |> scalar_term_to_predicate]
+ since C-relations are translated into logic ones.
+ @raise Fatal error if the expression is not a comparison and cannot be
+ compared to zero.
@since Sulfur-20171101
+ @modify Frama-C+dev
*)
-val expr_to_predicate: cast:bool -> exp -> identified_predicate
-(** same as {expr_to_term}, but the result is a predicate. Expressions starting
- with relational operators ([==], [<=], etc) are translated directly.
- Otherwise, the result of [expr_to_predicate e] is the predicate
- [e <> 0].
+val expr_to_ipredicate: exp -> identified_predicate
+(** Returns a predicate semantically equivalent to the condition
+ of the original C-expression.
+
+ Identical to [expr_to_predicate e |> Logic_const.new_predicate].
@raise Fatal error if the expression is not a comparison and cannot be
compared to zero.
@since Sulfur-20171101
+ @modify Frama-C+dev
+*)
+
+val expr_to_boolean: exp -> term
+(** Returns a boolean term semantically equivalent to the condition
+ of the original C-expression.
+
+ This is different from [expr_to_term e |> scalar_term_to_predicate]
+ since C-relations are translated into logic ones.
+
+ @raise Fatal error if the expression is not a comparison and cannot be
+ compared to zero.
+ @since Sulfur-20171101
+ @modify Frama-C+dev
+*)
+
+val is_zero_comparable: term -> bool
+(** [true] if the given term has a type for which a comparison to 0 exists
+ (i.e. scalar C types, logic integers and reals).
+
+ @since Sulfur-20171101
+*)
+
+val scalar_term_to_boolean: term -> term
+(** Compare the given term with the constant 0 (of the appropriate type)
+ to return the result of the comparison [e <> 0] as a boolean term.
+
+ @raise Fatal error if the argument cannot be compared to 0
+ @since Frama-C+dev
*)
val scalar_term_to_predicate: term -> predicate
@@ -202,19 +243,25 @@ val scalar_term_to_predicate: term -> predicate
@since Sulfur-20171101
*)
-val lval_to_term_lval : cast:bool -> lval -> term_lval
-val host_to_term_host : cast:bool -> lhost -> term_lhost
-val offset_to_term_offset :
- cast:bool -> offset -> term_offset
+val lval_to_term_lval : lval -> term_lval
+val host_to_term_lhost : lhost -> term_lhost
+val offset_to_term_offset : offset -> term_offset
val constant_to_lconstant: constant -> logic_constant
val lconstant_to_constant: logic_constant-> constant
-(** Parse the given string as a float logic constant, taking into account
- the fact that the constant may not be exactly representable. This
- function should only be called on strings that have been recognized
- by the parser as valid floats *)
-val string_to_float_lconstant: string -> logic_constant
+(** Parse the given string as a float or real logic constant.
+
+ The parsed literal is always kept as it is in the resulting term.
+ The returned term is either a real constant or
+ real constant casted into a C-float type.
+
+ Unsuffixed literals are considered as real numbers.
+ Literals suffixed by [f|d|l] or [F|D|L] are considered
+ as float constants of the associated kind. *)
+val parse_float : ?loc:location -> string -> term
+
+(** {2 Various Utilities} *)
(** [remove_term_offset o] returns [o] without its last offset and
this last offset. *)
@@ -240,8 +287,6 @@ val is_result : term -> bool
val lhost_c_type : term_lhost -> typ
-(** {2 Predicates} *)
-
(** [true] if the predicate is Ptrue.
@since Nitrogen-20111001 *)
val is_trivially_true: predicate -> bool
@@ -371,7 +416,7 @@ val concat_allocation: allocation -> allocation -> allocation
val merge_allocation : allocation -> allocation -> allocation
val merge_behaviors :
- ?oldloc:Cil_types.location -> silent:bool -> funbehavior list -> funbehavior list -> funbehavior list
+ ?oldloc:location -> silent:bool -> funbehavior list -> funbehavior list -> funbehavior list
(** [merge_funspec ?oldloc oldspec newspec] merges [newspec] into [oldspec].
If the funspec belongs to a kernel function, do not forget to call
@@ -379,7 +424,7 @@ val merge_behaviors :
@modify 20.0-Calcium add optional parameter [oldloc].
*)
val merge_funspec :
- ?oldloc:Cil_types.location -> ?silent_about_merging_behav:bool ->
+ ?oldloc:location -> ?silent_about_merging_behav:bool ->
funspec -> funspec -> unit
(** Reset the given funspec to empty.
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index b35db0760de8d187a2808397456db0636c0cfb48..36adae8427fe37790298e9a576b3e4847eaba0a6 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -96,7 +96,7 @@ let inline_call loc caller callee return args =
method! vterm_lval (host,offset) =
match host, return with
| TResult _, Some lv ->
- let tlv = Logic_utils.lval_to_term_lval ~cast:false lv in
+ let tlv = Logic_utils.lval_to_term_lval lv in
let offset = Visitor.visitFramacTermOffset self offset in
Cil.ChangeToPost
(Logic_const.addTermOffsetLval offset tlv, Extlib.id)
diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml
index 1b4d343a4de8e0c948bb89f997546fad3dd86318..13227afdd5da5ff1abadabed250a4c13aff26dd2 100644
--- a/src/libraries/utils/floating_point.ml
+++ b/src/libraries/utils/floating_point.ml
@@ -41,10 +41,10 @@ external set_rounding_mode: c_rounding_mode -> unit = "set_rounding_mode" "noall
[@@@ warning "+3"]
-external round_to_single_precision_float: float -> float = "round_to_float"
-external sys_single_precision_of_string: string -> float =
- "single_precision_of_string"
-(* TODO two functions above: declare "float",
+external round_to_single_precision_float: float -> float = "round_to_float"
+external sys_single_precision_of_string: string -> float =
+ "single_precision_of_string"
+(* TODO two functions above: declare "float",
must have separate version for bytecode, see OCaml manual *)
let max_single_precision_float = Int32.float_of_bits 0x7f7fffffl
@@ -56,16 +56,16 @@ type parsed_float = {
f_upper : float ;
}
-let inf ~man_size ~max_exp =
+let inf ~man_size ~max_exp =
let biggest_not_inf = ldexp (2.0 -. ldexp 1.0 (~- man_size)) max_exp in
- {
+ {
f_lower = biggest_not_inf ;
f_nearest = infinity ;
f_upper = infinity ;
}
(* [s = num * 2^exp / den] hold *)
-let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
+let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
assert (Integer.gt num Integer.zero);
assert (Integer.gt den Integer.zero);
(*
@@ -78,7 +78,7 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
let den = ref den in
let exp = ref exp in
- while
+ while
Integer.ge num (Integer.shift_left !den ssize_bi)
|| !exp < min_exp
do
@@ -88,7 +88,7 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
let den = !den in
let shifted_den = Integer.shift_left den size_bi in
let num = ref num in
- while
+ while
Integer.lt !num shifted_den && !exp > min_exp
do
num := Integer.shift_left !num Integer.one;
@@ -96,7 +96,7 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
done;
let num = !num in
let exp = !exp in
-(*
+(*
Format.printf "make_float2: num den exp:@\n%a@\n@\n%a@\n@\n%d@."
Datatype.Integer.pretty num Datatype.Integer.pretty den exp;
*)
@@ -107,9 +107,9 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
Integer.shift_left rem Integer.one
in
let man = Integer.to_int64 man in
-(* Format.printf "pre-round: num den man rem:@\n%a@\n@\n%a@\n@\n%Ld@\n@\n%a@."
- Datatype.Integer.pretty num Datatype.Integer.pretty den
- man Datatype.Integer.pretty rem; *)
+ (* Format.printf "pre-round: num den man rem:@\n%a@\n@\n%a@\n@\n%Ld@\n@\n%a@."
+ Datatype.Integer.pretty num Datatype.Integer.pretty den
+ man Datatype.Integer.pretty rem; *)
let lowb = ldexp (Int64.to_float man) exp in
if Integer.is_zero rem2 then {
f_lower = lowb ;
@@ -118,16 +118,16 @@ let make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp =
} else
let upb = ldexp (Int64.to_float (Int64.succ man)) exp in
if Integer.lt rem2 den ||
- (Integer.equal rem2 den && (Int64.logand man Int64.one) = 0L)
+ (Integer.equal rem2 den && (Int64.logand man Int64.one) = 0L)
then {
- f_lower = lowb ;
- f_nearest = lowb ;
- f_upper = upb ;
+ f_lower = lowb ;
+ f_nearest = lowb ;
+ f_upper = upb ;
}
else {
- f_lower = lowb ;
- f_nearest = upb ;
- f_upper = upb ;
+ f_lower = lowb ;
+ f_nearest = upb ;
+ f_upper = upb ;
}
let reg_exp = "[eE][+]?\\(-?[0-9]+\\)"
@@ -154,66 +154,66 @@ let parse_float ~man_size ~min_exp ~max_exp s =
with Failure _ ->
(* Format.printf "Error in exponent: %s@." s; *)
if s.[0] = '-'
- then raise (Shortcut {
- f_lower = 0.0 ;
- f_nearest = 0.0 ;
- f_upper = ldexp 1.0 (min_exp - man_size) ;
- })
+ then raise (Shortcut {
+ f_lower = 0.0 ;
+ f_nearest = 0.0 ;
+ f_upper = ldexp 1.0 (min_exp - man_size) ;
+ })
else raise (Shortcut (inf ~man_size ~max_exp))
in
- try
- (* At the end of the function, [s = num * 2^exp / den] *)
- let num, den, exp =
- if Str.string_match numdotfracexp s 0
- then
- let n = Str.matched_group 1 s in
- let frac = Str.matched_group 2 s in
- let len_frac = String.length frac in
- let num = Integer.of_string (n ^ frac) in
- let den = Integer.power_int_positive_int 5 len_frac in
- if Integer.is_zero num then raise (Shortcut zero);
- let exp10 = match_exp 3
- in
- if exp10 >= 0
- then
- Integer.mul num (Integer.power_int_positive_int 5 exp10),
- den,
- exp10 - len_frac
- else
- num,
- Integer.mul den (Integer.power_int_positive_int 5 (~- exp10)),
- exp10 - len_frac
- else if Str.string_match numdotfrac s 0
- then
- let n = Str.matched_group 1 s in
- let frac = Str.matched_group 2 s in
- let len_frac = String.length frac in
- Integer.of_string (n ^ frac),
- Integer.power_int_positive_int 5 len_frac,
- ~- len_frac
- else if Str.string_match numexp s 0
- then
- let n = Str.matched_group 1 s in
- let num = Integer.of_string n in
- if Integer.is_zero num then raise (Shortcut zero);
- let exp10 = match_exp 2 in
- if exp10 >= 0
- then
- Integer.mul num (Integer.power_int_positive_int 5 exp10),
- Integer.one,
- exp10
- else
- num,
- (Integer.power_int_positive_int 5 (~- exp10)),
- exp10
- else (Format.printf "Could not parse floating point number %S@." s;
- assert false)
- in
- if Integer.is_zero num
- then zero
- else
- make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp
- with Shortcut r -> r
+ try
+ (* At the end of the function, [s = num * 2^exp / den] *)
+ let num, den, exp =
+ if Str.string_match numdotfracexp s 0
+ then
+ let n = Str.matched_group 1 s in
+ let frac = Str.matched_group 2 s in
+ let len_frac = String.length frac in
+ let num = Integer.of_string (n ^ frac) in
+ let den = Integer.power_int_positive_int 5 len_frac in
+ if Integer.is_zero num then raise (Shortcut zero);
+ let exp10 = match_exp 3
+ in
+ if exp10 >= 0
+ then
+ Integer.mul num (Integer.power_int_positive_int 5 exp10),
+ den,
+ exp10 - len_frac
+ else
+ num,
+ Integer.mul den (Integer.power_int_positive_int 5 (~- exp10)),
+ exp10 - len_frac
+ else if Str.string_match numdotfrac s 0
+ then
+ let n = Str.matched_group 1 s in
+ let frac = Str.matched_group 2 s in
+ let len_frac = String.length frac in
+ Integer.of_string (n ^ frac),
+ Integer.power_int_positive_int 5 len_frac,
+ ~- len_frac
+ else if Str.string_match numexp s 0
+ then
+ let n = Str.matched_group 1 s in
+ let num = Integer.of_string n in
+ if Integer.is_zero num then raise (Shortcut zero);
+ let exp10 = match_exp 2 in
+ if exp10 >= 0
+ then
+ Integer.mul num (Integer.power_int_positive_int 5 exp10),
+ Integer.one,
+ exp10
+ else
+ num,
+ (Integer.power_int_positive_int 5 (~- exp10)),
+ exp10
+ else (Format.printf "Could not parse floating point number %S@." s;
+ assert false)
+ in
+ if Integer.is_zero num
+ then zero
+ else
+ make_float ~num ~den ~exp ~man_size ~min_exp ~max_exp
+ with Shortcut r -> r
let is_hex s =
let l = String.length s in
@@ -224,7 +224,7 @@ let opp_parse_float f =
let rec single_precision_of_string s =
if s.[0] = '-' then
- opp_parse_float (single_precision_of_string (String.sub s 1 (String.length s - 1)))
+ opp_parse_float (single_precision_of_string (String.sub s 1 (String.length s - 1)))
else if is_hex s
then
try
@@ -236,11 +236,11 @@ let rec single_precision_of_string s =
parse_float ~man_size:23 ~min_exp:(-126) ~max_exp:127 s
(* May raise Failure("float_of_string"). *)
-let rec double_precision_of_string s =
+let rec double_precision_of_string s =
if s.[0] = '-' then
opp_parse_float (double_precision_of_string (String.sub s 1 (String.length s - 1)))
else if is_hex s
- then
+ then
let f = float_of_string s in
{ f_lower = f ; f_nearest = f ; f_upper = f }
else (* decimal *)
@@ -274,6 +274,14 @@ let parse string =
Kernel.fatal ~current:true
"Unexpected error parsing floating-point constant: %s." string
+let has_suffix fk lit =
+ let s = match fk with
+ | Cil_types.FFloat -> 'F'
+ | Cil_types.FDouble -> 'D'
+ | Cil_types.FLongDouble -> 'L' in
+ let ln = String.length lit in
+ ln > 0 && Char.uppercase_ascii lit.[ln-1] = s
+
let pretty_normal ~use_hex fmt f =
let double_norm = Int64.shift_left 1L 52 in
let double_mask = Int64.pred double_norm in
@@ -285,62 +293,62 @@ let pretty_normal ~use_hex fmt f =
let s = if s then "-" else "" in
if exp = 2047
then begin
- if man = 0L
- then
- Format.fprintf fmt "%sinf" s
- else
- Format.fprintf fmt "NaN"
- end
+ if man = 0L
+ then
+ Format.fprintf fmt "%sinf" s
+ else
+ Format.fprintf fmt "NaN"
+ end
else
- let firstdigit, exp =
- if exp <> 0
- then 1, (exp - 1023)
- else 0, if f = 0. then 0 else -1022
- in
- if not use_hex
- then begin
+ let firstdigit, exp =
+ if exp <> 0
+ then 1, (exp - 1023)
+ else 0, if f = 0. then 0 else -1022
+ in
+ if not use_hex
+ then begin
let firstdigit, man, exp =
- if 0 < exp && exp <= 12
- then begin
- Int64.to_int
- (Int64.shift_right_logical
- (Int64.logor man double_norm)
- (52 - exp)),
- Int64.logand (Int64.shift_left man exp) double_mask,
- 0
- end
- else firstdigit, man, exp
+ if 0 < exp && exp <= 12
+ then begin
+ Int64.to_int
+ (Int64.shift_right_logical
+ (Int64.logor man double_norm)
+ (52 - exp)),
+ Int64.logand (Int64.shift_left man exp) double_mask,
+ 0
+ end
+ else firstdigit, man, exp
in
let d =
- Int64.float_of_bits
- (Int64.logor 0x3ff0000000000000L man)
+ Int64.float_of_bits
+ (Int64.logor 0x3ff0000000000000L man)
in
let d, re =
- if d >= 1.5
- then d -. 1.5, 5000000000000000L
- else d -. 1.0, 0L
+ if d >= 1.5
+ then d -. 1.5, 5000000000000000L
+ else d -. 1.0, 0L
in
let d = d *. 1e16 in
let decdigits = Int64.add re (Int64.of_float d) in
if exp = 0 || (firstdigit = 0 && decdigits = 0L && exp = -1022)
then
- Format.fprintf fmt "%s%d.%016Ld"
- s
- firstdigit
- decdigits
+ Format.fprintf fmt "%s%d.%016Ld"
+ s
+ firstdigit
+ decdigits
else
- Format.fprintf fmt "%s%d.%016Ld*2^%d"
- s
- firstdigit
- decdigits
- exp
+ Format.fprintf fmt "%s%d.%016Ld*2^%d"
+ s
+ firstdigit
+ decdigits
+ exp
end
- else
- Format.fprintf fmt "%s0x%d.%013Lxp%d"
- s
- firstdigit
- man
- exp
+ else
+ Format.fprintf fmt "%s0x%d.%013Lxp%d"
+ s
+ firstdigit
+ man
+ exp
let pretty fmt f =
let use_hex = Kernel.FloatHex.get() in
@@ -354,15 +362,15 @@ let pretty fmt f =
then
pretty_normal ~use_hex fmt f
else begin
- let r = Format.sprintf "%.*g" 12 f in
- if (String.contains r '.' || String.contains r 'e' ||
- String.contains r 'E')
- || (match classify_float f with
- | FP_normal | FP_subnormal | FP_zero -> false
- | FP_infinite | FP_nan -> true)
- then Format.pp_print_string fmt r
- else Format.fprintf fmt "%s." r
- end
+ let r = Format.sprintf "%.*g" 12 f in
+ if (String.contains r '.' || String.contains r 'e' ||
+ String.contains r 'E')
+ || (match classify_float f with
+ | FP_normal | FP_subnormal | FP_zero -> false
+ | FP_infinite | FP_nan -> true)
+ then Format.pp_print_string fmt r
+ else Format.fprintf fmt "%s." r
+ end
type sign = Neg | Pos
@@ -373,12 +381,12 @@ exception Float_Non_representable_as_Int64 of sign
raise Float_Non_representable_as_Int64. This is the most reasonable as
a floating-point number may represent an exponentially large integer. *)
let truncate_to_integer =
- let min_64_float = -9.22337203685477581e+18
- (* Int64.to_float (-0x8000000000000000L) *)
+ let min_64_float = -9.22337203685477581e+18
+ (* Int64.to_float (-0x8000000000000000L) *)
in
- let max_64_float = 9.22337203685477478e+18
-(* let open Int64 in
- float_of_bits (pred (bits_of_float (to_float max_int))) *)
+ let max_64_float = 9.22337203685477478e+18
+ (* let open Int64 in
+ float_of_bits (pred (bits_of_float (to_float max_int))) *)
in
fun x ->
let max_64_float = Extlib.id max_64_float in
@@ -388,10 +396,10 @@ let truncate_to_integer =
then raise (Float_Non_representable_as_Int64 Pos);
if x <= max_64_float then
Integer.of_int64 (Int64.of_float x)
- else
- Integer.add
- (Integer.of_int64 (Int64.of_float (x +. min_64_float)))
- (Integer.two_power_of_int 63)
+ else
+ Integer.add
+ (Integer.of_int64 (Int64.of_float (x +. min_64_float)))
+ (Integer.two_power_of_int 63)
let bits_of_max_double =
Integer.of_int64 (Int64.bits_of_float max_float)
diff --git a/src/libraries/utils/floating_point.mli b/src/libraries/utils/floating_point.mli
index 27a4bbbe39e94fe81019c1dd91c0fffdfe8108e8..11190c51425225feeae0faece5c12928f0090c90 100644
--- a/src/libraries/utils/floating_point.mli
+++ b/src/libraries/utils/floating_point.mli
@@ -30,8 +30,8 @@ val string_of_c_rounding_mode : c_rounding_mode -> string
external set_round_downward : unit -> unit = "set_round_downward" [@@noalloc]
external set_round_upward : unit -> unit = "set_round_upward" [@@noalloc]
-external set_round_nearest_even : unit -> unit =
- "set_round_nearest_even" [@@noalloc]
+external set_round_nearest_even : unit -> unit =
+ "set_round_nearest_even" [@@noalloc]
external set_round_toward_zero : unit -> unit =
"set_round_toward_zero" [@@noalloc]
external get_rounding_mode: unit -> c_rounding_mode =
@@ -49,8 +49,8 @@ val neg_min_denormal: float
val min_single_precision_denormal: float
val neg_min_single_precision_denormal: float
-external sys_single_precision_of_string: string -> float =
- "single_precision_of_string"
+external sys_single_precision_of_string: string -> float =
+ "single_precision_of_string"
(** If [s] is parsed as [(n, l, u)], then [n] is the nearest approximation of
@@ -69,6 +69,10 @@ type parsed_float = {
with no suffix are parsed as double. *)
val parse: string -> Cil_types.fkind * parsed_float
+(** Checks if the (uppercased) string ends with an explicit [F|D|L]
+ suffix corresponding to the given float kind. *)
+val has_suffix: Cil_types.fkind -> string -> bool
+
val pretty_normal : use_hex : bool -> Format.formatter -> float -> unit
val pretty : Format.formatter -> float -> unit
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index e869e3dd345b390b1adb58a48de5e25640ec7918..554af1f3639ad3531632e0f8dfec0de3e106852b 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -449,7 +449,7 @@ module Computer(I: Init) = struct
"too few arguments in call to %a" Printer.pp_varinfo f
| p::prms, a::args ->
let lv = Logic_const.tvar (Cil.cvar_to_lvar p) in
- let la = Logic_utils.expr_to_term ~cast:false a in
+ let la = Logic_utils.expr_to_term a in
let value =
Cil_datatype.Term.Map.add
la (Fixed 0) Cil_datatype.Term.Map.empty
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index ff3c2f3a3fe3dc68bc2950443cd8239b67c67f37..c4fb25191c1f4b7f166ad3666763e6eff90a1aa1 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -138,7 +138,7 @@ let isCrossableAtInit tr func =
let rec aux t =
match t.term_node with
| TConst (LEnum ei) ->
- aux (Logic_utils.expr_to_term ~cast:false ei.eival)
+ aux (Logic_utils.expr_to_term ei.eival)
| TLval lv ->
(match aux_lv lv with
| Some t -> t
@@ -241,7 +241,7 @@ let isCrossableAtInit tr func =
and aux_init off initinfo =
match off, initinfo with
| TNoOffset, SingleInit e ->
- Some (aux (Logic_utils.expr_to_term ~cast:false e))
+ Some (aux (Logic_utils.expr_to_term e))
| TIndex(t,oth), CompoundInit (ct,initl) ->
(match (aux t).term_node with
| TConst(Integer(i1,_)) ->
@@ -653,7 +653,7 @@ let one_term () = Cil.lconstant Integer.one
(** Returns a term representing the variable associated to the given varinfo *)
let mk_term_from_vi vi =
Logic_const.term
- (TLval((Logic_utils.lval_to_term_lval ~cast:true (Cil.var vi))))
+ (TLval((Logic_utils.lval_to_term_lval (Cil.var vi))))
(Ctype Cil.intType)
(** Given an lval term 'host' and an integer value 'off', it returns a lval term host[off]. *)
@@ -681,8 +681,7 @@ let mk_offseted_array_states_as_enum host off =
(Ctype Cil.intType)
(** Returns a lval term associated to the curState generated variable. *)
-let host_state_term() =
- lval_to_term_lval ~cast:true (state_lval())
+let host_state_term() = lval_to_term_lval (state_lval())
(*
(** Returns a lval term associated to the curStateOld generated variable. *)
let host_stateOld_term () =
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 75999fabf9b8be5f91d9ad19b06ce43e34311214..1bcaa67755f6727b12a02562f4759ac52095f220 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -694,8 +694,7 @@ let type_expr env ?tr ?current e =
let e = Cil.parseIntLogic ~loc s in
env, e, cond
| PCst (Logic_ptree.FloatConstant str) ->
- let c = Logic_utils.string_to_float_lconstant str in
- env, Logic_const.term (TConst c) Lreal, cond
+ env, Logic_utils.parse_float ~loc str, cond
| PCst (Logic_ptree.StringConstant s) ->
let t =
Logic_const.term
diff --git a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
index 2e24eb7f8a7502ffb36cad5f670b90fc673a2b01..b850086cbe94dbafa142e58f40a017022d73a22c 100644
--- a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
@@ -581,24 +581,26 @@ int g(int y)
ensures
\at(aorai_CurStates ≡ init,Pre) ∧
aorai_CurStates ≡ aorai_reject ⇒
- aorai_x_0 ≡ \at(1,Pre) + 0 ∨ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0;
+ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0 ∨
+ aorai_x_0 ≡ \at((int)1,Pre) + 0;
ensures
\at(aorai_CurStates ≡ init,Pre) ∧
aorai_CurStates ≡ aorai_reject ⇒
- aorai_y ≡ \at(2,Pre) + 0 ∨ aorai_y ≡ \at(aorai_y,Pre) + 0;
+ aorai_y ≡ \at(aorai_y,Pre) + 0 ∨ aorai_y ≡ \at((int)2,Pre) + 0;
ensures
\at(aorai_CurStates ≡ init,Pre) ∧
aorai_CurStates ≡ aorai_reject ⇒
- aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at(aorai_x,Pre) + 0;
+ aorai_x ≡ \at(aorai_x,Pre) + 0 ∨ aorai_x ≡ \at((int)1,Pre) + 0;
ensures
\at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
- aorai_x_0 ≡ \at(1,Pre) + 0 ∨ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0;
+ aorai_x_0 ≡ \at(aorai_x_0,Pre) + 0 ∨
+ aorai_x_0 ≡ \at((int)1,Pre) + 0;
ensures
\at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
- aorai_y ≡ \at(2,Pre) + 0 ∨ aorai_y ≡ \at(aorai_y,Pre) + 0;
+ aorai_y ≡ \at(aorai_y,Pre) + 0 ∨ aorai_y ≡ \at((int)2,Pre) + 0;
ensures
\at(aorai_CurStates ≡ init,Pre) ∧ aorai_CurStates ≡ OK ⇒
- aorai_x ≡ \at(1,Pre) + 0 ∨ aorai_x ≡ \at(aorai_x,Pre) + 0;
+ aorai_x ≡ \at(aorai_x,Pre) + 0 ∨ aorai_x ≡ \at((int)1,Pre) + 0;
*/
int main(void)
{
diff --git a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle b/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
index 91b4e2cc2ad540571330772e709520258a653f9b..480cdbac3e337e91a9a7e27ca0dee315fdfe892b 100644
--- a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
@@ -525,7 +525,12 @@ void g(void)
behavior buch_state_last_out:
ensures 0 ≡ last;
+ behavior buch_state_step1_in:
+ assumes 1 ≡ init ∧ x ≡ 3;
+ ensures 1 ≡ step1;
+
behavior buch_state_step1_out:
+ assumes 0 ≡ init ∨ ¬(x ≡ 3);
ensures 0 ≡ step1;
@/
void main_pre_func(void)
@@ -538,7 +543,9 @@ void g(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- step1_tmp = 0;
+ if (init == 1)
+ if (x == 3) step1_tmp = 1; else step1_tmp = 0;
+ else step1_tmp = 0;
last_tmp = 0;
if (init == 1)
if (x != 3) init_tmp = 1; else init_tmp = 0;
@@ -644,7 +651,6 @@ void g(void)
*/
/*@ requires 1 ≡ init ∧ 0 ≡ last ∧ 0 ≡ step1;
- requires 1 ≡ init ⇒ x ≢ 3;
behavior aorai_acceptance:
ensures 1 ≡ last;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
index 0b02e09b98b4a40aafb0895b7524d3459d38496c..ceb8eed7a93e5cd46801202607b737a163b9b95f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
@@ -13,7 +13,7 @@
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
+ assert \initialized(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
@@ -24,7 +24,8 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_3 +
- ((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
+ (int)((int)(__gen_e_acsl_v - -5) - 1)));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:31: Warning:
@@ -33,7 +34,8 @@
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
+ assert
+ \initialized(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
@@ -44,17 +46,19 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
- ((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
+ (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:45: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
+ assert \initialized(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+ assert
+ \initialized(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
@@ -63,7 +67,7 @@
function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
accessing uninitialized left-value.
- assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
+ assert \initialized(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
@@ -74,9 +78,9 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_7 +
- ((__gen_e_acsl_u_5 - 10) * 300 +
- (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
- ((__gen_e_acsl_w - 100) - 1))));
+ (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +
+ (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) * 100)
+ + (int)((int)(__gen_e_acsl_w - 100) - 1))));
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:54: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/at_on-purely-logic-variables.c:63: Warning:
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
index 007bc6daa68fc06d4f1f28ab9f26eb013b76aefb..17dee7105453488b730f112a3de0e6c604b8eeae 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
@@ -56,7 +56,7 @@ void g(void)
"tests/arith/at_on-purely-logic-variables.c",16);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
+ \initialized(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
*/
if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ;
else {
@@ -240,7 +240,7 @@ int main(void)
"tests/arith/at_on-purely-logic-variables.c",29);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
+ \initialized(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
*/
if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ;
else {
@@ -289,8 +289,8 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_3 +
- ((__gen_e_acsl_u - 9) * 11 +
- ((__gen_e_acsl_v - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
+ (int)((int)(__gen_e_acsl_v - -5) - 1)));
*/
if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
__gen_e_acsl_v - -5) - 1))))
@@ -374,7 +374,8 @@ int main(void)
"tests/arith/at_on-purely-logic-variables.c",41);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
+ \initialized(__gen_e_acsl_at_5 +
+ (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
*/
if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
;
@@ -427,8 +428,9 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_6 +
- ((__gen_e_acsl_u_3 - 9) * 32 +
- ((__gen_e_acsl_v_3 - -5) - 1)));
+ (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32)
+ +
+ (int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
*/
if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
(__gen_e_acsl_v_3 - -5) - 1))))
@@ -514,9 +516,17 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_7 +
- ((__gen_e_acsl_u_5 - 10) * 300 +
- (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
- ((__gen_e_acsl_w - 100) - 1))));
+ (int)((int)((int)(__gen_e_acsl_u_5 - 10) *
+ 300)
+ +
+ (int)((int)((int)((int)(__gen_e_acsl_v_5
+ - -10)
+ - 1)
+ * 100)
+ +
+ (int)((int)(__gen_e_acsl_w -
+ 100)
+ - 1))));
*/
if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + (
((__gen_e_acsl_v_5 - -10) - 1) * 100 + (
@@ -650,7 +660,8 @@ void __gen_e_acsl_f(int *t)
"tests/arith/at_on-purely-logic-variables.c",7);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
+ \initialized(__gen_e_acsl_at +
+ (int)((int)(__gen_e_acsl_n - 1) - 1));
*/
if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
int __gen_e_acsl_valid_read_2;
@@ -665,7 +676,8 @@ void __gen_e_acsl_f(int *t)
"tests/arith/at_on-purely-logic-variables.c",7);
/*@ assert
Eva: initialization:
- \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
+ \initialized(__gen_e_acsl_at_2 +
+ (int)((int)(__gen_e_acsl_n - 1) - 1));
*/
__gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
}
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index bd22a341b9b2fb5c25072ebb4b661bfbbac0f19f..7943b9907d694f73cfb478d604c04ca8a7ded3e2 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -57,9 +57,9 @@ int main(void)
__gmpq_clear(__gen_e_acsl__4);
}
/*@ assert 0.1 ≡ 0.1; */ ;
- __e_acsl_assert(1,"Assertion","main","(double)1.0 == 1.0",
+ __e_acsl_assert(1,"Assertion","main","1.0 == 1.0",
"tests/arith/rationals.c",14);
- /*@ assert (double)1.0 ≡ 1.0; */ ;
+ /*@ assert 1.0 ≡ 1.0; */ ;
{
__e_acsl_mpq_t __gen_e_acsl__5;
double __gen_e_acsl__6;
diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
index 259afb2e7cf7aff685e3f821c94a0a230968a678..47e55d3fc12d7dc4c433a4048dc6a87d3fe16138 100644
--- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
@@ -8,7 +8,7 @@ struct list {
/*@
logic ℤ length_aux{L}(struct list *l, ℤ n) =
\at(n < 0? -1:
- (l ≡ (struct list *)((void *)0)? n:
+ (l ≡ (struct list *)0? n:
(n < 2147483647? length_aux(l->next, n + 1): -1)),
L);
*/
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
index a7e98e9b92928f184ef61762e98d62f6f344b6f4..60fc5642381eca2bf0accc0e9093530f27e8f3c0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
@@ -57,25 +57,25 @@ int main(int argc, char **argv)
"__e_acsl_heap_allocation_size == 16",
"tests/memory/memsize.c",50);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
- __e_acsl_assert(b == (char *)0,"Assertion","main",
- "b == (char *)((void *)0)","tests/memory/memsize.c",51);
- /*@ assert b ≡ (char *)((void *)0); */ ;
+ __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
+ "tests/memory/memsize.c",51);
+ /*@ assert b ≡ (char *)0; */ ;
b = (char *)calloc(18446744073709551615UL,18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
"tests/memory/memsize.c",55);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
- __e_acsl_assert(b == (char *)0,"Assertion","main",
- "b == (char *)((void *)0)","tests/memory/memsize.c",56);
- /*@ assert b ≡ (char *)((void *)0); */ ;
+ __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
+ "tests/memory/memsize.c",56);
+ /*@ assert b ≡ (char *)0; */ ;
b = (char *)malloc(18446744073709551615UL);
__e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
"__e_acsl_heap_allocation_size == 16",
"tests/memory/memsize.c",60);
/*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
- __e_acsl_assert(b == (char *)0,"Assertion","main",
- "b == (char *)((void *)0)","tests/memory/memsize.c",61);
- /*@ assert b ≡ (char *)((void *)0); */ ;
+ __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
+ "tests/memory/memsize.c",61);
+ /*@ assert b ≡ (char *)0; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml
index 660db8c83c08e4939599cbd5819d41428f31515f..744917afbad2aef97acbe6cf1e75c29ba33873a0 100644
--- a/src/plugins/instantiate/basic_blocks.ml
+++ b/src/plugins/instantiate/basic_blocks.ml
@@ -131,7 +131,7 @@ let rec tunref_range ?loc ptr len =
and tunref_range_unfold ?loc lval typ =
match typ with
| Ctype(TArray(typ, Some e, _, _)) ->
- let len = Logic_utils.expr_to_term ~cast:false e in
+ let len = Logic_utils.expr_to_term ~coerce:true e in
let last = tminus ?loc len (tinteger ?loc 1) in
let range = trange ?loc (Some (tinteger ?loc 0), Some last) in
let lval = addTermOffsetLval (TIndex(range, TNoOffset)) lval in
@@ -218,7 +218,7 @@ and pall_elems_eq ?loc depth t1 t2 len =
and peq_unfold ?loc depth t1 t2 =
match Logic_utils.unroll_type t1.term_type with
| Ctype(TArray(_, Some len, _, _)) ->
- let len = Logic_utils.expr_to_term ~cast:false len in
+ let len = Logic_utils.expr_to_term ~coerce:true len in
pall_elems_eq ?loc depth t1 t2 len
| _ -> prel ?loc (Req, t1, t2)
@@ -236,7 +236,7 @@ and punfold_pred ?loc ?(dyn_len = None) depth t1 pred =
| Ctype(TArray(_, opt_len, _, _)) ->
let len =
match opt_len, dyn_len with
- | Some len, None -> Logic_utils.expr_to_term ~cast:false len
+ | Some len, None -> Logic_utils.expr_to_term ~coerce:true len
| _ , Some len -> len
| None, None ->
Options.fatal "Unfolding array: cannot find a length"
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index aafb865f3497f88cab6436031f261d94e62c2a72..d7b8da68dfc8abe36b54c7f5c9b0073c70a51d49 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -127,7 +127,7 @@ let occurrence_highlighter buffer loc ~start ~stop =
| PTermLval (_,ki,_,term_lval) ->
let same_tlval (_kf, k, l) =
Logic_utils.is_same_tlval
- (Logic_utils.lval_to_term_lval ~cast:true l)
+ (Logic_utils.lval_to_term_lval l)
term_lval
&& Kinstr.equal k ki
in
diff --git a/src/plugins/studia/studia_gui.ml b/src/plugins/studia/studia_gui.ml
index a235a6f490b520aa0db97e6cac358fc885b0e5fc..65638eed8780190662e21de733954378956fda8c 100644
--- a/src/plugins/studia/studia_gui.ml
+++ b/src/plugins/studia/studia_gui.ml
@@ -54,7 +54,7 @@ let get_lval_opt main_ui kf localizable =
match localizable with
| Pretty_source.PLval (Some _kf, (Kstmt _stmt), lv) ->
let lv_txt = Pretty_utils.to_string Printer.pp_lval lv in
- let tlv = Logic_utils.lval_to_term_lval ~cast:false lv in
+ let tlv = Logic_utils.lval_to_term_lval lv in
Some (lv_txt, tlv)
| Pretty_source.PTermLval (Some _kf, (Kstmt _stmt), _, tlv) ->
let tlv_txt = Pretty_utils.to_string Printer.pp_term_lval tlv in
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index de5887617b6b296e62609fe8fbe67d6ae974e4fb..c7cb5f5219d7ce702517e27cfac0d85b2b665b05 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -1080,10 +1080,12 @@ let rec stmts_of_cfg cfg current var_map locals return_exp acc =
| Assume (_, exp,b) ->
let exp = subst_in_exp var_map exp in
- let predicate = (Logic_utils.expr_to_predicate ~cast:true exp).Cil_types.ip_content in
+ let predicate = Logic_utils.expr_to_predicate exp in
let predicate = if b then predicate else Logic_const.pnot predicate in
- let code_annot = Logic_const.new_code_annotation(Cil_types.AAssert([],Assert,predicate)) in
- let stmt = Cil.mkStmtOneInstr ~valid_sid (Cil_types.Code_annot(code_annot,dummy_loc)) in
+ let code_node = Cil_types.AAssert([],Assert,predicate) in
+ let code_annot = Logic_const.new_code_annotation code_node in
+ let stmt_kind = Cil_types.Code_annot(code_annot,exp.eloc) in
+ let stmt = Cil.mkStmtOneInstr ~valid_sid stmt_kind in
stmts_of_cfg cfg n var_map locals return_exp (stmt::acc)
| EnterScope (_, vs) ->
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 995160e34820fe6858f6c4b5531d0d3aaf55efd4..0ae0bdbccedbff18dc04bfd431d88799bb18ad93 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -720,6 +720,16 @@ let known_logic_funs = [
"\\sign", ACSL;
"\\min", ACSL;
"\\max", ACSL;
+ "\\neg_float",ACSL;
+ "\\add_float",ACSL;
+ "\\sub_float",ACSL;
+ "\\mul_float",ACSL;
+ "\\div_float",ACSL;
+ "\\neg_double",ACSL;
+ "\\add_double",ACSL;
+ "\\sub_double",ACSL;
+ "\\mul_double",ACSL;
+ "\\div_double",ACSL;
]
let known_predicates = [
"\\warning", ACSL;
@@ -1354,11 +1364,13 @@ and eval_known_logic_function ~alarm_mode env li labels args =
eval_logic_charchr builtin
{ env with e_cur = lbl } s.eover c.eover s.ldeps c.ldeps
- | ("atan2" | "atan2f" | "fmod" | "fmodf" | "pow" | "powf"),
+ | ( "atan2" | "atan2f" | "fmod" | "fmodf" | "pow" | "powf"
+ | "\\add_float" | "\\sub_float" | "\\mul_float" | "\\div_float"
+ | "\\add_double" | "\\sub_double" | "\\mul_double" | "\\div_double" ),
_, _, [arg1; arg2] ->
eval_float_builtin_arity2 ~alarm_mode env lvi.lv_name arg1 arg2
- | ("sqrt" | "sqrtf"),_,_, [arg] ->
+ | ( "sqrt" | "sqrtf" | "\\neg_float" | "\\neg_double" ),_,_, [arg] ->
eval_float_builtin_arity1 ~alarm_mode env lvi.lv_name arg
| "\\sign", _, _, [arg] ->
@@ -1410,6 +1422,14 @@ and eval_float_builtin_arity2 ~alarm_mode env name arg1 arg2 =
| "fmodf" -> Fval.fmod Fval.Single
| "pow" -> Fval.pow Fval.Double
| "powf" -> Fval.pow Fval.Single
+ | "\\add_float" -> Fval.add Fval.Single
+ | "\\sub_float" -> Fval.sub Fval.Single
+ | "\\mul_float" -> Fval.mul Fval.Single
+ | "\\div_float" -> Fval.div Fval.Single
+ | "\\add_double" -> Fval.add Fval.Double
+ | "\\sub_double" -> Fval.sub Fval.Double
+ | "\\mul_double" -> Fval.mul Fval.Double
+ | "\\div_double" -> Fval.div Fval.Double
| _ -> assert false
in
let r1 = eval_term ~alarm_mode env arg1 in
@@ -1432,6 +1452,7 @@ and eval_float_builtin_arity1 ~alarm_mode env name arg =
let fcaml = match name with
| "sqrt" -> Fval.sqrt Fval.Double
| "sqrtf" -> Fval.sqrt Fval.Single
+ | "\\neg_float" | "\\neg_double" -> Fval.neg
| _ -> assert false
in
let r = eval_term ~alarm_mode env arg in
diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 39c437ff77f71ad07bd77057f2652d8c9e10f289..64e1cfd7065d4bd0a9de71a2afe0eb99abc6de41 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -91,6 +91,7 @@ type op =
| NE
| NEG
| ADD
+ | SUB
| MUL
| DIV
| REAL
@@ -105,6 +106,7 @@ let op_name = function
| NE -> "ne"
| NEG -> "neg"
| ADD -> "add"
+ | SUB -> "sub"
| MUL -> "mul"
| DIV -> "div"
| REAL -> "of"
@@ -275,6 +277,7 @@ let compute_float op ulp xs =
match op , xs with
| NEG , [ x ] -> qmake ulp (Q.neg (exact x))
| ADD , [ x ; y ] -> qmake ulp (Q.add (exact x) (exact y))
+ | SUB , [ x ; y ] -> qmake ulp (Q.sub (exact x) (exact y))
| MUL , [ x ; y ] -> qmake ulp (Q.mul (exact x) (exact y))
| DIV , [ x ; y ] ->
let res = match Q.div (exact x) (exact y) with
@@ -293,6 +296,7 @@ let compute_real op xs =
match op , xs with
| NEG , [ x ] -> F.e_opp x
| ADD , [ x ; y ] -> F.e_add x y
+ | SUB , [ x ; y ] -> F.e_sub x y
| MUL , [ x ; y ] -> F.e_mul x y
| DIV , [ x ; y ] -> F.e_div x y
| (ROUND|REAL) , [ x ] -> x
@@ -350,36 +354,51 @@ let flt_le ft = Compute.get (Context.get model, ft, LE) |> fst
let flt_lt ft = Compute.get (Context.get model, ft, LT) |> fst
let flt_neg ft = Compute.get (Context.get model, ft, NEG) |> fst
let flt_add ft = Compute.get (Context.get model, ft, ADD) |> fst
+let flt_sub ft = Compute.get (Context.get model, ft, SUB) |> fst
let flt_mul ft = Compute.get (Context.get model, ft, MUL) |> fst
let flt_div ft = Compute.get (Context.get model, ft, DIV) |> fst
let flt_of_real ft = Compute.get (Context.get model, ft, ROUND) |> fst
let real_of_flt ft = Compute.get (Context.get model, ft, REAL) |> fst
-
(* -------------------------------------------------------------------------- *)
(* --- Builtins --- *)
(* -------------------------------------------------------------------------- *)
-let make_hack ?(converse=false) ft op xs =
+let builtin kind ft op xs =
let phi, impl = Compute.get ((Context.get model), ft, op) in
- let xs = (if converse then List.rev xs else xs) in
- try impl xs with Not_found -> F.e_fun ~result:Logic.Bool phi xs
-
-let register_builtin ft =
+ let xs = (if kind=`ReV then List.rev xs else xs) in
+ try impl xs with Not_found ->
+ let result = match kind with
+ | `Binop | `Unop -> ftau ft
+ | `Rel | `ReV -> Logic.Bool
+ in F.e_fun ~result phi xs
+
+let register_builtins ft =
begin
let suffix = float_name ft in
- LogicBuiltins.hack ("\\eq_" ^ suffix) (make_hack ft EQ) ;
- LogicBuiltins.hack ("\\ne_" ^ suffix) (make_hack ft NE) ;
- LogicBuiltins.hack ("\\lt_" ^ suffix) (make_hack ~converse:false ft LT) ;
- LogicBuiltins.hack ("\\gt_" ^ suffix) (make_hack ~converse:true ft LT) ;
- LogicBuiltins.hack ("\\le_" ^ suffix) (make_hack ~converse:false ft LE) ;
- LogicBuiltins.hack ("\\ge_" ^ suffix) (make_hack ~converse:true ft LE)
+ let register (prefix,kind,op) =
+ LogicBuiltins.hack
+ (Printf.sprintf "\\%s_%s" prefix suffix)
+ (builtin kind ft op)
+ in List.iter register [
+ "eq",`Rel,EQ ;
+ "ne",`Rel,NE ;
+ "lt",`Rel,LT ;
+ "gt",`ReV,LT ;
+ "le",`Rel,LE ;
+ "ge",`ReV,LE ;
+ "neg",`Unop,NEG ;
+ "add",`Binop,ADD ;
+ "sub",`Binop,SUB ;
+ "mul",`Binop,MUL ;
+ "div",`Binop,DIV ;
+ ] ;
end
let () = Context.register
begin fun () ->
- register_builtin Float32 ;
- register_builtin Float64 ;
+ register_builtins Float32 ;
+ register_builtins Float64 ;
end
(* -------------------------------------------------------------------------- *)
@@ -435,16 +454,14 @@ let fcmp rop fop f x y =
| Float -> p_call (fop f) [x;y]
let fadd = fbinop e_add flt_add
+let fsub = fbinop e_sub flt_sub
let fmul = fbinop e_mul flt_mul
let fdiv = fbinop e_div flt_div
-
let fopp f x =
match Context.get model with
| Real -> e_opp x
| Float -> e_fun ~result:(ftau f) (flt_neg f) [x]
-let fsub f x y = fadd f x (fopp f y)
-
let flt = fcmp p_lt flt_lt
let fle = fcmp p_leq flt_le
let feq = fcmp p_equal flt_eq
diff --git a/src/plugins/wp/Cfloat.mli b/src/plugins/wp/Cfloat.mli
index 344ddbc093e210b08c1b87114f4252cd21da307d..c685e9139ea638eadb6cf2a49ddc946c0033e8f1 100644
--- a/src/plugins/wp/Cfloat.mli
+++ b/src/plugins/wp/Cfloat.mli
@@ -50,6 +50,7 @@ type op =
| NE
| NEG
| ADD
+ | SUB
| MUL
| DIV
| REAL
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 2a90684fe56e03ce94cd24a994d39dcbd468ac59..b15809c85bbac7dcbec5579d9e967a96fb5452de 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -1027,7 +1027,7 @@ struct
(* -------------------------------------------------------------------------- *)
let assigned_of_lval env ~unfold (lv : Cil_types.lval) =
- assignable_lval env ~unfold (Logic_utils.lval_to_term_lval ~cast:false lv)
+ assignable_lval env ~unfold (Logic_utils.lval_to_term_lval lv)
let assigned_of_froms env ~unfold froms =
List.concat
diff --git a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
index 3cfc3d7f07f7a38907537385c65ad9b590d72ee1..3f1bc5eb1b79440418007e44bed89924f9feb01a 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
@@ -145,10 +145,15 @@ theory Cfloat
function add_f32 (x:f32) (y:f32) : f32 = F32.(.+) x y
function add_f64 (x:f64) (y:f64) : f64 = F64.(.+) x y
+ (* Substraction *)
+
+ function sub_f32 (x:f32) (y:f32) : f32 = F32.(.-) x y
+ function sub_f64 (x:f64) (y:f64) : f64 = F64.(.-) x y
+
(* Multiplication *)
- function mul_f32 (x:f32) (y:f32) : f32 = F32.(.-) x y
- function mul_f64 (x:f64) (y:f64) : f64 = F64.(.-) x y
+ function mul_f32 (x:f32) (y:f32) : f32 = F32.(.*) x y
+ function mul_f64 (x:f64) (y:f64) : f64 = F64.(.*) x y
(* Division *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
index bd279cccc874f2274d8dfb05d4b76eb7d82e8dac..4249f034461a465c794b76fe03bd9cf26e1fa735 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/float_real.1.res.oracle
@@ -13,11 +13,11 @@
Goal Post-condition (file tests/wp_plugin/float_real.i, line 14) in 'dequal':
Assume {
Type: is_sint32(dequal_0).
- If lt_f64(add_f64(x, neg_f64(y)),
+ If lt_f64(sub_f64(x, y),
to_f64((5902958103587057.0/590295810358705651712)))
Then {
If lt_f64(to_f64((-5902958103587057.0/590295810358705651712)),
- add_f64(x, neg_f64(y)))
+ sub_f64(x, y))
Then { (* Return *) Have: dequal_0 = 1. }
Else { (* Return *) Have: dequal_0 = 0. }
}
diff --git a/tests/float/oracle/alarms.0.res.oracle b/tests/float/oracle/alarms.0.res.oracle
index 9cc4fd7b226e6f9d01374c4a2e35ca0abb4daf25..27b0de1e56c15f5a8d1abf36a81c6fa15903de14 100644
--- a/tests/float/oracle/alarms.0.res.oracle
+++ b/tests/float/oracle/alarms.0.res.oracle
@@ -71,17 +71,21 @@
[eva] computing for function main2 <- main.
Called from tests/float/alarms.i:71.
[eva:alarm] tests/float/alarms.i:38: Warning:
- non-finite double value. assert \is_finite((double)(1. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0.));
[eva:alarm] tests/float/alarms.i:39: Warning:
- non-finite double value. assert \is_finite((double)(0. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)0., (double)0.));
[eva] tests/float/alarms.i:41: assertion got status valid.
[eva] tests/float/alarms.i:42: assertion got status valid.
[eva] tests/float/alarms.i:43: assertion got status valid.
[eva] tests/float/alarms.i:44: assertion got status valid.
[eva:alarm] tests/float/alarms.i:46: Warning:
- non-finite double value. assert \is_finite((double)(1. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0.));
[eva:alarm] tests/float/alarms.i:50: Warning:
- non-finite double value. assert \is_finite((double)(0. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)0., (double)0.));
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
diff --git a/tests/float/oracle/alarms.1.res.oracle b/tests/float/oracle/alarms.1.res.oracle
index 6fe539d768879d442082f6ce346e5b3180b05dcb..0aa572dcab50325f861c33dfaf8bb25391255d73 100644
--- a/tests/float/oracle/alarms.1.res.oracle
+++ b/tests/float/oracle/alarms.1.res.oracle
@@ -71,14 +71,14 @@
[eva] computing for function main2 <- main.
Called from tests/float/alarms.i:71.
[eva:alarm] tests/float/alarms.i:39: Warning:
- NaN double value. assert ¬\is_NaN((double)(0. / 0.));
+ NaN double value. assert ¬\is_NaN(\div_double((double)0., (double)0.));
[eva] tests/float/alarms.i:41: assertion got status valid.
[eva] tests/float/alarms.i:42: assertion got status valid.
[eva] tests/float/alarms.i:43: assertion got status valid.
[eva] tests/float/alarms.i:44: assertion got status valid.
[eva] tests/float/alarms.i:47: assertion got status valid.
[eva:alarm] tests/float/alarms.i:50: Warning:
- NaN double value. assert ¬\is_NaN((double)(0. / 0.));
+ NaN double value. assert ¬\is_NaN(\div_double((double)0., (double)0.));
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
diff --git a/tests/float/oracle/const1.res.oracle b/tests/float/oracle/const1.res.oracle
index 638364e24627ee9b5d7d0801c6943a7deef32246..a88cc5055cf3dfb3a54b5ebaeb7be3a190c8416c 100644
--- a/tests/float/oracle/const1.res.oracle
+++ b/tests/float/oracle/const1.res.oracle
@@ -5,7 +5,7 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/float/const1.i:1: Warning:
- non-finite float value. assert \is_finite(1e40f);
+ non-finite float value. assert \is_finite((float)1e40f);
[eva] tests/float/const1.i:1: Warning:
evaluation of initializer '(unsigned long long)1e40f' failed
[eva] Initial state computed
diff --git a/tests/float/oracle/const2.res.oracle b/tests/float/oracle/const2.res.oracle
index e13374c9a69087e2f5b5eff971800610a94ce188..cbf8617870807c9608359bb8ee92ea09c49c562b 100644
--- a/tests/float/oracle/const2.res.oracle
+++ b/tests/float/oracle/const2.res.oracle
@@ -5,7 +5,7 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/float/const2.i:2: Warning:
- non-finite float value. assert \is_finite(1e40f);
+ non-finite float value. assert \is_finite((float)1e40f);
[eva] tests/float/const2.i:2: Warning: evaluation of initializer '1e40f' failed
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
diff --git a/tests/float/oracle/const4.0.res.oracle b/tests/float/oracle/const4.0.res.oracle
index fc3b0e788b83ec9cef38524e8ef6c8d2c18b7d70..7c1da402c214766126e2154048502a9670f28337 100644
--- a/tests/float/oracle/const4.0.res.oracle
+++ b/tests/float/oracle/const4.0.res.oracle
@@ -6,7 +6,7 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/float/const4.i:7: Warning:
- non-finite float value. assert \is_finite(3.405e38f);
+ non-finite float value. assert \is_finite((float)3.405e38f);
[eva] tests/float/const4.i:7: Warning:
evaluation of initializer '(double)3.405e38f' failed
[eva] Initial state computed
diff --git a/tests/float/oracle/const4.1.res.oracle b/tests/float/oracle/const4.1.res.oracle
index 5005f2e7aa3a9f83fbe7f95abebf0de23fce17ae..7f1381022516acfaa8fa4bc0e640684d198fd245 100644
--- a/tests/float/oracle/const4.1.res.oracle
+++ b/tests/float/oracle/const4.1.res.oracle
@@ -6,7 +6,7 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva:alarm] tests/float/const4.i:7: Warning:
- non-finite float value. assert \is_finite(3.405e38f);
+ non-finite float value. assert \is_finite((float)3.405e38f);
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
f1 ∈ [3.39999995214e+38 .. 3.40000015497e+38]
diff --git a/tests/float/oracle/cte_overflow.res.oracle b/tests/float/oracle/cte_overflow.res.oracle
index c0a3a0173b1e8461e25b19cec61e96b8eef45052..0aea223139cefa7745d90fe73a8131275a75f10c 100644
--- a/tests/float/oracle/cte_overflow.res.oracle
+++ b/tests/float/oracle/cte_overflow.res.oracle
@@ -13,9 +13,9 @@
[eva:initial-state] Values of globals at initialization
v ∈ [--..--]
[eva:alarm] tests/float/cte_overflow.i:12: Warning:
- non-finite double value. assert \is_finite(1e500);
+ non-finite double value. assert \is_finite((double)1e500);
[eva:alarm] tests/float/cte_overflow.i:17: Warning:
- non-finite float value. assert \is_finite(1e80f);
+ non-finite float value. assert \is_finite((float)1e80f);
[eva] Recording results for main
[eva] done for function main
[eva] tests/float/cte_overflow.i:12:
diff --git a/tests/float/oracle/dr_infinity.res.oracle b/tests/float/oracle/dr_infinity.res.oracle
index 1a2c304b3a2ed57f309868e5ace5067283845272..04bd0c13b12f6668575bba0d156fc44b92520016 100644
--- a/tests/float/oracle/dr_infinity.res.oracle
+++ b/tests/float/oracle/dr_infinity.res.oracle
@@ -22,28 +22,33 @@
v ∈ [--..--]
[eva] tests/float/dr_infinity.i:9: Frama_C_show_each: {0x1.fffffe0000000p127}
[eva:alarm] tests/float/dr_infinity.i:11: Warning:
- non-finite float value. assert \is_finite((float)3.402823567797366e+38);
+ non-finite float value.
+ assert \is_finite((float)((double)3.402823567797366e+38));
[eva:alarm] tests/float/dr_infinity.i:16: Warning:
- non-finite float value. assert \is_finite((float)(x * x));
+ non-finite float value. assert \is_finite(\mul_float(x, x));
[eva:alarm] tests/float/dr_infinity.i:21: Warning:
- non-finite double value. assert \is_finite((double)(d * (double)10));
+ non-finite double value. assert \is_finite(\mul_double(d, (double)10));
[eva:alarm] tests/float/dr_infinity.i:26: Warning:
- non-finite double value. assert \is_finite((double)((double)2 / d));
+ non-finite double value. assert \is_finite(\div_double((double)2, d));
[eva:alarm] tests/float/dr_infinity.i:31: Warning:
- non-finite double value. assert \is_finite((double)(d / 0.01));
+ non-finite double value. assert \is_finite(\div_double(d, (double)0.01));
[eva:alarm] tests/float/dr_infinity.i:36: Warning:
non-finite float value.
- assert \is_finite((float)((double)((double)x / 0.001)));
+ assert \is_finite((float)\div_double((double)x, (double)0.001));
[eva:alarm] tests/float/dr_infinity.i:41: Warning:
- non-finite double value. assert \is_finite((double)(d / 0.));
+ non-finite double value. assert \is_finite(\div_double(d, (double)0.));
[eva] Recording results for main
[eva] done for function main
[eva] tests/float/dr_infinity.i:11:
assertion 'Eva,is_nan_or_infinite' got final status invalid.
[eva] tests/float/dr_infinity.i:16:
assertion 'Eva,is_nan_or_infinite' got final status invalid.
+[eva] tests/float/dr_infinity.i:21:
+ assertion 'Eva,is_nan_or_infinite' got final status invalid.
[eva] tests/float/dr_infinity.i:26:
assertion 'Eva,is_nan_or_infinite' got final status invalid.
+[eva] tests/float/dr_infinity.i:31:
+ assertion 'Eva,is_nan_or_infinite' got final status invalid.
[eva] tests/float/dr_infinity.i:36:
assertion 'Eva,is_nan_or_infinite' got final status invalid.
[eva] tests/float/dr_infinity.i:41:
diff --git a/tests/float/oracle/logic.0.res.oracle b/tests/float/oracle/logic.0.res.oracle
index a78dc74e8eaac554d264eb78a2b28fffc8e7de2c..2f18d3f38e7ca97d1ac9afb26c914f3f1a72783a 100644
--- a/tests/float/oracle/logic.0.res.oracle
+++ b/tests/float/oracle/logic.0.res.oracle
@@ -59,7 +59,8 @@
[eva:alarm] tests/float/logic.i:42: Warning: check got status invalid.
[eva:alarm] tests/float/logic.i:43: Warning: check got status invalid.
[eva:alarm] tests/float/logic.i:45: Warning:
- non-finite double value. assert \is_finite((double)(1. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0.));
[eva:alarm] tests/float/logic.i:64: Warning: check got status unknown.
[eva:alarm] tests/float/logic.i:65: Warning: check got status unknown.
[eva:alarm] tests/float/logic.i:66: Warning: check got status unknown.
@@ -314,7 +315,8 @@
[eva] Recording results for test_comparison_reduction
[eva] Done for function test_comparison_reduction
[eva:alarm] tests/float/logic.i:133: Warning:
- non-finite double value. assert \is_finite((double)(1. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0.));
[eva] Recording results for test_builtin_comparisons
[eva] Done for function test_builtin_comparisons
[eva] computing for function test_is_finite <- main.
diff --git a/tests/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 5e60b7a32e5ff2014f7a279f2b314b5969f31798..b3c87ee207887a60ae61edd6f4c1cd84e13ffc73 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -171,10 +171,10 @@
[eva] Done for function Frama_C_float_interval
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert 0 ≤ (int)((double)((double)(i * i) + 2.0));
+ assert 0 ≤ (int)\add_double(\mul_double(i, i), (double)2.0);
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert (int)((double)((double)(i * i) + 2.0)) < 10;
+ assert (int)\add_double(\mul_double(i, i), (double)2.0) < 10;
[eva] computing for function access_bits <- other <- main.
Called from tests/float/nonlin.c:69.
[eva] Recording results for access_bits
@@ -195,8 +195,9 @@
[eva:alarm] tests/float/nonlin.c:77: Warning:
non-finite double value.
assert
- \is_finite((double)((double)1 /
- (double)((double)((double)ff * (double)ff) + 0.000000001)));
+ \is_finite(\div_double((double)1,
+ \add_double(\mul_double((double)ff, (double)ff),
+ (double)0.000000001)));
[eva] Recording results for split_alarm
[eva] Done for function split_alarm
[eva] computing for function norm <- main.
@@ -220,12 +221,12 @@
function Frama_C_float_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_float_interval
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v1 * v1));
+ non-finite float value. assert \is_finite(\mul_float(v1, v1));
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v2 * v2));
+ non-finite float value. assert \is_finite(\mul_float(v2, v2));
[eva:alarm] tests/float/nonlin.c:92: Warning:
non-finite float value.
- assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
+ assert \is_finite(\add_float(\mul_float(v1, v1), \mul_float(v2, v2)));
[eva] Recording results for norm
[eva] Done for function norm
[eva] computing for function garbled <- main.
@@ -243,7 +244,7 @@
[eva:alarm] tests/float/nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] tests/float/nonlin.c:99: Warning:
- non-finite float value. assert \is_finite((float)(a_0 + a_0));
+ non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva] tests/float/nonlin.c:99:
Assigning imprecise value to f.
The imprecision originates from Arithmetic
@@ -260,7 +261,8 @@
[eva] Done for function Frama_C_float_interval
[eva:alarm] tests/float/nonlin.c:113: Warning:
non-finite float value.
- assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
+ assert
+ \is_finite(\div_float(f1, \sub_float(\sub_float(\add_float(f, f), f), f1)));
[eva] Recording results for around_zeros
[eva] Done for function around_zeros
[eva] computing for function subdivide_strategy <- main.
@@ -276,7 +278,7 @@
non-finite double value. assert \is_finite(nondet);
[eva:alarm] tests/float/nonlin.c:135: Warning:
non-finite double value.
- assert \is_finite((double)((double)(x_0 - d_0) * (double)(x_0 - d_0)));
+ assert \is_finite(\mul_double(\sub_double(x_0, d_0), \sub_double(x_0, d_0)));
[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
Called from tests/float/nonlin.c:136.
[eva] tests/float/nonlin.c:136:
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 036f8d26e43e182434e95dcde6ced28107a6d3bb..6116e8b7c3b2828b99b91740ccf3ea2d0374e39e 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -177,7 +177,7 @@
[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert (int)((double)((double)(i * i) + 2.0)) < 10;
+ assert (int)\add_double(\mul_double(i, i), (double)2.0) < 10;
[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
@@ -243,12 +243,12 @@
[eva:nonlin] tests/float/nonlin.c:92: subdividing on v1
[eva:nonlin] tests/float/nonlin.c:92: subdividing on v2
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v1 * v1));
+ non-finite float value. assert \is_finite(\mul_float(v1, v1));
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v2 * v2));
+ non-finite float value. assert \is_finite(\mul_float(v2, v2));
[eva:alarm] tests/float/nonlin.c:92: Warning:
non-finite float value.
- assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
+ assert \is_finite(\add_float(\mul_float(v1, v1), \mul_float(v2, v2)));
[eva] Recording results for norm
[eva] Done for function norm
[eva] computing for function garbled <- main.
@@ -266,7 +266,7 @@
[eva:alarm] tests/float/nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] tests/float/nonlin.c:99: Warning:
- non-finite float value. assert \is_finite((float)(a_0 + a_0));
+ non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva] tests/float/nonlin.c:99:
Assigning imprecise value to f.
The imprecision originates from Arithmetic
@@ -287,7 +287,8 @@
[eva:nonlin] tests/float/nonlin.c:113: subdividing on f
[eva:alarm] tests/float/nonlin.c:113: Warning:
non-finite float value.
- assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
+ assert
+ \is_finite(\div_float(f1, \sub_float(\sub_float(\add_float(f, f), f), f1)));
[eva] Recording results for around_zeros
[eva] Done for function around_zeros
[eva] computing for function subdivide_strategy <- main.
@@ -308,7 +309,7 @@
[eva:nonlin] tests/float/nonlin.c:135: subdividing on x_0
[eva:alarm] tests/float/nonlin.c:135: Warning:
non-finite double value.
- assert \is_finite((double)((double)(x_0 - d_0) * (double)(x_0 - d_0)));
+ assert \is_finite(\mul_double(\sub_double(x_0, d_0), \sub_double(x_0, d_0)));
[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
Called from tests/float/nonlin.c:136.
[eva] tests/float/nonlin.c:136:
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 112f643e8810a8acfb5c96421196df65e43d7fe5..15dfbc52f71215bca7c9d87879422e69575dc601 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -177,7 +177,7 @@
[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert (int)((double)((double)(i * i) + 2.0)) < 10;
+ assert (int)\add_double(\mul_double(i, i), (double)2.0) < 10;
[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index f791b980831bd6f9e0c61b1febfb6e83cba17dda..b5f30cd1f748e45b9ab0972fcc731c6dfbc1ae9f 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -171,10 +171,10 @@
[eva] Done for function Frama_C_float_interval
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert 0 ≤ (int)((double)((double)((float)(i * i)) + 2.0));
+ assert 0 ≤ (int)\add_double((double)\mul_float(i, i), (double)2.0);
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert (int)((double)((double)((float)(i * i)) + 2.0)) < 10;
+ assert (int)\add_double((double)\mul_float(i, i), (double)2.0) < 10;
[eva] computing for function access_bits <- other <- main.
Called from tests/float/nonlin.c:69.
[eva] Recording results for access_bits
@@ -195,8 +195,9 @@
[eva:alarm] tests/float/nonlin.c:77: Warning:
non-finite double value.
assert
- \is_finite((double)((double)1 /
- (double)((double)((double)ff * (double)ff) + 0.000000001)));
+ \is_finite(\div_double((double)1,
+ \add_double(\mul_double((double)ff, (double)ff),
+ (double)0.000000001)));
[eva] Recording results for split_alarm
[eva] Done for function split_alarm
[eva] computing for function norm <- main.
@@ -220,12 +221,12 @@
function Frama_C_float_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_float_interval
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v1 * v1));
+ non-finite float value. assert \is_finite(\mul_float(v1, v1));
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v2 * v2));
+ non-finite float value. assert \is_finite(\mul_float(v2, v2));
[eva:alarm] tests/float/nonlin.c:92: Warning:
non-finite float value.
- assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
+ assert \is_finite(\add_float(\mul_float(v1, v1), \mul_float(v2, v2)));
[eva] Recording results for norm
[eva] Done for function norm
[eva] computing for function garbled <- main.
@@ -243,7 +244,7 @@
[eva:alarm] tests/float/nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] tests/float/nonlin.c:99: Warning:
- non-finite float value. assert \is_finite((float)(a_0 + a_0));
+ non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva] tests/float/nonlin.c:99:
Assigning imprecise value to f.
The imprecision originates from Arithmetic
@@ -260,7 +261,8 @@
[eva] Done for function Frama_C_float_interval
[eva:alarm] tests/float/nonlin.c:113: Warning:
non-finite float value.
- assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
+ assert
+ \is_finite(\div_float(f1, \sub_float(\sub_float(\add_float(f, f), f), f1)));
[eva] Recording results for around_zeros
[eva] Done for function around_zeros
[eva] computing for function subdivide_strategy <- main.
@@ -276,7 +278,7 @@
non-finite float value. assert \is_finite(nondet);
[eva:alarm] tests/float/nonlin.c:135: Warning:
non-finite float value.
- assert \is_finite((float)((float)(x_0 - d_0) * (float)(x_0 - d_0)));
+ assert \is_finite(\mul_float(\sub_float(x_0, d_0), \sub_float(x_0, d_0)));
[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
Called from tests/float/nonlin.c:136.
[eva] tests/float/nonlin.c:136:
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index ba58150afafceddb7303e4ef4f35b0d438a7b2b4..52f4a2d9697a022028a265fc38b4728b6b54fe02 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -177,7 +177,7 @@
[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert (int)((double)((double)((float)(i * i)) + 2.0)) < 10;
+ assert (int)\add_double((double)\mul_float(i, i), (double)2.0) < 10;
[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
@@ -243,12 +243,12 @@
[eva:nonlin] tests/float/nonlin.c:92: subdividing on v1
[eva:nonlin] tests/float/nonlin.c:92: subdividing on v2
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v1 * v1));
+ non-finite float value. assert \is_finite(\mul_float(v1, v1));
[eva:alarm] tests/float/nonlin.c:92: Warning:
- non-finite float value. assert \is_finite((float)(v2 * v2));
+ non-finite float value. assert \is_finite(\mul_float(v2, v2));
[eva:alarm] tests/float/nonlin.c:92: Warning:
non-finite float value.
- assert \is_finite((float)((float)(v1 * v1) + (float)(v2 * v2)));
+ assert \is_finite(\add_float(\mul_float(v1, v1), \mul_float(v2, v2)));
[eva] Recording results for norm
[eva] Done for function norm
[eva] computing for function garbled <- main.
@@ -266,7 +266,7 @@
[eva:alarm] tests/float/nonlin.c:99: Warning:
non-finite float value. assert \is_finite(a_0);
[eva:alarm] tests/float/nonlin.c:99: Warning:
- non-finite float value. assert \is_finite((float)(a_0 + a_0));
+ non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva] tests/float/nonlin.c:99:
Assigning imprecise value to f.
The imprecision originates from Arithmetic
@@ -287,7 +287,8 @@
[eva:nonlin] tests/float/nonlin.c:113: subdividing on f
[eva:alarm] tests/float/nonlin.c:113: Warning:
non-finite float value.
- assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
+ assert
+ \is_finite(\div_float(f1, \sub_float(\sub_float(\add_float(f, f), f), f1)));
[eva] Recording results for around_zeros
[eva] Done for function around_zeros
[eva] computing for function subdivide_strategy <- main.
@@ -308,7 +309,7 @@
[eva:nonlin] tests/float/nonlin.c:135: subdividing on x_0
[eva:alarm] tests/float/nonlin.c:135: Warning:
non-finite float value.
- assert \is_finite((float)((float)(x_0 - d_0) * (float)(x_0 - d_0)));
+ assert \is_finite(\mul_float(\sub_float(x_0, d_0), \sub_float(x_0, d_0)));
[eva] computing for function Frama_C_float_interval <- subdivide_strategy <- main.
Called from tests/float/nonlin.c:136.
[eva] tests/float/nonlin.c:136:
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 36e1a671ef649728d5f1a3b4b1ba0f00f12488ea..04154d9e75bb6b6f7948187198acac640d1bc51e 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -177,7 +177,7 @@
[eva:nonlin] tests/float/nonlin.c:63: subdividing on i
[eva:alarm] tests/float/nonlin.c:63: Warning:
accessing out of bounds index.
- assert (int)((double)((double)((float)(i * i)) + 2.0)) < 10;
+ assert (int)\add_double((double)\mul_float(i, i), (double)2.0) < 10;
[eva:nonlin] tests/float/nonlin.c:64: non-linear 's - s', lv 's'
[eva:nonlin] tests/float/nonlin.c:64: subdividing on s
[eva:nonlin] tests/float/nonlin.c:65: non-linear 's - s', lv 's'
diff --git a/tests/float/oracle/parse.res.oracle b/tests/float/oracle/parse.res.oracle
index 99068d34513acf3f0265fbf6ecada78cb40eacbb..3d54be548a3179ceb69f05ad3f2b3d3711af3f2b 100644
--- a/tests/float/oracle/parse.res.oracle
+++ b/tests/float/oracle/parse.res.oracle
@@ -14,11 +14,12 @@
[eva] tests/float/parse.i:26:
Frama_C_show_each: {0x1.83a99c3ec7eb0p893}, {{ "reached" }}
[eva:alarm] tests/float/parse.i:30: Warning:
- non-finite double value. assert \is_finite(0.0000001E9999999999999999999);
+ non-finite double value.
+ assert \is_finite((double)0.0000001E9999999999999999999);
[eva] tests/float/parse.i:36: Warning:
cannot parse floating-point constant, returning imprecise result
[eva:alarm] tests/float/parse.i:36: Warning:
- non-finite long double value. assert \is_finite(0x1p32767L);
+ non-finite long double value. assert \is_finite((long double)0x1p32767L);
[eva:alarm] tests/float/parse.i:37: Warning:
non-finite long double value. assert \is_finite(l);
[eva:alarm] tests/float/parse.i:37: Warning:
diff --git a/tests/float/oracle/widen.0.res.oracle b/tests/float/oracle/widen.0.res.oracle
index 218c0d29cca4f218650f5d82f241cdaf3e39f402..4c881d40cfff401e4548d83ed32e6598436c1849 100644
--- a/tests/float/oracle/widen.0.res.oracle
+++ b/tests/float/oracle/widen.0.res.oracle
@@ -8,7 +8,7 @@
Called from tests/float/widen.c:50.
[eva] tests/float/widen.c:13: starting to merge loop iterations
[eva:alarm] tests/float/widen.c:14: Warning:
- non-finite double value. assert \is_finite((double)(max * 2.));
+ non-finite double value. assert \is_finite(\mul_double(max, (double)2.));
[eva] tests/float/widen.c:16: starting to merge loop iterations
[eva] tests/float/widen.c:24:
Frama_C_show_each_double_inf: [1. .. 1.79769313486e+308]
diff --git a/tests/misc/oracle/widen_hints_float.res.oracle b/tests/misc/oracle/widen_hints_float.res.oracle
index 45e531fdbc470f765c870b2955bad55c59c4f6e8..9fad6f26134fdf5db05974bf00879b0771336e0e 100644
--- a/tests/misc/oracle/widen_hints_float.res.oracle
+++ b/tests/misc/oracle/widen_hints_float.res.oracle
@@ -37,7 +37,8 @@
[eva:alarm] tests/misc/widen_hints_float.c:34: Warning:
non-finite double value.
assert
- \is_finite((double)((double)(f3 - (double)64) * (double)(f3 - (double)64)));
+ \is_finite(\mul_double(\sub_double(f3, (double)64),
+ \sub_double(f3, (double)64)));
[eva] Recording results for parabola
[eva] Done for function parabola
[eva] computing for function trigo <- main.
diff --git a/tests/rte/oracle/addsub_typedef.res.oracle b/tests/rte/oracle/addsub_typedef.res.oracle
index adf710ee1acf5ddc82ee2dc8b5d8929dd5784866..8e0232c30bab6c46aa1f8853d6f891a4bda2baa9 100644
--- a/tests/rte/oracle/addsub_typedef.res.oracle
+++ b/tests/rte/oracle/addsub_typedef.res.oracle
@@ -41,7 +41,8 @@ int main(void)
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-0x7ffffffc) - y; */
z = -0x7ffffffc - y;
/*@ assert rte: signed_overflow: -2147483647 ≤ x; */
- /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-x) - 0x7ffffffc; */
+ /*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-x) - 0x7ffffffc;
+ */
z = - x - 0x7ffffffc;
/*@ assert rte: signed_overflow: 0x7ffffffc + y ≤ 2147483647; */
z = 0x7ffffffc + y;
diff --git a/tests/rte/oracle/addsub_unsigned.1.res.oracle b/tests/rte/oracle/addsub_unsigned.1.res.oracle
index b30ebf8b1ab7fc6c883c202859c8e06dd13657cf..1a6a8a945930b511bcb9ea1b7b90de32c9d0fb77 100644
--- a/tests/rte/oracle/addsub_unsigned.1.res.oracle
+++ b/tests/rte/oracle/addsub_unsigned.1.res.oracle
@@ -19,7 +19,7 @@ int main(void)
uy = 0x80000000U + 0x80000000U;
/*@ assert rte: unsigned_overflow: 2U * 0x80000000U ≤ 4294967295; */
uy = 2U * 0x80000000U;
- /*@ assert rte: unsigned_overflow: ux + (unsigned int)2 ≤ 4294967295; */
+ /*@ assert rte: unsigned_overflow: ux + 2 ≤ 4294967295; */
uz = ux + (unsigned int)2;
__retres = 0;
return __retres;
diff --git a/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle b/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle
index 98f2482e3cc09f06427c2684a918ac6760cede61..3c0fc49fce384954abdbf613aafe4722b1df764b 100644
--- a/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle
+++ b/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle
@@ -20,7 +20,7 @@ int main(void)
uy = 0x80000000U + 0x80000000U;
/*@ assert rte: unsigned_overflow: 2U * 0x80000000U ≤ 4294967295; */
uy = 2U * 0x80000000U;
- /*@ assert rte: unsigned_overflow: ux + (unsigned int)2 ≤ 4294967295; */
+ /*@ assert rte: unsigned_overflow: ux + 2 ≤ 4294967295; */
uz = ux + (uint)2;
__retres = 0;
return __retres;
diff --git a/tests/rte/oracle/divmod_typedef.res.oracle b/tests/rte/oracle/divmod_typedef.res.oracle
index 51b06e5796e1d2d9b536684513fdde9e05346750..a965ff5054db7b38756b6c5523d7268fbb119e62 100644
--- a/tests/rte/oracle/divmod_typedef.res.oracle
+++ b/tests/rte/oracle/divmod_typedef.res.oracle
@@ -65,7 +65,7 @@ int main(void)
uz = (unsigned int)((int)(0x80000000 / 0xffffffff));
/*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
/*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
- /*@ assert rte: division_by_zero: (int)(x + y) ≢ 0; */
+ /*@ assert rte: division_by_zero: (tint)(x + y) ≢ 0; */
z = 1 / (x + y);
/*@ assert rte: signed_overflow: x / (int)(-1) ≤ 2147483647; */
z = x / -1;
diff --git a/tests/rte/oracle/finite_float.res.oracle b/tests/rte/oracle/finite_float.res.oracle
index 3e0ca8cba95bf4e72e96ea68cadaac3b6d34d378..5adab0a6237db04160e6a06b2ea1e1b7184e6c74 100644
--- a/tests/rte/oracle/finite_float.res.oracle
+++ b/tests/rte/oracle/finite_float.res.oracle
@@ -5,12 +5,12 @@
#include "math.h"
void main(void)
{
- /*@ assert rte: is_nan_or_infinite: \is_finite(0x1p10000); */
+ /*@ assert rte: is_nan_or_infinite: \is_finite((double)0x1p10000); */
double d = 0x1p10000;
d = 0.;
- /*@ assert rte: is_nan_or_infinite: \is_finite((double)(d / d)); */
+ /*@ assert rte: is_nan_or_infinite: \is_finite(\div_double(d, d)); */
/*@ assert
- rte: is_nan_or_infinite: \is_finite((double)((double)(d / d) + d));
+ rte: is_nan_or_infinite: \is_finite(\add_double(\div_double(d, d), d));
*/
double e = d / d + d;
return;
diff --git a/tests/rte_manual/oracle/unsigned.1.res.oracle b/tests/rte_manual/oracle/unsigned.1.res.oracle
index ed1ad94cf29fa2456a9d34125464d34e62674c21..37e1f70016c7bb12f5c0104bc73d1d76ee3ec89a 100644
--- a/tests/rte_manual/oracle/unsigned.1.res.oracle
+++ b/tests/rte_manual/oracle/unsigned.1.res.oracle
@@ -8,8 +8,8 @@ unsigned int f(unsigned int a, unsigned int b)
unsigned int z;
/*@ assert rte: unsigned_overflow: a << 3 ≤ 4294967295; */
x = a << 3;
- /*@ assert rte: unsigned_overflow: 0 ≤ b * (unsigned int)2; */
- /*@ assert rte: unsigned_overflow: b * (unsigned int)2 ≤ 4294967295; */
+ /*@ assert rte: unsigned_overflow: 0 ≤ b * 2; */
+ /*@ assert rte: unsigned_overflow: b * 2 ≤ 4294967295; */
y = b * (unsigned int)2;
/*@ assert rte: unsigned_overflow: 0 ≤ x - y; */
/*@ assert rte: unsigned_overflow: x - y ≤ 4294967295; */
diff --git a/tests/slicing/oracle/keep_annot.2.res.oracle b/tests/slicing/oracle/keep_annot.2.res.oracle
index 0cbe4ace479b127e913f7bae2e141a61ec2855a9..f8ab7b83c160852293a27331eccd5df9c7b1b488 100644
--- a/tests/slicing/oracle/keep_annot.2.res.oracle
+++ b/tests/slicing/oracle/keep_annot.2.res.oracle
@@ -14,8 +14,9 @@
[eva:alarm] tests/slicing/keep_annot.i:41: Warning:
non-finite float value.
assert
- \is_finite((float)((double)((double)u -
- (double)((double)*(dabs + (int)(ii + 1)) * 2.0))));
+ \is_finite((float)\sub_double((double)u,
+ \mul_double((double)*(dabs + (int)(ii + 1)),
+ (double)2.0)));
[eva:alarm] tests/slicing/keep_annot.i:42: Warning:
assertion got status unknown.
[eva] Recording results for L
diff --git a/tests/slicing/oracle/keep_annot.3.res.oracle b/tests/slicing/oracle/keep_annot.3.res.oracle
index 52b2ca08307d14ae8fb79ba46492e0f554d748e8..77fc3eb76de0f7f2760cc54384439a1626e6f421 100644
--- a/tests/slicing/oracle/keep_annot.3.res.oracle
+++ b/tests/slicing/oracle/keep_annot.3.res.oracle
@@ -14,8 +14,9 @@
[eva:alarm] tests/slicing/keep_annot.i:41: Warning:
non-finite float value.
assert
- \is_finite((float)((double)((double)u -
- (double)((double)*(dabs + (int)(ii + 1)) * 2.0))));
+ \is_finite((float)\sub_double((double)u,
+ \mul_double((double)*(dabs + (int)(ii + 1)),
+ (double)2.0)));
[eva:alarm] tests/slicing/keep_annot.i:42: Warning:
assertion got status unknown.
[eva] Recording results for L
diff --git a/tests/slicing/oracle/unravel-variance.0.res.oracle b/tests/slicing/oracle/unravel-variance.0.res.oracle
index b91a1fe5bed87339e51dd7fffbe8c5305aeb23dc..0538b7db677b80251e23c6750e0bacd1b39c0227 100644
--- a/tests/slicing/oracle/unravel-variance.0.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.0.res.oracle
@@ -21,20 +21,20 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
- non-finite float value. assert \is_finite((float)(x[i] * x[i]));
+ non-finite float value. assert \is_finite(\mul_float(x[i], x[i]));
[eva] tests/slicing/unravel-variance.i:32: starting to merge loop iterations
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
- non-finite float value. assert \is_finite((float)(t1 + x[i]));
+ non-finite float value. assert \is_finite(\add_float(t1, x[i]));
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value.
- assert \is_finite((float)(ssq + (float)(x[i] * x[i])));
+ assert \is_finite(\add_float(ssq, \mul_float(x[i], x[i])));
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
@@ -47,69 +47,75 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
accessing out of bounds index. assert i < 1024;
[eva:alarm] tests/slicing/unravel-variance.i:38: Warning:
- non-finite float value. assert \is_finite((float)(t1 / (float)n));
+ non-finite float value. assert \is_finite(\div_float(t1, (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
- non-finite float value. assert \is_finite((float)((float)n * avg));
+ non-finite float value. assert \is_finite(\mul_float((float)n, avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
signed overflow. assert -2147483648 ≤ n - 1;
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)((float)((float)n * avg) * avg));
+ assert \is_finite(\mul_float(\mul_float((float)n, avg), avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)(ssq - (float)((float)((float)n * avg) * avg)));
+ assert
+ \is_finite(\sub_float(ssq, \mul_float(\mul_float((float)n, avg), avg)));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)((float)((float)n * avg) * avg)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq,
+ \mul_float(\mul_float((float)n, avg), avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(t1 * avg));
+ non-finite float value. assert \is_finite(\mul_float(t1, avg));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(ssq - (float)(t1 * avg)));
+ non-finite float value.
+ assert \is_finite(\sub_float(ssq, \mul_float(t1, avg)));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)(t1 * avg)) / (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq, \mul_float(t1, avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
- non-finite float value. assert \is_finite((float)(t1 * t1));
+ non-finite float value. assert \is_finite(\mul_float(t1, t1));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t1 * t1) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t1, t1), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
- non-finite float value. assert \is_finite((float)(ssq - t1));
+ non-finite float value. assert \is_finite(\sub_float(ssq, t1));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
non-finite float value.
- assert \is_finite((float)((float)(ssq - t1) / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(\sub_float(ssq, t1), (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
- non-finite float value. assert \is_finite((float)(x[i] - avg));
+ non-finite float value. assert \is_finite(\sub_float(x[i], avg));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(dev * dev));
+ non-finite float value. assert \is_finite(\mul_float(dev, dev));
[eva] tests/slicing/unravel-variance.i:44: starting to merge loop iterations
[eva:alarm] tests/slicing/unravel-variance.i:47: Warning:
- non-finite float value. assert \is_finite((float)(t2 + dev));
+ non-finite float value. assert \is_finite(\add_float(t2, dev));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(t1 + (float)(dev * dev)));
+ non-finite float value.
+ assert \is_finite(\add_float(t1, \mul_float(dev, dev)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
- non-finite float value. assert \is_finite((float)(t2 * t2));
+ non-finite float value. assert \is_finite(\mul_float(t2, t2));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t2 * t2) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t2, t2), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)(t1 - (float)((float)(t2 * t2) / (float)n)));
+ assert \is_finite(\sub_float(t1, \div_float(\mul_float(t2, t2), (float)n)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(t1 - (float)((float)(t2 * t2) / (float)n)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(t1,
+ \div_float(\mul_float(t2, t2), (float)n)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:51: Warning:
non-finite float value.
- assert \is_finite((float)(t1 / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(t1, (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert -2147483649 < var2;
diff --git a/tests/slicing/oracle/unravel-variance.1.res.oracle b/tests/slicing/oracle/unravel-variance.1.res.oracle
index 1b7ede21df7a647fe79953593bdfa679ba0d0830..fa17384ccb6a919e4e5571fffb3c5e297a251580 100644
--- a/tests/slicing/oracle/unravel-variance.1.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.1.res.oracle
@@ -21,20 +21,20 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
- non-finite float value. assert \is_finite((float)(x[i] * x[i]));
+ non-finite float value. assert \is_finite(\mul_float(x[i], x[i]));
[eva] tests/slicing/unravel-variance.i:32: starting to merge loop iterations
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
- non-finite float value. assert \is_finite((float)(t1 + x[i]));
+ non-finite float value. assert \is_finite(\add_float(t1, x[i]));
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value.
- assert \is_finite((float)(ssq + (float)(x[i] * x[i])));
+ assert \is_finite(\add_float(ssq, \mul_float(x[i], x[i])));
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
@@ -47,69 +47,75 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
accessing out of bounds index. assert i < 1024;
[eva:alarm] tests/slicing/unravel-variance.i:38: Warning:
- non-finite float value. assert \is_finite((float)(t1 / (float)n));
+ non-finite float value. assert \is_finite(\div_float(t1, (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
- non-finite float value. assert \is_finite((float)((float)n * avg));
+ non-finite float value. assert \is_finite(\mul_float((float)n, avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
signed overflow. assert -2147483648 ≤ n - 1;
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)((float)((float)n * avg) * avg));
+ assert \is_finite(\mul_float(\mul_float((float)n, avg), avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)(ssq - (float)((float)((float)n * avg) * avg)));
+ assert
+ \is_finite(\sub_float(ssq, \mul_float(\mul_float((float)n, avg), avg)));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)((float)((float)n * avg) * avg)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq,
+ \mul_float(\mul_float((float)n, avg), avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(t1 * avg));
+ non-finite float value. assert \is_finite(\mul_float(t1, avg));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(ssq - (float)(t1 * avg)));
+ non-finite float value.
+ assert \is_finite(\sub_float(ssq, \mul_float(t1, avg)));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)(t1 * avg)) / (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq, \mul_float(t1, avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
- non-finite float value. assert \is_finite((float)(t1 * t1));
+ non-finite float value. assert \is_finite(\mul_float(t1, t1));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t1 * t1) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t1, t1), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
- non-finite float value. assert \is_finite((float)(ssq - t1));
+ non-finite float value. assert \is_finite(\sub_float(ssq, t1));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
non-finite float value.
- assert \is_finite((float)((float)(ssq - t1) / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(\sub_float(ssq, t1), (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
- non-finite float value. assert \is_finite((float)(x[i] - avg));
+ non-finite float value. assert \is_finite(\sub_float(x[i], avg));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(dev * dev));
+ non-finite float value. assert \is_finite(\mul_float(dev, dev));
[eva] tests/slicing/unravel-variance.i:44: starting to merge loop iterations
[eva:alarm] tests/slicing/unravel-variance.i:47: Warning:
- non-finite float value. assert \is_finite((float)(t2 + dev));
+ non-finite float value. assert \is_finite(\add_float(t2, dev));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(t1 + (float)(dev * dev)));
+ non-finite float value.
+ assert \is_finite(\add_float(t1, \mul_float(dev, dev)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
- non-finite float value. assert \is_finite((float)(t2 * t2));
+ non-finite float value. assert \is_finite(\mul_float(t2, t2));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t2 * t2) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t2, t2), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)(t1 - (float)((float)(t2 * t2) / (float)n)));
+ assert \is_finite(\sub_float(t1, \div_float(\mul_float(t2, t2), (float)n)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(t1 - (float)((float)(t2 * t2) / (float)n)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(t1,
+ \div_float(\mul_float(t2, t2), (float)n)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:51: Warning:
non-finite float value.
- assert \is_finite((float)(t1 / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(t1, (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert -2147483649 < var2;
diff --git a/tests/slicing/oracle/unravel-variance.2.res.oracle b/tests/slicing/oracle/unravel-variance.2.res.oracle
index 344a7d901f6b110bd383305f098efdad9eb9d5c0..48bf86249b3ce934353728416cb2f02dc2613341 100644
--- a/tests/slicing/oracle/unravel-variance.2.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.2.res.oracle
@@ -21,20 +21,20 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
- non-finite float value. assert \is_finite((float)(x[i] * x[i]));
+ non-finite float value. assert \is_finite(\mul_float(x[i], x[i]));
[eva] tests/slicing/unravel-variance.i:32: starting to merge loop iterations
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
- non-finite float value. assert \is_finite((float)(t1 + x[i]));
+ non-finite float value. assert \is_finite(\add_float(t1, x[i]));
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value.
- assert \is_finite((float)(ssq + (float)(x[i] * x[i])));
+ assert \is_finite(\add_float(ssq, \mul_float(x[i], x[i])));
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
@@ -47,69 +47,75 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
accessing out of bounds index. assert i < 1024;
[eva:alarm] tests/slicing/unravel-variance.i:38: Warning:
- non-finite float value. assert \is_finite((float)(t1 / (float)n));
+ non-finite float value. assert \is_finite(\div_float(t1, (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
- non-finite float value. assert \is_finite((float)((float)n * avg));
+ non-finite float value. assert \is_finite(\mul_float((float)n, avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
signed overflow. assert -2147483648 ≤ n - 1;
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)((float)((float)n * avg) * avg));
+ assert \is_finite(\mul_float(\mul_float((float)n, avg), avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)(ssq - (float)((float)((float)n * avg) * avg)));
+ assert
+ \is_finite(\sub_float(ssq, \mul_float(\mul_float((float)n, avg), avg)));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)((float)((float)n * avg) * avg)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq,
+ \mul_float(\mul_float((float)n, avg), avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(t1 * avg));
+ non-finite float value. assert \is_finite(\mul_float(t1, avg));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(ssq - (float)(t1 * avg)));
+ non-finite float value.
+ assert \is_finite(\sub_float(ssq, \mul_float(t1, avg)));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)(t1 * avg)) / (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq, \mul_float(t1, avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
- non-finite float value. assert \is_finite((float)(t1 * t1));
+ non-finite float value. assert \is_finite(\mul_float(t1, t1));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t1 * t1) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t1, t1), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
- non-finite float value. assert \is_finite((float)(ssq - t1));
+ non-finite float value. assert \is_finite(\sub_float(ssq, t1));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
non-finite float value.
- assert \is_finite((float)((float)(ssq - t1) / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(\sub_float(ssq, t1), (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
- non-finite float value. assert \is_finite((float)(x[i] - avg));
+ non-finite float value. assert \is_finite(\sub_float(x[i], avg));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(dev * dev));
+ non-finite float value. assert \is_finite(\mul_float(dev, dev));
[eva] tests/slicing/unravel-variance.i:44: starting to merge loop iterations
[eva:alarm] tests/slicing/unravel-variance.i:47: Warning:
- non-finite float value. assert \is_finite((float)(t2 + dev));
+ non-finite float value. assert \is_finite(\add_float(t2, dev));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(t1 + (float)(dev * dev)));
+ non-finite float value.
+ assert \is_finite(\add_float(t1, \mul_float(dev, dev)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
- non-finite float value. assert \is_finite((float)(t2 * t2));
+ non-finite float value. assert \is_finite(\mul_float(t2, t2));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t2 * t2) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t2, t2), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)(t1 - (float)((float)(t2 * t2) / (float)n)));
+ assert \is_finite(\sub_float(t1, \div_float(\mul_float(t2, t2), (float)n)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(t1 - (float)((float)(t2 * t2) / (float)n)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(t1,
+ \div_float(\mul_float(t2, t2), (float)n)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:51: Warning:
non-finite float value.
- assert \is_finite((float)(t1 / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(t1, (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert -2147483649 < var2;
diff --git a/tests/slicing/oracle/unravel-variance.3.res.oracle b/tests/slicing/oracle/unravel-variance.3.res.oracle
index 75bbcf89bca26210963c035183b657e335b465d0..6f444dfaef6f22c6e07971d1e6293c933dcbf944 100644
--- a/tests/slicing/oracle/unravel-variance.3.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.3.res.oracle
@@ -21,20 +21,20 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
- non-finite float value. assert \is_finite((float)(x[i] * x[i]));
+ non-finite float value. assert \is_finite(\mul_float(x[i], x[i]));
[eva] tests/slicing/unravel-variance.i:32: starting to merge loop iterations
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
- non-finite float value. assert \is_finite((float)(t1 + x[i]));
+ non-finite float value. assert \is_finite(\add_float(t1, x[i]));
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value.
- assert \is_finite((float)(ssq + (float)(x[i] * x[i])));
+ assert \is_finite(\add_float(ssq, \mul_float(x[i], x[i])));
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
@@ -47,69 +47,75 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
accessing out of bounds index. assert i < 1024;
[eva:alarm] tests/slicing/unravel-variance.i:38: Warning:
- non-finite float value. assert \is_finite((float)(t1 / (float)n));
+ non-finite float value. assert \is_finite(\div_float(t1, (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
- non-finite float value. assert \is_finite((float)((float)n * avg));
+ non-finite float value. assert \is_finite(\mul_float((float)n, avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
signed overflow. assert -2147483648 ≤ n - 1;
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)((float)((float)n * avg) * avg));
+ assert \is_finite(\mul_float(\mul_float((float)n, avg), avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)(ssq - (float)((float)((float)n * avg) * avg)));
+ assert
+ \is_finite(\sub_float(ssq, \mul_float(\mul_float((float)n, avg), avg)));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)((float)((float)n * avg) * avg)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq,
+ \mul_float(\mul_float((float)n, avg), avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(t1 * avg));
+ non-finite float value. assert \is_finite(\mul_float(t1, avg));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(ssq - (float)(t1 * avg)));
+ non-finite float value.
+ assert \is_finite(\sub_float(ssq, \mul_float(t1, avg)));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)(t1 * avg)) / (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq, \mul_float(t1, avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
- non-finite float value. assert \is_finite((float)(t1 * t1));
+ non-finite float value. assert \is_finite(\mul_float(t1, t1));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t1 * t1) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t1, t1), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
- non-finite float value. assert \is_finite((float)(ssq - t1));
+ non-finite float value. assert \is_finite(\sub_float(ssq, t1));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
non-finite float value.
- assert \is_finite((float)((float)(ssq - t1) / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(\sub_float(ssq, t1), (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
- non-finite float value. assert \is_finite((float)(x[i] - avg));
+ non-finite float value. assert \is_finite(\sub_float(x[i], avg));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(dev * dev));
+ non-finite float value. assert \is_finite(\mul_float(dev, dev));
[eva] tests/slicing/unravel-variance.i:44: starting to merge loop iterations
[eva:alarm] tests/slicing/unravel-variance.i:47: Warning:
- non-finite float value. assert \is_finite((float)(t2 + dev));
+ non-finite float value. assert \is_finite(\add_float(t2, dev));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(t1 + (float)(dev * dev)));
+ non-finite float value.
+ assert \is_finite(\add_float(t1, \mul_float(dev, dev)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
- non-finite float value. assert \is_finite((float)(t2 * t2));
+ non-finite float value. assert \is_finite(\mul_float(t2, t2));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t2 * t2) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t2, t2), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)(t1 - (float)((float)(t2 * t2) / (float)n)));
+ assert \is_finite(\sub_float(t1, \div_float(\mul_float(t2, t2), (float)n)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(t1 - (float)((float)(t2 * t2) / (float)n)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(t1,
+ \div_float(\mul_float(t2, t2), (float)n)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:51: Warning:
non-finite float value.
- assert \is_finite((float)(t1 / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(t1, (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert -2147483649 < var2;
diff --git a/tests/slicing/oracle/unravel-variance.4.res.oracle b/tests/slicing/oracle/unravel-variance.4.res.oracle
index f651a4d6a3b199273e49d1c59403270dbb63e24a..ac6ef9b1483d3fe1ee4b72ce634390b98f67253f 100644
--- a/tests/slicing/oracle/unravel-variance.4.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.4.res.oracle
@@ -21,20 +21,20 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
- non-finite float value. assert \is_finite((float)(x[i] * x[i]));
+ non-finite float value. assert \is_finite(\mul_float(x[i], x[i]));
[eva] tests/slicing/unravel-variance.i:32: starting to merge loop iterations
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
- non-finite float value. assert \is_finite((float)(t1 + x[i]));
+ non-finite float value. assert \is_finite(\add_float(t1, x[i]));
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:36: Warning:
non-finite float value.
- assert \is_finite((float)(ssq + (float)(x[i] * x[i])));
+ assert \is_finite(\add_float(ssq, \mul_float(x[i], x[i])));
[eva] computing for function scanf <- main.
Called from tests/slicing/unravel-variance.i:34.
[eva] Done for function scanf
@@ -47,69 +47,75 @@
[eva:alarm] tests/slicing/unravel-variance.i:35: Warning:
accessing out of bounds index. assert i < 1024;
[eva:alarm] tests/slicing/unravel-variance.i:38: Warning:
- non-finite float value. assert \is_finite((float)(t1 / (float)n));
+ non-finite float value. assert \is_finite(\div_float(t1, (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
- non-finite float value. assert \is_finite((float)((float)n * avg));
+ non-finite float value. assert \is_finite(\mul_float((float)n, avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
signed overflow. assert -2147483648 ≤ n - 1;
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)((float)((float)n * avg) * avg));
+ assert \is_finite(\mul_float(\mul_float((float)n, avg), avg));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
- assert \is_finite((float)(ssq - (float)((float)((float)n * avg) * avg)));
+ assert
+ \is_finite(\sub_float(ssq, \mul_float(\mul_float((float)n, avg), avg)));
[eva:alarm] tests/slicing/unravel-variance.i:39: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)((float)((float)n * avg) * avg)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq,
+ \mul_float(\mul_float((float)n, avg), avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(t1 * avg));
+ non-finite float value. assert \is_finite(\mul_float(t1, avg));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
- non-finite float value. assert \is_finite((float)(ssq - (float)(t1 * avg)));
+ non-finite float value.
+ assert \is_finite(\sub_float(ssq, \mul_float(t1, avg)));
[eva:alarm] tests/slicing/unravel-variance.i:40: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(ssq - (float)(t1 * avg)) / (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(ssq, \mul_float(t1, avg)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
- non-finite float value. assert \is_finite((float)(t1 * t1));
+ non-finite float value. assert \is_finite(\mul_float(t1, t1));
[eva:alarm] tests/slicing/unravel-variance.i:41: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t1 * t1) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t1, t1), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
- non-finite float value. assert \is_finite((float)(ssq - t1));
+ non-finite float value. assert \is_finite(\sub_float(ssq, t1));
[eva:alarm] tests/slicing/unravel-variance.i:42: Warning:
non-finite float value.
- assert \is_finite((float)((float)(ssq - t1) / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(\sub_float(ssq, t1), (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
accessing uninitialized left-value. assert \initialized(&x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
non-finite float value. assert \is_finite(x[i]);
[eva:alarm] tests/slicing/unravel-variance.i:46: Warning:
- non-finite float value. assert \is_finite((float)(x[i] - avg));
+ non-finite float value. assert \is_finite(\sub_float(x[i], avg));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(dev * dev));
+ non-finite float value. assert \is_finite(\mul_float(dev, dev));
[eva] tests/slicing/unravel-variance.i:44: starting to merge loop iterations
[eva:alarm] tests/slicing/unravel-variance.i:47: Warning:
- non-finite float value. assert \is_finite((float)(t2 + dev));
+ non-finite float value. assert \is_finite(\add_float(t2, dev));
[eva:alarm] tests/slicing/unravel-variance.i:48: Warning:
- non-finite float value. assert \is_finite((float)(t1 + (float)(dev * dev)));
+ non-finite float value.
+ assert \is_finite(\add_float(t1, \mul_float(dev, dev)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
- non-finite float value. assert \is_finite((float)(t2 * t2));
+ non-finite float value. assert \is_finite(\mul_float(t2, t2));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)((float)(t2 * t2) / (float)n));
+ assert \is_finite(\div_float(\mul_float(t2, t2), (float)n));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
- assert \is_finite((float)(t1 - (float)((float)(t2 * t2) / (float)n)));
+ assert \is_finite(\sub_float(t1, \div_float(\mul_float(t2, t2), (float)n)));
[eva:alarm] tests/slicing/unravel-variance.i:50: Warning:
non-finite float value.
assert
- \is_finite((float)((float)(t1 - (float)((float)(t2 * t2) / (float)n)) /
- (float)((int)(n - 1))));
+ \is_finite(\div_float(\sub_float(t1,
+ \div_float(\mul_float(t2, t2), (float)n)),
+ (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:51: Warning:
non-finite float value.
- assert \is_finite((float)(t1 / (float)((int)(n - 1))));
+ assert \is_finite(\div_float(t1, (float)((int)(n - 1))));
[eva:alarm] tests/slicing/unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert -2147483649 < var2;
diff --git a/tests/spec/expr_to_term.i b/tests/spec/expr_to_term.i
index 5320e071398288731edd84d484de97ffc5cf4677..e0e887144169aea4640bb1f008beabd15bfba32b 100644
--- a/tests/spec/expr_to_term.i
+++ b/tests/spec/expr_to_term.i
@@ -2,14 +2,19 @@
MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: -print
*/
+
+
+// This predicate is modified by expr_to_term.ml plugin to compare
+// the assigned l-value or condition at provided stmt id with the logical term
+
+/*@ predicate int_eq(int logical, int from_stmt_id) = logical == from_stmt_id; */
+
int x[10];
struct S { int y; int z; } s;
int t;
-/*@ predicate int_eq(int logical, int from_c) = logical == from_c; */
-
/*@ ensures int_eq(*(int*)((unsigned)0x1 + 0x2),(int)0); */
int f() {
@@ -29,7 +34,12 @@ int main() {
t = 4;
}
-/*@ ensures int_eq((int)!t,(int)5); */
+/*@ ensures int_eq((int)(t!=0 ? 0 : 1),(int)5); */
int g() {
if (!t) return 2; else return 3;
}
+
+/*@ ensures int_eq((int)(t<5 ? 1 : 0),(int)6); */
+int h() {
+ if (t<5) return 2; else return 3;
+}
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index 17478ac46f188ed3bd618d92ccdab4ea2d51c863..b6ce6b3ab15e0fab3b0e5eb4f46909816c7b4d8d 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -2,7 +2,7 @@ open Cil_types
let emitter = Emitter.(create "Test" [Funspec] ~correctness:[] ~tuning:[])
-let check_expr_term check fct s e =
+let check_expr_term check fct s post =
let exp =
match s.skind with
| Instr (Set (lv,_,loc)) -> Cil.new_exp ~loc (Lval lv)
@@ -10,12 +10,11 @@ let check_expr_term check fct s e =
| _ -> Kernel.fatal "Unexpected statement %a" Printer.pp_stmt s
in
let term =
- match e with
+ match post with
| (_, { ip_content = { pred_content = Papp(_,_,[l;_]) } }) -> l
- | _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond e
+ | _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond post
in
- let term' = Logic_utils.expr_to_term ~cast:false exp in
- let term' = Logic_utils.mk_cast Cil.intType term' in
+ let term' = Logic_utils.expr_to_term ~coerce:false exp in
if check && not (Cil_datatype.Term.equal term term') then
Kernel.fatal
"translation of C expression %a is %a, inconsistent with logic term %a"
@@ -29,7 +28,7 @@ let treat_fct check fct =
let stmts = (Kernel_function.get_definition fct).sbody.bstmts in
let stmts =
List.filter
- (function
+ (function
{ skind = Instr (Set (lv,_,_)) } ->
(match lv with (Var v,_) -> v.vglob | _ -> true)
| { skind = If _ } -> true
@@ -41,7 +40,7 @@ let treat_fct check fct =
(* A bit fragile, but should do the trick as long as the test itself does
not get too complicated (regarding the C code at least). *)
if not (List.length stmts = List.length ensures) then
- Kernel.fatal
+ Kernel.fatal
"Stmts:@\n%a@\nPreds:@\n%a@\n"
(Pretty_utils.pp_list ~sep:"@\n@\n" Printer.pp_stmt) stmts
(Pretty_utils.pp_list ~sep:"@\n@\n" Printer.pp_post_cond) ensures;
@@ -52,9 +51,12 @@ 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 true g
-
+ let h = Globals.Functions.find_by_name "h" in
+ begin
+ treat_fct true main;
+ treat_fct false f;
+ treat_fct true g;
+ treat_fct true h;
+ end
let () = Db.Main.extend compute
diff --git a/tests/spec/oracle/cast_enum_bts1546.0.res.oracle b/tests/spec/oracle/cast_enum_bts1546.0.res.oracle
index 859426aa635fc488beca0b51816d51a6201d5d15..8a5f937eecdd7fa43e78b21ef4a70b88991fc0d0 100644
--- a/tests/spec/oracle/cast_enum_bts1546.0.res.oracle
+++ b/tests/spec/oracle/cast_enum_bts1546.0.res.oracle
@@ -39,7 +39,7 @@ enum e f(enum e x)
return __retres;
}
-/*@ ensures P: \result ≡ (unsigned int)E0; */
+/*@ ensures P: \result ≡ E0; */
enum e g(enum e x)
{
enum e __retres;
diff --git a/tests/spec/oracle/expr_to_term.res.oracle b/tests/spec/oracle/expr_to_term.res.oracle
index a378207a1b9cec63fef9d84d30052cc663076a14..fcb612aeeffb7d9c85f1f1ab6724eb0bb42c00e0 100644
--- a/tests/spec/oracle/expr_to_term.res.oracle
+++ b/tests/spec/oracle/expr_to_term.res.oracle
@@ -4,12 +4,14 @@ struct S {
int y ;
int z ;
};
+/*@
+predicate int_eq(int logical, int from_stmt_id) = logical ≡ from_stmt_id;
+ */
int x[10];
struct S s;
int t;
-/*@ predicate int_eq(int logical, int from_c) = logical ≡ from_c;
- */
-/*@ ensures int_eq(*((int *)(0x1 + 0x2)), *((int *)(0x1 + 0x2)));
+/*@ ensures
+ int_eq(*((int *)(0x1 + 0x2)), *((int *)((unsigned int)(0x1 + 0x2))));
ensures int_eq(*((int *)(0x1 + 0x2)), (int)0);
*/
int f(void)
@@ -40,8 +42,8 @@ int main(void)
return __retres;
}
-/*@ ensures int_eq((int)(!(t ≢ 0)), (int)(!(t ≢ 0)));
- ensures int_eq((int)(!(t ≢ 0)), (int)5);
+/*@ ensures int_eq((int)(t ≢ 0? 0: 1), (int)(t ≢ 0? 0: 1));
+ ensures int_eq((int)(t ≢ 0? 0: 1), (int)5);
*/
int g(void)
{
@@ -57,4 +59,21 @@ int g(void)
return_label: return __retres;
}
+/*@ ensures int_eq((int)(t < 5? 1: 0), (int)(t < 5? 1: 0));
+ ensures int_eq((int)(t < 5? 1: 0), (int)6);
+ */
+int h(void)
+{
+ int __retres;
+ if (t < 5) {
+ __retres = 2;
+ goto return_label;
+ }
+ else {
+ __retres = 3;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
diff --git a/tests/spec/oracle/null_ptr.res.oracle b/tests/spec/oracle/null_ptr.res.oracle
index 5412691e03a9c6d7725e8c152d128c7d7cfe42d4..c33037bd34a749312d9fff4efaf9cc42e3659b39 100644
--- a/tests/spec/oracle/null_ptr.res.oracle
+++ b/tests/spec/oracle/null_ptr.res.oracle
@@ -10,12 +10,12 @@
*/
/*@ predicate eq(char *x, char *y) = x ≡ y;
*/
-/*@ predicate my_null(char *x) = x ≡ (char *)((void *)0);
+/*@ predicate my_null(char *x) = x ≡ (char *)0;
*/
void f(char *x)
{
x = (char *)0;
- /*@ assert x ≡ (char *)((void *)0); */ ;
+ /*@ assert x ≡ (char *)0; */ ;
/*@ assert my_null(x); */ ;
/*@ assert null(x); */ ;
/*@ assert eq(x, (char *)0); */ ;
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index 45fd238338830505dfb51f5e815426113210c637..41512d12b91061aab693700eb907c7e937b17b62 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,5 +1,5 @@
/* run.config*
- FILTER: sed 's|/tmp/[^ ]*\.i|/tmp/FILE.i|g'
+ FILTER: sed 's:/\(tmp\|var\)/[^ ]*\.i:/tmp/FILE.i:g'
OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
OPT: -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\" \"using \\% has no effect : \$(basename \"\%input\")\""
diff --git a/tests/syntax/oracle/assembly_gmp.1.res.oracle b/tests/syntax/oracle/assembly_gmp.1.res.oracle
index 63a12b1b07bab4c049fb972e2f853cc2330cf8dd..70ffc4d780c3a76abd0e4e060e91dec0c49f39e2 100644
--- a/tests/syntax/oracle/assembly_gmp.1.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.1.res.oracle
@@ -38,9 +38,9 @@ mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
p0 = (long)(__m0 * __m1);
}
/*@ assigns r2, r1, r0;
- assigns r2 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r1 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r0 \from r0, p1, *(ap + (n - 3)), p0;
+ assigns r2 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
+ assigns r1 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
+ assigns r0 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
*/
__asm__ (
"add\t%6, %q2\n\t"
diff --git a/tests/syntax/oracle/assembly_gmp.2.res.oracle b/tests/syntax/oracle/assembly_gmp.2.res.oracle
index 2684a9a66550dfd450d38cd9166036597ebdab3b..d3e9aca3737cce222093576d7e70a7e44cf4d481 100644
--- a/tests/syntax/oracle/assembly_gmp.2.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.2.res.oracle
@@ -38,9 +38,9 @@ mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
p0 = (long)(__m0 * __m1);
}
/*@ assigns r2, r1, r0;
- assigns r2 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r1 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r0 \from r0, p1, *(ap + (n - 3)), p0;
+ assigns r2 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
+ assigns r1 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
+ assigns r0 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
*/
__asm__ (
"add%I6c\t%2, %5, %6\n\t"
diff --git a/tests/syntax/oracle/undeclared_local_bts1113.res.oracle b/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
index 809576ab5a896f46826575c7a6cba00ccf7a8bff..97b551d63eb90d30964fb8910c53a61c73f989fd 100644
--- a/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
+++ b/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
@@ -16,19 +16,25 @@ void funk(int rounds)
int i;
unsigned int __lengthof_k_long_long_size;
int k_positive_size[4 - 2];
- /*@ assert alloca_bounds: 0 < sizeof(int) * (2 * rounds) ≤ 4294967295; */
+ /*@
+ assert alloca_bounds: 0 < sizeof(int) * (int)(2 * rounds) ≤ 4294967295;
+ */
;
__lengthof_k = (unsigned int)(2 * rounds);
int *k = __fc_vla_alloc(sizeof(int) * __lengthof_k);
/*@
assert
- alloca_bounds: 0 < sizeof(int) * (unsigned int)(2 * rounds) ≤ 4294967295;
+ alloca_bounds:
+ 0 < sizeof(int) * (unsigned int)((int)(2 * rounds)) ≤ 4294967295;
*/
;
__lengthof_kk = (unsigned int)(2 * rounds);
int *kk = __fc_vla_alloc(sizeof(int) * __lengthof_kk);
long long j = (long long)(rounds * rounds);
- /*@ assert alloca_bounds: 0 < sizeof(int) * (j * 2) ≤ 4294967295; */ ;
+ /*@
+ assert alloca_bounds: 0 < sizeof(int) * (long long)(j * 2) ≤ 4294967295;
+ */
+ ;
__lengthof_k_long_long_size = (unsigned int)(j * (long long)2);
int *k_long_long_size =
__fc_vla_alloc(sizeof(int) * __lengthof_k_long_long_size);
diff --git a/tests/syntax/oracle/vla_strlen.res.oracle b/tests/syntax/oracle/vla_strlen.res.oracle
index 49dc5fb0597065d6ebcc3a9412b46b1a04719d72..0fe38231c89af62740bef5c9bca1ab60a670c39d 100644
--- a/tests/syntax/oracle/vla_strlen.res.oracle
+++ b/tests/syntax/oracle/vla_strlen.res.oracle
@@ -17,7 +17,11 @@ void f(char *s)
unsigned int __lengthof_t;
size_t tmp;
tmp = strlen((char const *)s);
- /*@ assert alloca_bounds: 0 < sizeof(char) * (tmp + 1) ≤ 4294967295; */ ;
+ /*@
+ assert
+ alloca_bounds: 0 < sizeof(char) * (unsigned int)(tmp + 1) ≤ 4294967295;
+ */
+ ;
__lengthof_t = tmp + (size_t)1;
char *t = __fc_vla_alloc(sizeof(char) * __lengthof_t);
char *p = t;
diff --git a/tests/value/oracle/CruiseControl.res.oracle b/tests/value/oracle/CruiseControl.res.oracle
index f7ec6058482ccd412e0d0ba211c2ec94993c08a5..42ea97e36d2fe6087189c3437ab4719b952c7a8d 100644
--- a/tests/value/oracle/CruiseControl.res.oracle
+++ b/tests/value/oracle/CruiseControl.res.oracle
@@ -37,17 +37,19 @@
Called from tests/value/CruiseControl.c:242.
[eva:alarm] tests/value/CruiseControl.c:172: Warning:
non-finite float value.
- assert \is_finite((float)(_C_->_L1_CruiseControl - _C_->_L2_CruiseControl));
+ assert
+ \is_finite(\sub_float(_C_->_L1_CruiseControl, _C_->_L2_CruiseControl));
[eva:alarm] tests/value/CruiseControl.c:175: Warning:
non-finite float value.
- assert \is_finite((float)(_C_->_L3_CruiseControl * _C_->_L6_CruiseControl));
+ assert
+ \is_finite(\mul_float(_C_->_L3_CruiseControl, _C_->_L6_CruiseControl));
[eva:alarm] tests/value/CruiseControl.c:194: Warning:
non-finite float value.
assert
- \is_finite((float)(_C_->_L16_CruiseControl + _C_->_L18_CruiseControl));
+ \is_finite(\add_float(_C_->_L16_CruiseControl, _C_->_L18_CruiseControl));
[eva:alarm] tests/value/CruiseControl.c:199: Warning:
non-finite float value.
- assert \is_finite((float)(_C_->ProportionnalAction + _C_->IntegralAction));
+ assert \is_finite(\add_float(_C_->ProportionnalAction, _C_->IntegralAction));
[eva] computing for function SaturateThrottle <- ThrottleRegulation <-
ThrottleCmd <- CruiseControl.
Called from tests/value/CruiseControl.c:202.
diff --git a/tests/value/oracle/bts1306.res.oracle b/tests/value/oracle/bts1306.res.oracle
index cae97e181bce3b4cd4ec6d54740d1865ca77e109..f0036f751b5313034ee6be275ecd516dc6b0d154 100644
--- a/tests/value/oracle/bts1306.res.oracle
+++ b/tests/value/oracle/bts1306.res.oracle
@@ -7,7 +7,7 @@
[eva] computing for function g <- main.
Called from tests/value/bts1306.i:9.
[eva:alarm] tests/value/bts1306.i:5: Warning:
- non-finite double value. assert \is_finite((double)(x * x));
+ non-finite double value. assert \is_finite(\mul_double(x, x));
[eva] Recording results for g
[eva] Done for function g
[eva] Recording results for main
@@ -20,7 +20,7 @@
/* Generated by Frama-C */
void g(double x)
{
- /*@ assert Eva: is_nan_or_infinite: \is_finite((double)(x * x)); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(\mul_double(x, x)); */
double y = x * x;
return;
}
@@ -42,7 +42,7 @@ int main(double x)
[eva] computing for function g <- main.
Called from tests/value/bts1306.i:9.
[eva:alarm] tests/value/bts1306.i:5: Warning:
- non-finite double value. assert \is_finite((double)(x * x));
+ non-finite double value. assert \is_finite(\mul_double(x, x));
[eva] Recording results for g
[eva] Done for function g
[eva] Recording results for main
@@ -55,7 +55,7 @@ int main(double x)
/* Generated by Frama-C */
void g(double x)
{
- /*@ assert Eva: is_nan_or_infinite: \is_finite((double)(x * x)); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(\mul_double(x, x)); */
double y = x * x;
return;
}
diff --git a/tests/value/oracle/const.res.oracle b/tests/value/oracle/const.res.oracle
index 857b44485fb8b2726177f21bf24a680cbbb9ff97..5836c004bf9e267db3186acd7fb6a78a3b5b7c3c 100644
--- a/tests/value/oracle/const.res.oracle
+++ b/tests/value/oracle/const.res.oracle
@@ -141,6 +141,8 @@
[eva] done for function main
[eva] tests/value/const.i:21:
assertion 'Eva,mem_access' got final status invalid.
+[eva] tests/value/const.i:26:
+ assertion 'Eva,mem_access' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function aux_ret_const:
__retres ∈ {1}
diff --git a/tests/value/oracle/descending.res.oracle b/tests/value/oracle/descending.res.oracle
index 3b11d3495c607a8fe2f9068f6ac1faa87a5d17f6..7e67df6441b64d7719631c3bc6a09fc8caf77f81 100644
--- a/tests/value/oracle/descending.res.oracle
+++ b/tests/value/oracle/descending.res.oracle
@@ -14,7 +14,7 @@
[eva:alarm] tests/value/descending.i:13: Warning:
accessing out of bounds index. assert (int)(i - 1) < 10;
[eva:alarm] tests/value/descending.i:13: Warning:
- accessing uninitialized left-value. assert \initialized(&A[i - 1]);
+ accessing uninitialized left-value. assert \initialized(&A[(int)(i - 1)]);
[eva] Recording results for test1
[eva] Done for function test1
[eva] computing for function test2 <- main.
diff --git a/tests/value/oracle/downcast.0.res.oracle b/tests/value/oracle/downcast.0.res.oracle
index c27a3ff663f1e3ba23a8e2cf6cc34c19e724e10e..3bcfeedcaf1a4fcf05706f41e611665214e4e489 100644
--- a/tests/value/oracle/downcast.0.res.oracle
+++ b/tests/value/oracle/downcast.0.res.oracle
@@ -28,9 +28,9 @@
[eva] computing for function main4_pointer <- main.
Called from tests/value/downcast.i:159.
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+ signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+ signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva] Recording results for main4_pointer
[eva] Done for function main4_pointer
[eva] computing for function main5_wrap_signed <- main.
diff --git a/tests/value/oracle/downcast.1.res.oracle b/tests/value/oracle/downcast.1.res.oracle
index 4430fdae7754b7ca73df1a85b6314fffe75916ad..80b62a21f498dfb27b00b455bd4709bb5043756c 100644
--- a/tests/value/oracle/downcast.1.res.oracle
+++ b/tests/value/oracle/downcast.1.res.oracle
@@ -40,9 +40,9 @@
[eva] computing for function main4_pointer <- main.
Called from tests/value/downcast.i:159.
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+ signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+ signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva:alarm] tests/value/downcast.i:56: Warning:
signed downcast. assert -2147483648 ≤ p;
[eva:alarm] tests/value/downcast.i:56: Warning:
diff --git a/tests/value/oracle/downcast.2.res.oracle b/tests/value/oracle/downcast.2.res.oracle
index 0c43f9fb2f787dbfc9aa221ef2c9387f3ed6f8c6..ce711f9fe6aa4528c8f1a9e7f06cdfac216fd10a 100644
--- a/tests/value/oracle/downcast.2.res.oracle
+++ b/tests/value/oracle/downcast.2.res.oracle
@@ -42,9 +42,9 @@
[eva] computing for function main4_pointer <- main.
Called from tests/value/downcast.i:159.
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+ signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+ signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva:alarm] tests/value/downcast.i:55: Warning:
unsigned downcast. assert 0 ≤ p;
[eva:alarm] tests/value/downcast.i:55: Warning:
diff --git a/tests/value/oracle/downcast.3.res.oracle b/tests/value/oracle/downcast.3.res.oracle
index d25d52f4759afa0aabbfca5eb6c5cd47d4312a86..8d2a9ee99b2b0162311fae95e37a7c09cc0ef24d 100644
--- a/tests/value/oracle/downcast.3.res.oracle
+++ b/tests/value/oracle/downcast.3.res.oracle
@@ -38,9 +38,9 @@
[eva] computing for function main4_pointer <- main.
Called from tests/value/downcast.i:159.
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+ signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+ signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva:alarm] tests/value/downcast.i:56: Warning:
signed downcast. assert -2147483648 ≤ p;
[eva:alarm] tests/value/downcast.i:56: Warning:
@@ -61,7 +61,7 @@
[eva] computing for function main6_val_warn_converted_signed <- main.
Called from tests/value/downcast.i:161.
[eva:alarm] tests/value/downcast.i:75: Warning:
- signed downcast. assert (int)65300u ≤ 32767;
+ signed downcast. assert 65300u ≤ 32767;
[eva:alarm] tests/value/downcast.i:91: Warning:
signed downcast. assert -32768 ≤ (int)e_1;
[eva:alarm] tests/value/downcast.i:95: Warning:
diff --git a/tests/value/oracle/downcast.4.res.oracle b/tests/value/oracle/downcast.4.res.oracle
index d691ffe3fe111924fcefe788f39991a23f6f2f9b..b2070c3d348f6208a80e688e7ae51a13d6f69a70 100644
--- a/tests/value/oracle/downcast.4.res.oracle
+++ b/tests/value/oracle/downcast.4.res.oracle
@@ -28,9 +28,9 @@
[eva] computing for function main4_pointer <- main.
Called from tests/value/downcast.i:159.
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert -9223372036854775808 ≤ p + (long long)100;
+ signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] tests/value/downcast.i:54: Warning:
- signed overflow. assert p + (long long)100 ≤ 9223372036854775807;
+ signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva] Recording results for main4_pointer
[eva] Done for function main4_pointer
[eva] computing for function main5_wrap_signed <- main.
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 7cf52beab44793b0f3ed8c99f8dc13f610b85e11..bf8af26b55f010cf2427c09aeae8f0e9ad55183d 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -277,7 +277,7 @@
signed overflow. assert -2147483648 ≤ numNonZero - 1;
[eva:alarm] tests/value/gauges.c:202: Warning:
non-finite float value.
- assert \is_finite((float)(*p * (float)(*tmp * *tmp_0)));
+ assert \is_finite(\mul_float(*p, \mul_float(*tmp, *tmp_0)));
(tmp from A++, tmp_0 from B++)
[eva] Recording results for main10_aux
[eva] Done for function main10_aux
diff --git a/tests/value/oracle/incompatible_states.res.oracle b/tests/value/oracle/incompatible_states.res.oracle
index 9cd3bb24391f4465605fdb1d0b224608334bcc3d..d020cc431768e426b4883194da3f4b86841a0c0a 100644
--- a/tests/value/oracle/incompatible_states.res.oracle
+++ b/tests/value/oracle/incompatible_states.res.oracle
@@ -22,9 +22,11 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] tests/value/incompatible_states.c:38: Warning:
- accessing uninitialized left-value. assert \initialized(&t[(2 * i) / 2]);
+ accessing uninitialized left-value.
+ assert \initialized(&t[(int)((int)(2 * i) / 2)]);
[eva:alarm] tests/value/incompatible_states.c:41: Warning:
- accessing uninitialized left-value. assert \initialized(&t[(2 * i) / 2]);
+ accessing uninitialized left-value.
+ assert \initialized(&t[(int)((int)(2 * i) / 2)]);
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index abf27f96c2e64aa9abb9a239c22e5330e3b3cdf1..16be4cd6f9d1bd4e952d9eebfe1bfd3987072a4d 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -129,7 +129,7 @@
[eva:alarm] tests/value/library.i:44: Warning:
non-finite float value. assert \is_finite(*pf);
[eva:alarm] tests/value/library.i:44: Warning:
- non-finite float value. assert \is_finite((float)(*pf + *pf));
+ non-finite float value. assert \is_finite(\add_float(*pf, *pf));
[eva] computing for function k <- main.
Called from tests/value/library.i:45.
[eva] using specification for function k
diff --git a/tests/value/oracle/pointer_comparison.0.res.oracle b/tests/value/oracle/pointer_comparison.0.res.oracle
index 6ac5900dc2e425cc69bd9317d1baadd5b41e2e7f..0202337ff61b091c94af6196bc605e43313ef656 100644
--- a/tests/value/oracle/pointer_comparison.0.res.oracle
+++ b/tests/value/oracle/pointer_comparison.0.res.oracle
@@ -194,7 +194,8 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer comparison. assert \pointer_comparable((void *)p, (void *)(&y));
+ pointer comparison.
+ assert \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:alarm] tests/value/pointer_comparison.c:18: Warning:
@@ -254,7 +255,8 @@
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
assert
- Eva: ptr_comparison: \pointer_comparable((void *)p, (void *)(&y));
+ Eva: ptr_comparison:
+ \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
assert
diff --git a/tests/value/oracle/pointer_comparison.1.res.oracle b/tests/value/oracle/pointer_comparison.1.res.oracle
index cd63714dccccd315f1b03fddceefecccc8f7ddd8..0f48c4ee7e0a0f10c28b128a2b8f6ccc00f590cf 100644
--- a/tests/value/oracle/pointer_comparison.1.res.oracle
+++ b/tests/value/oracle/pointer_comparison.1.res.oracle
@@ -221,7 +221,8 @@
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
pointer downcast. assert (unsigned int)(&y) ≤ 2147483647;
[eva:alarm] tests/value/pointer_comparison.c:16: Warning:
- pointer comparison. assert \pointer_comparable((void *)p, (void *)(&y));
+ pointer comparison.
+ assert \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
[eva] tests/value/pointer_comparison.c:16: Frama_C_show_each_5: {{ &x + {16} }}
[eva] tests/value/pointer_comparison.c:17: Frama_C_show_each_5e: {{ &x + {16} }}
[eva:alarm] tests/value/pointer_comparison.c:18: Warning:
@@ -282,7 +283,8 @@
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 16)
assert
- Eva: ptr_comparison: \pointer_comparable((void *)p, (void *)(&y));
+ Eva: ptr_comparison:
+ \pointer_comparable((void *)((int)p), (void *)((int)(&y)));
tried with Eva.
[ - ] Assertion 'Eva,ptr_comparison' (file tests/value/pointer_comparison.c, line 18)
assert
diff --git a/tests/value/oracle/propagate_bottom.res.oracle b/tests/value/oracle/propagate_bottom.res.oracle
index 2b291b99b1160a933b7e4e50c6cbd1bfc4df425f..84b9c0efca5685428362ae64672e2f16403634f0 100644
--- a/tests/value/oracle/propagate_bottom.res.oracle
+++ b/tests/value/oracle/propagate_bottom.res.oracle
@@ -17,17 +17,23 @@
[eva:alarm] tests/value/propagate_bottom.i:20: Warning:
division by zero. assert 0 ≢ 0;
[eva:alarm] tests/value/propagate_bottom.i:25: Warning:
- non-finite double value. assert \is_finite((double)(1. / (double)0));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0));
[eva:alarm] tests/value/propagate_bottom.i:28: Warning:
- non-finite double value. assert \is_finite((double)(1. / (double)0));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0));
[eva:alarm] tests/value/propagate_bottom.i:31: Warning:
- non-finite double value. assert \is_finite((double)(1. / (double)0));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0));
[eva:alarm] tests/value/propagate_bottom.i:34: Warning:
- non-finite double value. assert \is_finite((double)(1. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0.));
[eva:alarm] tests/value/propagate_bottom.i:37: Warning:
- non-finite double value. assert \is_finite((double)(1. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0.));
[eva:alarm] tests/value/propagate_bottom.i:40: Warning:
- non-finite double value. assert \is_finite((double)(1. / 0.));
+ non-finite double value.
+ assert \is_finite(\div_double((double)1., (double)0.));
[eva] Recording results for main
[eva] done for function main
[eva] tests/value/propagate_bottom.i:5:
diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle
index adc483ff665929f6a5ccbcac65eee15f7da03395..aa8dc50d410df0a8961e66ac04949f144fedee20 100644
--- a/tests/value/oracle/sizeof.res.oracle
+++ b/tests/value/oracle/sizeof.res.oracle
@@ -25,16 +25,16 @@
The imprecision originates from Arithmetic {tests/value/sizeof.i:32}
[eva:alarm] tests/value/sizeof.i:33: Warning:
accessing out of bounds index.
- assert (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ assert (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
[eva:alarm] tests/value/sizeof.i:33: Warning:
out of bounds write.
- assert \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ assert \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
[eva:alarm] tests/value/sizeof.i:34: Warning:
accessing out of bounds index.
- assert (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ assert (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
[eva:alarm] tests/value/sizeof.i:34: Warning:
out of bounds write.
- assert \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ assert \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function f <- main.
@@ -129,19 +129,21 @@ void main2(void)
/*@ assert Eva: pointer_downcast: (unsigned int)(&s1) ≤ 2147483647; */
struct s *p = (& s1 + (int)(& s1)) - (int)(& s1);
/*@ assert
- Eva: index_bound: (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ Eva: index_bound:
+ (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
*/
/*@ assert
Eva: mem_access:
- \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
*/
p->t[sizeof(s1.t) - (unsigned int)i] = 1;
/*@ assert
- Eva: index_bound: (unsigned int)(sizeof(s1.t) - (unsigned int)i) < 10;
+ Eva: index_bound:
+ (unsigned int)(sizeof(int [10]) - (unsigned int)i) < 10;
*/
/*@ assert
Eva: mem_access:
- \valid(&p->t[(unsigned int)(sizeof(s1.t) - (unsigned int)i)]);
+ \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]);
*/
p->t[sizeof(s1.t) - (unsigned int)i] = 2;
return;
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index f5bcadc1abb5d0f1908434ef0ff16c53d5cdbe34..8c983fd90a289be87579fd40cfe9efbde6414a90 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -30,7 +30,7 @@
[eva:alarm] tests/value/summary.i:34: Warning:
non-finite double value. assert \is_finite(volatile_d);
[eva:alarm] tests/value/summary.i:35: Warning:
- non-finite double value. assert \is_finite((double)(d - d));
+ non-finite double value. assert \is_finite(\sub_double(d, d));
[eva:alarm] tests/value/summary.i:36: Warning:
overflow in conversion from floating-point to integer.
assert -2147483649 < d;
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 80d3ffdb4b19723e3faea13031852ffe5fbcb15e..3e988afe4882c009bbfa39e4f7c73ed77f551148 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -52,7 +52,7 @@
[eva:alarm] tests/value/summary.i:35: Warning:
assertion 'rte,is_nan_or_infinite' got status unknown.
[eva:alarm] tests/value/summary.i:35: Warning:
- non-finite double value. assert \is_finite((double)(d - d));
+ non-finite double value. assert \is_finite(\sub_double(d, d));
[eva:alarm] tests/value/summary.i:36: Warning:
assertion 'rte,float_to_int' got status unknown.
[eva:alarm] tests/value/summary.i:39: Warning: