diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index a80ffdbd855f502b9ced959aad0a6fcf443fe4db..08754985e86dd7e348461aabe1223347e0532e04 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -345,6 +345,7 @@ let extended_interv_of_typ ty = match interv_of_typ ty with
Ival (Ival.inject_range l u);
| Rational | Real | Nan | Float (_,_) as i
-> i
+
(*
(* Compute the interval of the extended quantifier \sum, \product and \numof.
[lambda] is the interval of the lambda term, [i] (resp. [j]) is the interval
@@ -392,13 +393,12 @@ let interv_of_extended_quantifier lambda lb up name =
*)
(* Compute the interval of the extended quantifier \sum, \product and \numof.
- [lbd_ival] is the interval of the lambda term, [k_ival] is the interval of the
- quantifier and [name] is the identifier of the extended quantifier (\sum,
- \product or \numof). The returned ival is the interval of the extended
- quantifier *)
+ [lbd_ival] is the interval of the lambda term, [k_ival] is the interval of
+ the quantifier and [name] is the identifier of the extended quantifier (\sum
+ or \product). The returned ival is the interval of the extended quantifier *)
let interv_of_extended_quantifier lambda i j name =
match lambda, i, j with
- | Ival lbd_ival, Ival i_ival, Ival j_ival->
+ | Ival lbd_ival, Ival i_ival, Ival j_ival ->
(try
let min_lambda, max_lambda = Ival.min_and_max lbd_ival in
let i_inf, i_sup = Ival.min_and_max i_ival in
@@ -426,30 +426,40 @@ let interv_of_extended_quantifier lambda i j name =
let compute_bound_product =
(try
match min_lambda, max_lambda, i_inf, i_sup, j_inf, j_sup with
- | _, _, Some i_inf, _, _, Some j_sup when (Z.compare i_inf j_sup)=1 ->
+ | _, _, Some i_inf, _, _, Some j_sup
+ when (Z.compare i_inf j_sup) = 1 ->
(Ival.inject_range (Some Z.one) (Some Z.one))
| Some lambda_inf, Some lambda_sup, Some i_inf, _, _, Some j_sup
- when (Z.compare i_inf j_sup)<=0 && (Z.compare lambda_inf Z.zero)<=0 &&
- (Z.compare Z.zero lambda_sup)<=0->
+ when (Z.compare i_inf j_sup) <= 0 &&
+ (Z.compare lambda_inf Z.zero) <= 0 &&
+ (Z.compare Z.zero lambda_sup) <= 0 ->
let exponent = Z.to_int (Z.sub j_sup i_inf) in
let bound =
- if (Z.compare lambda_sup (Z.neg lambda_inf))<=0 then
+ if (Z.compare lambda_sup (Z.neg lambda_inf)) <= 0 then
(Z.pow (Z.neg lambda_inf) exponent)
else
(Z.pow lambda_sup exponent)
in (Ival.inject_range (Some (Z.neg bound)) (Some bound))
- | Some lambda_inf, Some lambda_sup, Some i_inf, Some i_sup, Some j_inf, Some j_sup when (Z.compare i_inf j_sup)<=0 && (Z.compare lambda_inf Z.zero)=1 && (Z.compare lambda_inf lambda_sup)<=0->
+ | Some lambda_inf, Some lambda_sup, Some i_inf, Some i_sup,
+ Some j_inf, Some j_sup
+ when (Z.compare i_inf j_sup) <= 0 &&
+ (Z.compare lambda_inf Z.zero) = 1 &&
+ (Z.compare lambda_inf lambda_sup) <= 0 ->
let exponent= Z.to_int (Z.sub j_sup i_inf) in
let bound_inf =
- if (Z.compare i_sup j_inf<=0) then
+ if (Z.compare i_sup j_inf <= 0) then
Z.pow lambda_inf (Z.to_int (Z.sub j_inf i_sup))
else
Z.one
- in Ival.inject_range (Some bound_inf) (Some (Z.pow lambda_sup exponent))
+ in
+ Ival.inject_range
+ (Some bound_inf) (Some (Z.pow lambda_sup exponent))
| Some lambda_inf, Some lambda_sup, Some i_inf, _, _, Some j_sup
- when (Z.compare i_inf j_sup)<=0 && (Z.compare lambda_sup Z.zero)=(-1)
- && (Z.compare lambda_inf lambda_sup)<=0->
- let bound = Z.pow (Z.neg lambda_inf) (Z.to_int (Z.sub j_sup i_inf)) in
+ when (Z.compare i_inf j_sup) <= 0 &&
+ (Z.compare lambda_sup Z.zero)=(-1) &&
+ (Z.compare lambda_inf lambda_sup) <= 0 ->
+ let bound = Z.pow (Z.neg lambda_inf) (Z.to_int (Z.sub j_sup i_inf))
+ in
Ival.inject_range (Some (Z.neg bound)) (Some bound)
| _ -> Ival.inject_range None None
with Z.Overflow ->
@@ -460,7 +470,7 @@ let interv_of_extended_quantifier lambda i j name =
(compute_bound_sum min_lambda true)
(compute_bound_sum max_lambda false))
| "\\product" -> Ival compute_bound_product
- | _ -> assert false (*unreachable branch*)
+ | _ -> assert false (* unreachable branch *)
with Abstract_interp.Error_Bottom ->
bottom)
| _ -> Error.not_yet "extended quantifiers with non-integer parameters"
@@ -764,7 +774,7 @@ let rec infer t =
in
fixpoint bottom
| LBnone when li.l_var_info.lv_name = "\\sum" ||
- li.l_var_info.lv_name = "\\product"->
+ li.l_var_info.lv_name = "\\product" ->
(match args with
| [ t1; t2; {term_node = Tlambda([ k ], _)} as lambda ] ->
let t1_ival = infer t1 in
@@ -784,11 +794,10 @@ let rec infer t =
the code of the lambda term *)
interv_of_extended_quantifier
lambda_ival t1_ival t2_ival li.l_var_info
- | _ -> Options.fatal "unexpected input for an extended quantifier %a"
- Printer.pp_logic_var li.l_var_info)
+ | _ -> Error.not_yet "extended quantifiers without lambda term")
| LBnone when li.l_var_info.lv_name = "\\numof" ->
(match args with
- | [ t1; t2; {term_node = Tlambda([ k ], predicate)}] ->
+ | [ t1; t2; {term_node = Tlambda([ k ], predicate)} ] ->
let logic_info = Cil_const.make_logic_info "\\sum" in
logic_info.l_type <- li.l_type;
logic_info.l_tparams <- li.l_tparams;
@@ -796,10 +805,18 @@ let rec infer t =
logic_info.l_profile <- li.l_profile;
logic_info.l_body <- li.l_body;
let numof_as_sum =
- (Logic_const.term (Tapp(logic_info, lst, [t1;t2;Logic_const.term (Tlambda([k],Logic_const.term (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger)) Linteger])) Linteger)
+ let conditional_term =
+ Logic_const.term
+ (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
+ in
+ let lambda_term =
+ Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
+ in
+ (Logic_const.term
+ (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
in infer numof_as_sum
- | _ -> Options.fatal "unexpected input for an extended quantifier \\numof"
- )
+ | _ ->
+ Options.fatal "unexpected input for an extended quantifier \\numof")
| LBnone
| LBreads _ ->
(match li.l_type with
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index bf3370f975d3f58db37bd760fdc0967d6cee953c..db78316a1b6e841c86f00c68957261cd18d0b414 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -605,7 +605,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
end
| LBnone ->
(match args with
- | [ t1; t2; lambda ] ->
+ | [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ] ->
let anonymous =
Logic_const.term (TBinOp(PlusA, t2, Cil.lone ())) Linteger
in
@@ -623,13 +623,12 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
ignore (type_term ~use_gmp_opt:true ?ctx ~lenv lambda);
dup ty
| [ ] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ ->
- Error.not_yet "logic functions or predicates with no definition \
- nor reads clause"
(* TODO : improve error message to distinguish error messages
corresponding to unsupported primitives and wrong application
of supported primitive
(one is a fatal and the other is a not_yet) *)
- )
+ Error.not_yet "logic functions or predicates with no definition \
+ nor reads clause")
| LBreads _ ->
Error.not_yet "logic functions or predicates performing read accesses"
| LBinductive _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 012250eabff6a3ea36d5db01e158bd7a7653d7ac..bebbab025e8e29e7e5b85e8e399444b20827920c 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -193,7 +193,7 @@ and tlval_to_lval kf env (host, offset) =
(* Compute the expression which corresponds to an extended_quantifier term in a
given environment. [t] is the extended_quantifier term, [t_min] the lower bound,
[t max] the upper bound, [lambda] the lambda term and [name] is the identifier of
- the extended quantifier ("\sum", "\product" or "\numof") *)
+ the extended quantifier ("\sum" or "\product") *)
and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
match lambda.term_node with
| Tlambda([ k ] ,lt) when name.lv_name="\\product" || name.lv_name="\\sum" ->
@@ -208,7 +208,9 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
let init_k_stmt = Gmp.init_set ~loc (Cil.var k_as_varinfo) k_as_exp e_min in
(*variable initialization*)
(*one = 1;*)
- let _, one_as_exp, env = create_and_init_var ~loc kf ty_k "one" (Cil.one ~loc) env in
+ let _, one_as_exp, env =
+ create_and_init_var ~loc kf ty_k "one" (Cil.one ~loc) env
+ in
(*cond = 0;*)
let cond_as_varinfo, cond_as_exp, env =
create_and_init_var ~loc kf Cil.intType "cond" (Cil.zero ~loc) env
@@ -238,7 +240,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
affect_binop ~loc cond_as_varinfo None Gt ty_k k_as_exp e_max
in
(*acc = acc op lbda; or __gmpz_op(acc,acc,lbda);*)
- let acc_plus_lbd_stmt = if name.lv_name="\\sum" then
+ let acc_plus_lbd_stmt = if name.lv_name = "\\sum" then
affect_binop
~loc acc_as_varinfo (Some acc_as_exp) PlusA ty_op acc_as_exp lbd_as_exp
else
@@ -279,8 +281,8 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
let env = Env.add_stmt env kf (Smart_stmt.block_stmt final_stmt) in
let adata, env = Assert.register_term ~loc kf env t acc_as_exp adata in
acc_as_exp, adata, env, Typed_number.C_number, ""
- | _ -> Options.fatal "%a is not a valid extended quantifier"
- Printer.pp_logic_var name
+ | _ ->
+ assert false (* unreachable branch *)
and context_insensitive_term_to_exp ~adata kf env t =
let loc = t.term_loc in
@@ -729,24 +731,31 @@ and context_insensitive_term_to_exp ~adata kf env t =
let e = Cil.mkAddrOrStartOf ~loc lv in
let adata, env = Assert.register_term ~loc kf env t e adata in
e, adata, env, Typed_number.C_number, "startof"
- | Tapp(li, _, [ t1; t2; lambda ]) when li.l_body = LBnone && (li.l_var_info.lv_name="\\sum" || li.l_var_info.lv_name="\\product")->
+ | Tapp(li, _, [ t1; t2; {term_node = Tlambda([ _ ], _)} as lambda ])
+ when li.l_body = LBnone && (li.l_var_info.lv_name = "\\sum" ||
+ li.l_var_info.lv_name = "\\product")->
extended_quantifier_to_exp ~adata ~loc kf env t t1 t2 lambda li.l_var_info
- | Tapp(li, lst, [ t1; t2; lambda ]) when li.l_body = LBnone && li.l_var_info.lv_name="\\numof" ->
- (match lambda with
- | {term_node = Tlambda([ k ], predicate)} ->
- let logic_info = Cil_const.make_logic_info "\\sum" in
- logic_info.l_type <- li.l_type;
- logic_info.l_tparams <- li.l_tparams;
- logic_info.l_labels <- li.l_labels;
- logic_info.l_profile <- li.l_profile;
- logic_info.l_body <- li.l_body;
- let anonymous =
- (Logic_const.term (Tapp(logic_info, lst, [t1;t2;Logic_const.term (Tlambda([k],Logic_const.term (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger)) Linteger])) Linteger)
- in
- Typing.type_term ~use_gmp_opt:false anonymous;
- context_insensitive_term_to_exp ~adata kf env anonymous
- | _ -> Options.fatal "unexpected input for an extended quantifier \\numof"
- )
+ | Tapp(li, lst, [ t1; t2; {term_node = Tlambda([ k ], predicate)}])
+ when li.l_body = LBnone && li.l_var_info.lv_name = "\\numof" ->
+ let logic_info = Cil_const.make_logic_info "\\sum" in
+ logic_info.l_type <- li.l_type;
+ logic_info.l_tparams <- li.l_tparams;
+ logic_info.l_labels <- li.l_labels;
+ logic_info.l_profile <- li.l_profile;
+ logic_info.l_body <- li.l_body;
+ let numof_as_sum =
+ let conditional_term =
+ Logic_const.term
+ (Tif(predicate, Cil.lone (), Cil.lzero ())) Linteger
+ in
+ let lambda_term =
+ Logic_const.term (Tlambda([ k ], conditional_term)) Linteger
+ in
+ (Logic_const.term
+ (Tapp(logic_info, lst, [ t1; t2; lambda_term ])) Linteger)
+ in
+ Typing.type_term ~use_gmp_opt:true numof_as_sum;
+ context_insensitive_term_to_exp ~adata kf env numof_as_sum
| Tapp(_, [], _) ->
let e, adata, env = Logic_functions.tapp_to_exp ~adata kf env t in
let adata, env = Assert.register_term ~loc kf env t e adata in
diff --git a/src/plugins/e-acsl/tests/arith/oracle_dev/sum.e-acsl.err.log b/src/plugins/e-acsl/tests/arith/oracle_dev/extended_quantifiers.e-acsl.err.log
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle_dev/sum.e-acsl.err.log
rename to src/plugins/e-acsl/tests/arith/oracle_dev/extended_quantifiers.e-acsl.err.log
diff --git a/src/plugins/value/values/numerors/numerors_float.ml b/src/plugins/value/values/numerors/numerors_float.ml
index b3816466d613ffa59d20e3cb82ac9b2440565814..e314cef6c12a8f52ef51041b6da7e96c6cc96f85 100644
--- a/src/plugins/value/values/numerors/numerors_float.ml
+++ b/src/plugins/value/values/numerors/numerors_float.ml
@@ -75,8 +75,8 @@ let change_prec ?(rnd = Mpfr.Near) prec (p, x) =
calling the unary function f on an input of type t *)
let unary_mpfrf f =
fun ?(rnd = Rounding.Near) ?(prec = P.Real) x ->
- prec >>- fun () ->
- f (change_prec prec x) (rounding rnd)
+ prec >>- fun () ->
+ f (change_prec prec x) (rounding rnd)
(* Returns a function which apply the rounding of its optionnal parameter rnd
and change the precision according to its optionnal parameter prec before