Skip to content

GitLab

Commit 19a1a060 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'fix/virgile/579-compile-constant-float' into 'master' 

const-fold floating point

Closes #579

See merge request frama-c/frama-c!2553
parents d7796be3 3b9e7308
Hide whitespace changes
Inline Side-by-side
.gitignore
View file @ 19a1a060
......@@ -41,16 +41,22 @@ autom4te.cache
.Makefile.plugin.generated
#tests
/tests/ptests_config
/tests/**/result/
/tests/**/result_*/
/tests/crowbar/*constfold
/tests/crowbar/integer_bb_pretty
/tests/crowbar/mutable
/tests/crowbar/output-*
/tests/crowbar/test_ghost_cfg
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
/tests/*/*.opt
/tests/pdg/*.dot
/tests/crowbar/output-*
/tests/crowbar/mutable
/devel_tools/fc-time
/devel_tools/fc-memuse
/bin/ocamldep_transitive_closure
......@@ -104,6 +110,8 @@ autom4te.cache
/doc/code/qed
/doc/code/wp
/doc/doxygen
/doc/pdg/call-f.eps
/doc/pdg/call-f.fig
/doc/pdg/call-f.pdf
......@@ -186,10 +194,18 @@ Makefile.plugin.generated
/src/kernel_internals/parsing/clexer.ml
/src/kernel_internals/parsing/cparser.ml
/src/kernel_internals/parsing/cparser.mli
/src/plugins/value/domains/apron/apron_domain.ml
/src/plugins/value/domains/numerors/numerors_domain.ml
/src/kernel_services/ast_queries/json_compilation_database.ml
/src/libraries/stdlib/transitioning.ml
/src/plugins/gui/dgraph.ml
/src/plugins/gui/dgraph.mli
/src/plugins/gui/dgraph_helper.ml
/src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli
/src/plugins/gui/GSourceView2.ml
/src/plugins/gui/GSourceView2.mli
/src/plugins/gui/gtk_compat.ml
/src/plugins/value/domains/apron/apron_domain.ml
/src/plugins/value/domains/numerors/numerors_domain.ml
# generated tar.gz files
......@@ -199,14 +215,3 @@ hello-*.tar.gz
#######################
# should remain empty #
#######################
/src/plugins/gui/GSourceView2.mli
/src/plugins/gui/GSourceView2.ml
/src/plugins/gui/dgraph.ml
/src/plugins/gui/dgraph.mli
/src/plugins/gui/gtk_compat.ml
/src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli
/tests/crowbar/integer_bb_pretty
/src/plugins/gui/dgraph_helper.ml
/doc/doxygen
/tests/crowbar/test_ghost_cfg
Makefile
View file @ 19a1a060
......@@ -1438,6 +1438,10 @@ tests/crowbar/%: tests/crowbar/%.ml tests/crowbar/.%.depend .depend \
-deps tests/crowbar/.$*.depend -deps .depend) \
$<
tests/crowbar/full-link-%: tests/crowbar/%.ml lib/fc/frama-c.cmxa
$(OCAMLOPT) $(OLINKFLAGS) -ccopt "-Llib/fc" -w -42 -package crowbar -o $@ \
lib/fc/frama-c.cmxa $<
crowbar-%: tests/crowbar/%
$<
......
src/kernel_internals/typing/cabs2cil.ml
View file @ 19a1a060
......@@ -7199,58 +7199,49 @@ and doExp local_env
| ADrop -> ADrop
| _ -> AExp None
in
(* if we are evaluating a constant expression, e1 is supposed to
evaluate to either true or false statically, and we can type-check
only the appropriate branch. In fact, 6.6§3 seems to indicate that
the dead branch can contain sub-expressions that are normally
forbidden in a constant expression context, such as function calls.
*)
let is_true_cond = evaluate_cond_exp ce1 in
if asconst <> CNoConst && is_true_cond = `CTrue then begin
(* Now we must find the type of both branches, in order to compute
* the type of the result *)
let r2, se2, e2'o (* is an option. None means use e1 *), t2 =
match e2.expr_node with
| A.NOTHING ->
(match ce1 with
| CEExp (_,e) -> finishExp [] empty e (Cil.typeOf e)
| _ ->
finishExp
[] empty (Cil.one ~loc:e2.expr_loc) Cil.intType
(* e1 is the result of logic operations that by
definition of this branch evaluate to one. *))
| A.NOTHING -> begin (* The same as the type of e1 *)
match ce1 with
| CEExp (_, e1') ->
[], unspecified_chunk empty, None, typeOf e1'
(* Do not promote to bool *)
| _ -> [], unspecified_chunk empty, None, intType
end
| _ ->
let _,c2,e2,t2 =
(* if e1 is false, e2 is only interesting for its type, but
we won't evaluate it. Hence, it can contain
non-const constructions *)
let asconst =
if is_true_cond = `CFalse then CMayConst else asconst
in
let r2, se2, e2', t2 =
doExp (no_paren_local_env local_env) asconst e2 what'
in
clean_up_chunk_locals c2;
finishExp [] empty e2 t2
r2, se2, Some e2', t2
in
(* Do e3 for real. See above for the value of asconst *)
let asconst' = if is_true_cond = `CTrue then CMayConst else asconst in
let r3, se3, e3', t3 =
doExp (no_paren_local_env local_env) asconst' e3 what'
in
let tresult = conditionalConversion t2 t3 in
if asconst <> CNoConst && is_true_cond = `CTrue then begin
clean_up_chunk_locals se2;
clean_up_chunk_locals se3;
let loc = e2.expr_loc in
let e2' = match e2'o with None -> Cil.one ~loc | Some e -> e in
let _,e2' = castTo t2 tresult e2' in
finishExp [] empty e2' tresult;
end else if asconst <> CNoConst && is_true_cond = `CFalse then begin
let _,c3,e3,t3 =
doExp (no_paren_local_env local_env) asconst e3 what'
in
clean_up_chunk_locals c3;
finishExp [] empty e3 t3
clean_up_chunk_locals se2;
clean_up_chunk_locals se3;
let _,e3' = castTo t3 tresult e3' in
finishExp [] empty e3' tresult
end else begin
(* Now we must find the type of both branches, in order to compute
* the type of the result *)
let r2, se2, e2'o (* is an option. None means use e1 *), t2 =
match e2.expr_node with
| A.NOTHING -> begin (* The same as the type of e1 *)
match ce1 with
| CEExp (_, e1') ->
[], unspecified_chunk empty, None, typeOf e1'
(* Do not promote to bool *)
| _ -> [], unspecified_chunk empty, None, intType
end
| _ ->
let r2, se2, e2', t2 =
doExp (no_paren_local_env local_env) asconst e2 what'
in
r2, se2, Some e2', t2
in
(* Do e3 for real *)
let r3, se3, e3', t3 =
doExp (no_paren_local_env local_env) asconst e3 what'
in
let tresult = conditionalConversion t2 t3 in
if not (isEmpty se2) then
ConditionalSideEffectHook.apply (e,e2);
if not (isEmpty se3) then
......
src/kernel_services/ast_queries/cil.ml
View file @ 19a1a060
......@@ -208,8 +208,6 @@ let () =
let selfMachine_is_computed = TheMachine.is_computed
let debugConstFold = false
let new_exp ~loc e = { eloc = loc; eid = Cil_const.Eid.next (); enode = e }
let dummy_exp e = { eid = -1; enode = e; eloc = Cil_datatype.Location.unknown }
......@@ -3051,7 +3049,16 @@ let integer_constant i = CInt64(Integer.of_int i, IInt, None)
(* Construct an integer. Use only for values that fit on 31 bits *)
let integer ~loc (i: int) = new_exp ~loc (Const (integer_constant i))
let kfloat ~loc k f = new_exp ~loc (Const (CReal(f,k,None)))
let kfloat ~loc k f =
let is_single_precision =
match k with FFloat -> true | FDouble | FLongDouble -> false
in
let f =
if is_single_precision then
Floating_point.round_to_single_precision_float f
else f
in
new_exp ~loc (Const (CReal(f,k,None)))
let zero ~loc = integer ~loc 0
let one ~loc = integer ~loc 1
......@@ -3509,6 +3516,11 @@ let isArithmeticType t =
(TInt _ | TEnum _ | TFloat _) -> true
| _ -> false
let isLongDoubleType t =
match unrollTypeSkel t with
| TFloat(FLongDouble,_) -> true
| _ -> false
let isArithmeticOrPointerType t=
match unrollTypeSkel t with
| TInt _ | TEnum _ | TFloat _ | TPtr _ -> true
......@@ -4398,33 +4410,48 @@ and bitsOffset (baset: typ) (off: offset) : int * int =
See also {!Cil.constFoldVisitor}, which will run constFold on all
expressions in a given AST node.*)
and constFold (machdep: bool) (e: exp) : exp =
if debugConstFold then Kernel.debug "ConstFold to %a@." !pp_exp_ref e;
let dkey = Kernel.dkey_constfold in
Kernel.debug ~dkey "ConstFold %a@." !pp_exp_ref e;
let loc = e.eloc in
match e.enode with
BinOp(bop, e1, e2, tres) -> constFoldBinOp ~loc machdep bop e1 e2 tres
| UnOp(unop, e1, tres) -> begin
try
let tk =
match unrollTypeSkel tres with
| TInt(ik, _) -> ik
| TEnum (ei,_) -> ei.ekind
| _ -> raise Not_found (* probably a float *)
in
let e1c = constFold machdep e1 in
match e1c.enode with
Const(CInt64(i,_ik,repr)) -> begin
match unop with
Neg ->
let repr = Extlib.opt_map (fun s -> "-" ^ s) repr in
kinteger64 ~loc ?repr ~kind:tk (Integer.neg i)
| BNot -> kinteger64 ~loc ~kind:tk (Integer.lognot i)
| LNot ->
if Integer.equal i Integer.zero then one ~loc
else zero ~loc
end
| _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop, e1c, tres))
with Not_found -> e
| UnOp(unop, e1, tres) when isIntegralType tres -> begin
let tk =
match unrollTypeSkel tres with
| TInt(ik, _) -> ik
| TEnum (ei,_) -> ei.ekind
| _ -> assert false (* tres is an integral type *)
in
let e1c = constFold machdep e1 in
match e1c.enode with
Const(CInt64(i,_ik,repr)) -> begin
match unop with
Neg ->
let repr = Extlib.opt_map (fun s -> "-" ^ s) repr in
kinteger64 ~loc ?repr ~kind:tk (Integer.neg i)
| BNot -> kinteger64 ~loc ~kind:tk (Integer.lognot i)
| LNot ->
if Integer.equal i Integer.zero then one ~loc
else zero ~loc
end
| _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop, e1c, tres))
end
| UnOp(unop, e1, tres) when isArithmeticType tres -> begin
let tk =
match unrollTypeSkel tres with
| TFloat(fk,_) -> fk
| _ -> assert false (*tres is arithmetic but not integral, i.e. Float *)
in
let e1c = constFold machdep e1 in
match e1c.enode with
| Const (CReal(f,_,_)) -> begin
match unop with
| Neg -> kfloat ~loc tk (-. f)
| _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop,e1c,tres))
end
| _ -> if e1 == e1c then e else new_exp ~loc (UnOp(unop,e1c,tres))
end
| UnOp _ -> e
(* Characters are integers *)
| Const(CChr c) -> new_exp ~loc (Const(charConstToIntConstant c))
| Const(CEnum {eival = v}) -> constFold machdep v
......@@ -4468,16 +4495,14 @@ and constFold (machdep: bool) (e: exp) : exp =
end
| CastE (t, e) -> begin
if debugConstFold then
Kernel.debug "ConstFold CAST to to %a@." !pp_typ_ref t ;
Kernel.debug ~dkey "ConstFold CAST to %a@." !pp_typ_ref t ;
let e = constFold machdep e in
match e.enode, unrollType t with
| Const(CInt64(i,_k,_)),(TInt(nk,a)|TEnum({ekind = nk},a)) when a = [] ->
begin
(* If the cast has attributes, leave it alone. *)
if debugConstFold then
Kernel.debug "ConstFold to %a : %a@."
!pp_ikind_ref nk Datatype.Integer.pretty i;
Kernel.debug ~dkey "ConstFold to %a : %a@."
!pp_ikind_ref nk Datatype.Integer.pretty i;
(* Downcasts might truncate silently *)
kinteger64 ~loc ~kind:nk i
end
......@@ -4494,6 +4519,20 @@ and constFold (machdep: bool) (e: exp) : exp =
with Floating_point.Float_Non_representable_as_Int64 _ -> (* too big*)
new_exp ~loc (CastE (t, e))
end
| Const (CReal(f,_,_)), TFloat (FFloat,a) when a = [] ->
let f = Floating_point.round_to_single_precision_float f in
new_exp ~loc (Const (CReal (f,FFloat,None)))
| Const (CReal(f,_,_)), TFloat (FDouble,a) when a = [] ->
new_exp ~loc (Const (CReal (f,FDouble,None)))
(* We don't treat cast to long double, as we don't really know
how to handle this type anyway. *)
| Const (CInt64(i,_,_)), (TFloat(FFloat,a)) when a = [] ->
let f = Integer.to_float i in
let f = Floating_point.round_to_single_precision_float f in
new_exp ~loc (Const (CReal (f,FFloat,None)))
| Const (CInt64(i,_,_)), (TFloat(FDouble,a)) when a = [] ->
let f = Integer.to_float i in
new_exp ~loc (Const (CReal (f,FDouble,None)))
| _, _ -> new_exp ~loc (CastE (t, e))
end
| Lval lv -> new_exp ~loc (Lval (constFoldLval machdep lv))
......@@ -4651,6 +4690,18 @@ and constFoldBinOp ~loc (machdep: bool) bop e1 e2 tres =
| Gt, Const(CInt64(i1,ik1,_)),Const(CInt64(i2,ik2,_)) ->
let i1', i2', _ = convertInts i1 ik1 i2 ik2 in
if Integer.gt i1' i2' then one ~loc else zero ~loc
| Eq, Const(CReal(f1,fk1,_)),Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
if f1 = f2 then one ~loc else zero ~loc
| Ne, Const(CReal(f1,fk1,_)),Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
if f1 = f2 then zero ~loc else one ~loc
| Le, Const(CReal(f1,fk1,_)),Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
if f1 <= f2 then one ~loc else zero ~loc
| Ge, Const(CReal(f1,fk1,_)),Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
if f1 >= f2 then one ~loc else zero ~loc
| Lt, Const(CReal(f1,fk1,_)),Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
if f1 < f2 then one ~loc else zero ~loc
| Gt, Const(CReal(f1,fk1,_)),Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
if f1 > f2 then one ~loc else zero ~loc
(* We rely on the fact that LAnd/LOr appear in global initializers
and should not have side effects. *)
......@@ -4664,11 +4715,27 @@ and constFoldBinOp ~loc (machdep: bool) bop e1 e2 tres =
one ~loc
| _ -> new_exp ~loc (BinOp(bop, e1', e2', tres))
in
if debugConstFold then
Format.printf "Folded %a to %a@."
!pp_exp_ref (new_exp ~loc (BinOp(bop, e1', e2', tres)))
!pp_exp_ref newe;
Kernel.debug ~dkey:Kernel.dkey_constfold "Folded %a to %a@."
!pp_exp_ref (new_exp ~loc (BinOp(bop, e1', e2', tres)))
!pp_exp_ref newe;
newe
end else if isArithmeticType tres && not (isLongDoubleType tres) then begin
let tk =
match unrollTypeSkel tres with
| TFloat(fk,_) -> fk
| _ -> Kernel.fatal "constFoldBinOp: not a floating type"
in
match bop, e1'.enode, e2'.enode with
| PlusA, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
kfloat ~loc tk (f1 +. f2)
| MinusA, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
kfloat ~loc tk (f1 -. f2)
| Mult, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
kfloat ~loc tk (f1 *. f2)
| Div, Const(CReal(f1,fk1,_)), Const(CReal(f2,fk2,_)) when fk1 = fk2 ->
(*might be infinity or NaN, but that's still a float*)
kfloat ~loc tk (f1 /. f2)
| _ -> new_exp ~loc (BinOp(bop,e1',e2',tres))
end else
new_exp ~loc (BinOp(bop, e1', e2', tres))
......
src/kernel_services/plugin_entry_points/kernel.ml
View file @ 19a1a060
......@@ -49,6 +49,8 @@ let dkey_ast = register_category "ast"
let dkey_check = register_category "check"
let dkey_constfold = register_category "constfold"
let dkey_comments = register_category "parser:comments"
let dkey_dataflow = register_category "dataflow"
......
src/kernel_services/plugin_entry_points/kernel.mli
View file @ 19a1a060
......@@ -43,6 +43,8 @@ val dkey_ast: category
val dkey_check: category
val dkey_constfold: category
val dkey_comments: category
val dkey_compilation_db: category
......
src/libraries/utils/floating_point.mli
View file @ 19a1a060
......@@ -28,18 +28,16 @@ type c_rounding_mode =
val string_of_c_rounding_mode : c_rounding_mode -> string
(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
[@@@ warning "-3"]
external set_round_downward : unit -> unit = "set_round_downward" "noalloc"
external set_round_upward : unit -> unit = "set_round_upward" "noalloc"
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_toward_zero : unit -> unit = "set_round_toward_zero" "noalloc"
external get_rounding_mode: unit -> c_rounding_mode = "get_rounding_mode" "noalloc"
external set_rounding_mode: c_rounding_mode -> unit = "set_rounding_mode" "noalloc"
[@@@ warning "+3"]
"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 =
"get_rounding_mode" [@@noalloc]
external set_rounding_mode: c_rounding_mode -> unit =
"set_rounding_mode" [@@noalloc]
external round_to_single_precision_float: float -> float = "round_to_float"
......
src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
View file @ 19a1a060
......@@ -20,9 +20,6 @@ int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_assert(3. != 1.5,(char *)"Assertion",(char *)"main",
(char *)"3 != 1.5",12);
/*@ assert 3 ≢ 1.5; */ ;
{
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
......@@ -42,7 +39,7 @@ int main(void)
__gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"3 == 1.5 + 1.5",13);
(char *)"3 == 1.5 + 1.5",12);
__gmpq_clear(__gen_e_acsl_);
__gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl__3);
......@@ -57,12 +54,12 @@ int main(void)
__gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
(char *)"main",(char *)"0.1 == 0.1",14);
(char *)"main",(char *)"0.1 == 0.1",13);
__gmpq_clear(__gen_e_acsl__4);
}
/*@ assert 0.1 ≡ 0.1; */ ;
__e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
(char *)"(double)1.0 == 1.0",15);
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(double)1.0 == 1.0",14);
/*@ assert (double)1.0 ≡ 1.0; */ ;
{
__e_acsl_mpq_t __gen_e_acsl__5;
......@@ -78,7 +75,7 @@ int main(void)
__gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
(char *)"(double)0.1 != 0.1",16);
(char *)"(double)0.1 != 0.1",15);
__gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl__7);
}
......@@ -97,7 +94,7 @@ int main(void)
*/
__e_acsl_assert((double)((float)__gen_e_acsl__9) != __gen_e_acsl__10,
(char *)"Assertion",(char *)"main",
(char *)"(float)0.1 != (double)0.1",17);
(char *)"(float)0.1 != (double)0.1",16);
__gmpq_clear(__gen_e_acsl__8);
}
/*@ assert (float)0.1 ≢ (double)0.1; */ ;
......@@ -126,7 +123,7 @@ int main(void)
__gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",18);
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",17);
__gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__14);
......@@ -161,7 +158,7 @@ int main(void)
__gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
(char *)"main",(char *)"1 + 0.1 == 2 - 0.9",19);
(char *)"main",(char *)"1 + 0.1 == 2 - 0.9",18);
__gmpq_clear(__gen_e_acsl__16);
__gmpq_clear(__gen_e_acsl__17);
__gmpq_clear(__gen_e_acsl_add_3);
......@@ -192,7 +189,7 @@ int main(void)
__gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",23);
(char *)"main",(char *)"sum != x * y",22);
__gmpq_clear(__gen_e_acsl_y);
__gmpq_clear(__gen_e_acsl__20);
__gmpq_clear(__gen_e_acsl_mul);
......@@ -220,7 +217,7 @@ int main(void)
__gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
(char *)"main",(char *)"1.1d != 1 + 0.1",30);
(char *)"main",(char *)"1.1d != 1 + 0.1",29);
__gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl__23);
__gmpq_clear(__gen_e_acsl_add_4);
......
src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
View file @ 19a1a060
[kernel:parser:decimal-float] tests/arith/rationals.c:20: Warning:
[kernel:parser:decimal-float] tests/arith/rationals.c:19: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/arith/rationals.c:17: Warning:
[e-acsl] tests/arith/rationals.c:16: Warning:
E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/arith/rationals.c:13: Warning:
[eva:alarm] tests/arith/rationals.c:12: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:14: Warning:
[eva:alarm] tests/arith/rationals.c:13: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:14: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:16: Warning:
[eva:alarm] tests/arith/rationals.c:13: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:15: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6);
[eva:alarm] tests/arith/rationals.c:16: Warning:
[eva:alarm] tests/arith/rationals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:17: Warning:
[eva:alarm] tests/arith/rationals.c:15: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:16: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] tests/arith/rationals.c:17: Warning:
[eva:alarm] tests/arith/rationals.c:16: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
[eva:alarm] tests/arith/rationals.c:17: Warning:
[eva:alarm] tests/arith/rationals.c:16: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
[eva:alarm] tests/arith/rationals.c:17: Warning:
[eva:alarm] tests/arith/rationals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:18: Warning:
[eva:alarm] tests/arith/rationals.c:17: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/arith/rationals.c:17: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:17: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:18: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:19: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:23: Warning:
[eva:alarm] tests/arith/rationals.c:22: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:4: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:4: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
[eva:alarm] tests/arith/rationals.c:30: Warning:
[eva:alarm] tests/arith/rationals.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:30: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:29: Warning: assertion got status unknown.
src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
View file @ 19a1a060
[kernel] Parsing tests/arith/rationals.c (with preprocessing)
[kernel:parser:decimal-float] tests/arith/rationals.c:20: Warning:
[kernel:parser:decimal-float] tests/arith/rationals.c:19: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
src/plugins/e-acsl/tests/arith/rationals.c
View file @ 19a1a060
......@@ -9,7 +9,6 @@ double avg(double a, double b) {
}
int main(void) {
/*@ assert 3 != 1.5; */ ;
/*@ assert 3 == 1.5 + 1.5; */ ;
/*@ assert 0.1 == 0.1; */ ;