diff --git a/.gitignore b/.gitignore
index 4803da7469b4c370aaa2751465c27be30a26c397..2b8b272dc8c3db14beee19536f597b09aac0f460 100644
--- a/.gitignore
+++ b/.gitignore
@@ -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
diff --git a/Makefile b/Makefile
index 42f3027d607538976c4081b72d9599c8990c398b..f957448149622595ff8b6905e187323dc27f3399 100644
--- a/Makefile
+++ b/Makefile
@@ -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/%
$<
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index e51686df1b00a4ccb394dfcc3d5de8476e8f7648..481fde16c7eb3a4bf955c7730e5107c74cd29c0c 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -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
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index b07aa521d24e2df794de12ce953d223341f51d6b..ef7e44c7b89ede003c9d485b7a5b6c544351af5a 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -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))
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 468438d093834bf3d11dcba23ae383702478c9fa..f52a143e1fd81843203fae6b3287d874108e57d9 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -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"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index d9e6e71f16b587a3bc481c545e095a62e503978b..b0170ce1a88d76ae84412fa161db8002d8e44a13 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -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
diff --git a/src/libraries/utils/floating_point.mli b/src/libraries/utils/floating_point.mli
index 8e82a0a59b39867adac48ab0f6eed8e32a7c8880..aadafebbebffc7583ea0306eb04633389476c185 100644
--- a/src/libraries/utils/floating_point.mli
+++ b/src/libraries/utils/floating_point.mli
@@ -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"
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 789a97a40cde83610a53a2a7468076e315b15f5d..2161d2fc0f7e7621343e918328102589aa8ca0bf 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
@@ -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);
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
index a6a2923fc7d78b732768d31af599c9bae4a98cc8..6b6e958fe3307d88f08470895bdaf3de1960c169 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
@@ -1,45 +1,45 @@
-[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.
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
index ab4a875d1ad88731e1251bb3bf2f3097a47a32ea..590199db8f04040ab84e966d5307b0dfc39f2ec5 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle
@@ -1,4 +1,4 @@
[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)
diff --git a/src/plugins/e-acsl/tests/arith/rationals.c b/src/plugins/e-acsl/tests/arith/rationals.c
index 84c8b0949b4d44178f43101ad840b05ad734d50e..18ed5111f7089b4cb079af9d45d206907818ee31 100644
--- a/src/plugins/e-acsl/tests/arith/rationals.c
+++ b/src/plugins/e-acsl/tests/arith/rationals.c
@@ -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; */ ;
/*@ assert (double)1.0 == 1.0; */ ;
diff --git a/tests/crowbar/constfold.ml b/tests/crowbar/constfold.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b98c69153c173ba6dd2cbae5cf252e3459196a44
--- /dev/null
+++ b/tests/crowbar/constfold.ml
@@ -0,0 +1,230 @@
+open Cabs
+open Crowbar
+
+let loc = Cabshelper.cabslu
+
+let gen_int_type =
+ choose [
+ const Tint;
+ const Tlong;
+ const Tunsigned;
+ ]
+
+let gen_type =
+ choose [
+ gen_int_type;
+ const Tfloat;
+ const Tdouble;
+ ]
+
+let mk_exp expr_node = { expr_loc = loc; expr_node }
+
+let needs_int_unary = function
+ | NOT | BNOT -> true
+ | _ -> false
+
+let gen_unary =
+ choose [
+ const NOT;
+ const BNOT;
+ const MINUS;
+ const PLUS;
+ ]
+
+(* NB: we don't generate shifts and division/modulo operands to avoid
+ undefined operations. Overflows alarms are deactivated as well. *)
+
+let needs_int_binary = function
+ | AND | OR | BAND | BOR | XOR -> true
+ | _ -> false
+
+let gen_binary =
+ choose [
+ const AND;
+ const OR;
+ const BAND;
+ const BOR;
+ const XOR;
+ const ADD;
+ const SUB;
+ const MUL;
+ const EQ;
+ const NE;
+ const LT;
+ const GT;
+ const LE;
+ const GE;
+ ]
+
+(* int32 generator as the default machdep is 32 bit.
+ Moreover, we only generate positive integers here, as negative ones are
+ supposed to be given by unary -
+*)
+let gen_constant =
+ choose [
+ map [ range 4 ]
+ (fun i -> mk_exp (CONSTANT (CONST_INT (string_of_int i))));
+ map [ float ]
+ (fun f ->
+ let up = 4.0 in
+ let f = if f < 0.0 then 0. else f in
+ let f = if f > up then up else f in
+ mk_exp (CONSTANT (CONST_FLOAT (string_of_float f))))
+ ]
+
+let mk_cast t e = mk_exp (CAST (([SpecType t],JUSTBASE), SINGLE_INIT e))
+
+let protected_cast t e =
+ let max = mk_exp (CONSTANT(CONST_INT("255"))) in
+ let min =
+ match t with
+ | Tunsigned -> mk_exp(CONSTANT(CONST_INT("0")))
+ | _ -> mk_exp (UNARY(MINUS,max))
+ in
+ let maxr = mk_cast t max in
+ let minr = mk_cast t min in
+ mk_exp(
+ QUESTION(
+ mk_exp(BINARY(GE,e,min)),
+ mk_exp(QUESTION(mk_exp(BINARY(LE,e,max)),e,maxr)),
+ minr))
+
+let force_int typ e =
+ let e = protected_cast typ e in
+ mk_exp (CAST (([SpecType typ],JUSTBASE), SINGLE_INIT e))
+
+let gen_expr =
+ fix
+ (fun gen_expr ->
+ choose [
+ gen_constant;
+ map [ gen_int_type; gen_unary; gen_expr]
+ (fun t u e ->
+ let e = if needs_int_unary u then force_int t e else e in
+ mk_exp (UNARY(u,e)));
+ map [ gen_int_type; gen_binary; gen_expr; gen_expr ]
+ (fun t b e1 e2 ->
+ let e1,e2 =
+ if needs_int_binary b then
+ force_int t e1, force_int t e2
+ else e1,e2
+ in
+ mk_exp (BINARY (b,e1,e2)));
+ map [ gen_expr; gen_expr; gen_expr ]
+ (fun c et ef -> mk_exp (QUESTION (c,et,ef)));
+ map [ gen_type; gen_expr ]
+ (fun t e ->
+ let e = protected_cast t e in
+ mk_exp (CAST (([SpecType t],JUSTBASE), SINGLE_INIT e)));
+ ])
+
+let gen_cabs typ expr =
+ let expr = protected_cast typ expr in
+ (Datatype.Filepath.dummy,
+ [ false,
+ DECDEF(
+ None,
+ ([SpecType typ],
+ [("a",
+ ARRAY(JUSTBASE,[],{ expr_loc = loc; expr_node = NOTHING}),[],loc),
+ COMPOUND_INIT [NEXT_INIT, SINGLE_INIT expr]]),
+ loc);
+ false,
+ DECDEF(None,([SpecType Tint],[("result", JUSTBASE,[],loc),NO_INIT]),loc);
+ false,
+ FUNDEF(
+ None,([SpecType Tvoid],("f", PROTO(JUSTBASE,[],[],false),[],loc)),
+ { blabels = [];
+ battrs = [];
+ bstmts = [
+ { stmt_ghost = false;
+ stmt_node =
+ DEFINITION(
+ DECDEF(
+ None,
+ ([SpecType typ], [("x",JUSTBASE,[],loc),SINGLE_INIT expr]),
+ loc))};
+ { stmt_ghost = false;
+ stmt_node =
+ COMPUTATION(
+ mk_exp(
+ BINARY(
+ ASSIGN,
+ mk_exp (VARIABLE "result"),
+ mk_exp (
+ BINARY(
+ EQ,
+ mk_exp (VARIABLE "x"),
+ mk_exp(
+ INDEX(
+ mk_exp (VARIABLE "a"),
+ mk_exp (CONSTANT (CONST_INT "0")))))))), loc)}
+ ]
+ },
+ loc,loc)])
+
+let () = Kernel.AutoLoadPlugins.off()
+
+let () = Project.set_current (Project.create "my_project")
+
+let () = Dynamic.set_module_load_path [ "lib/plugins" ]
+
+let () = Dynamic.load_module "frama-c-eva"
+
+let on_from_name s f = Project.on (Project.from_unique_name s) f ()
+
+let () =
+ Cmdline.(
+ parse_and_boot
+ ~on_from_name:{ on_from_name }
+ ~get_toplevel:(fun () f -> f ())
+ ~play_analysis:(fun _ -> ()))
+
+let run typ expr =
+ Project.clear ();
+ let loc = Cil_datatype.Location.unknown in
+ let cabs = gen_cabs typ expr in
+ Kernel.SignedOverflow.off ();
+ Kernel.SignedDowncast.off ();
+ Kernel.UnsignedOverflow.off ();
+ Kernel.UnsignedDowncast.off ();
+ Kernel.add_debug_keys Kernel.dkey_constfold;
+ (* otherwise, we must load scope in addition to eva. *)
+ Dynamic.Parameter.Bool.off "-eva-remove-redundant-alarms" ();
+ Errorloc.clear_errors ();
+ Format.printf "Cabs is@\n%a@." Cprint.printFile cabs;
+ let cil =
+ try Cabs2cil.convFile cabs
+ with exn ->
+ failf "Failed to typecheck cabs: %s@\n%a@."
+ (Printexc.to_string exn)
+ Cprint.printFile cabs
+ in
+ if Errorloc.had_errors () then begin
+ failf "Failed to typecheck cabs (had errors)@\n%a@."
+ Cprint.printFile cabs
+ end;
+ File.prepare_cil_file cil;
+ Kernel.MainFunction.set "f";
+ !Db.Value.compute ();
+ let kf = Globals.Functions.find_by_name "f" in
+ let r = Globals.Vars.find_from_astinfo "result" Cil_types.VGlobal in
+ let ret = Kernel_function.find_return kf in
+ let state = Db.Value.get_stmt_state ret in
+ let v1 =
+ !Db.Value.eval_expr
+ ~with_alarms:CilE.warn_none_mode state (Cil.evar ~loc r)
+ in
+ let itv =
+ try Cvalue.V.project_ival v1
+ with exn ->
+ failf "Eva analysis did not reduce to a constant: %s@\n%t@."
+ (Printexc.to_string exn)
+ (fun fmt -> File.pretty_ast ~fmt ())
+ in
+ if not (Ival.is_one itv) then begin
+ failf "const fold did not reduce to identical value:@\n%t@."
+ (fun fmt -> File.pretty_ast ~fmt ())
+ end
+
+let () = add_test ~name:"constfold" [gen_type; gen_expr] run
diff --git a/tests/syntax/compile_constant.c b/tests/syntax/compile_constant.c
new file mode 100644
index 0000000000000000000000000000000000000000..7dcef8ed9d028f7e170e9f4b87d7a531d73d0aa4
--- /dev/null
+++ b/tests/syntax/compile_constant.c
@@ -0,0 +1,18 @@
+#define M0(x) (x)*(x)<4.0?0.0:1.0
+char pixels[] = {M0(0.0), M0(1), M0(2.0f)};
+
+/* tests below should evaluate to 2. */
+
+char test_neg = { (-0.) ? 1. : 2. };
+
+char test_ge = { ((-1.) >= 0.) ? 1. : 2. };
+
+char test_cast[] = { 1 >= (0?1U:(-1)) ? 1. : 2.,
+ ((double)1) >= (0?1U:(-1)) ? 1. : 2. };
+
+double a = 2 >= 5 ? 5 ? (long)0 || 0 ? 0. >= 0 ?: 0 : 2 : 5 : 0;
+
+extern int f(void);
+
+/* no call should be evaluated. */
+char no_call[] = { 1 ? 1 : f(), 0?f():2 };
diff --git a/tests/syntax/oracle/compile_constant.res.oracle b/tests/syntax/oracle/compile_constant.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b979c0f88dc4faab3ab08f39b414e081ed5ac5be
--- /dev/null
+++ b/tests/syntax/oracle/compile_constant.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing tests/syntax/compile_constant.c (with preprocessing)
+/* Generated by Frama-C */
+char pixels[3] = {(char)0.0, (char)0.0, (char)1.0};
+char test_neg = (char)2.;
+char test_ge = (char)2.;
+char test_cast[2] = {(char)2., (char)2.};
+double a = (double)0;
+char no_call[2] = {(char)1, (char)2};
+