diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index e413080ea770e83d7567e0495d846c6e64ffaa17..958147981d2e6ef21740a6be8a9ac9d4f0eb7f3f 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -443,12 +443,112 @@ end
end
+(* Imperative environment to perform fixpoint algorithm for recursive
+ functions *)
+module LF_env : sig
+ val find : logic_info -> Profile.t -> ival
+
+ val clear : unit -> unit
+
+ val interv_of_typ_containing_interv : ival -> ival
+
+ val is_rec : logic_info -> bool
+
+ val fixpoint :
+ infer : (
+ ?force_infer:bool ->
+ logic_env: Logic_environment.t ->
+ term ->
+ ival Error.result) ->
+ logic_info ->
+ Profile.t ->
+ term ->
+ ival ->
+ ival
+
+end
+= struct
+
+ module LFProf =
+ Datatype.Pair_with_collections (Cil_datatype.Logic_info) (Profile)
+ (struct
+ let module_name = "E_ACSL.Interval.LF_env.LFProf"
+ end)
+
+ let tbl = LFProf.Hashtbl.create 97
+
+ let clear () = LFProf.Hashtbl.clear tbl
+
+ let find li profile = LFProf.Hashtbl.find tbl (li,profile)
+
+ exception Recursive
+
+ let contain li = object
+ inherit Visitor.frama_c_inplace
+
+ method !vpredicate p =
+ match p.pred_content with
+ | Papp (li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
+ raise Recursive;
+ | _ -> Cil.DoChildren
+
+ method !vterm t =
+ match t.term_node with
+ | Tapp(li_app,_,_) when Cil_datatype.Logic_info.equal li li_app ->
+ raise Recursive
+ | _ -> Cil.DoChildren
+
+ end
+
+ let is_rec li =
+ match li.l_body with
+ | LBpred p ->
+ (try ignore (Visitor.visitFramacPredicate (contain li) p); false
+ with Recursive -> true)
+ | LBterm t ->
+ (try ignore (Visitor.visitFramacTerm (contain li) t); false
+ with Recursive -> true)
+ | LBreads _ | LBnone |LBinductive _ -> false
+
+ let interv_of_typ_containing_interv = function
+ | Float _ | Rational | Real | Nan as x ->
+ x
+ | Ival i ->
+ try
+ let kind = ikind_of_ival i in
+ interv_of_typ (TInt(kind, []))
+ with Cil.Not_representable ->
+ top_ival
+
+ let rec fixpoint ~(infer : ?force_infer:bool ->
+ logic_env:Logic_environment.t ->
+ term ->
+ ival Error.result)
+ li args_ival t' ival =
+ LFProf.Hashtbl.replace tbl (li,args_ival) ival;
+ let get_res = Error.map (fun x -> x) in
+ let logic_env = Logic_environment.create li.l_profile args_ival in
+ let inferred_ival = get_res (infer ~force_infer:true ~logic_env t') in
+ if is_included inferred_ival ival
+ then
+ ival
+ else
+ fixpoint ~infer li args_ival t' inferred_ival
+
+end
+
(* Memoization module which retrieves the computed info of some terms. If the
info is already computed for a term, it is never recomputed *)
module Memo: sig
val memo:
- profile:Profile.t -> (term -> ival) -> term -> ival Error.or_error
- val get: profile:Profile.t -> term -> ival Error.or_error
+ force_infer:bool ->
+ profile:Profile.t ->
+ (term -> ival) ->
+ term ->
+ ival Error.result
+ val get: profile:Profile.t -> term -> ival Error.result
+ val get_widened_profile: Profile.t -> term -> Profile.t
+ val add_widened_profile: Profile.t -> term -> Profile.t -> unit
val clear: unit -> unit
end = struct
(* The comparison over terms is the physical equality. It cannot be the
@@ -478,6 +578,21 @@ end = struct
let dep_tbl : ival Error.result Id_term_in_profile.Hashtbl.t
= Id_term_in_profile.Hashtbl.create 97
+ let widened_profile_tbl : Profile.t Id_term_in_profile.Hashtbl.t
+ = Id_term_in_profile.Hashtbl.create 97
+
+ let get_widened_profile profile t =
+ Id_term_in_profile.Hashtbl.find_def
+ widened_profile_tbl
+ (t,profile)
+ profile
+
+ let add_widened_profile profile t args_ival =
+ Id_term_in_profile.Hashtbl.add
+ widened_profile_tbl
+ (t,profile)
+ args_ival
+
let get_dep profile t =
try Id_term_in_profile.Hashtbl.find dep_tbl (t,profile)
with Not_found -> Error.not_memoized ()
@@ -491,32 +606,49 @@ end = struct
| [] -> get_nondep t
| _::_ -> get_dep profile t
- let memo_nondep f t =
- try Misc.Id_term.Hashtbl.find tbl t
- with Not_found ->
+ let memo_nondep ~force_infer f t =
+ if force_infer then
let x =
try
- Error.Res (f t);
- with Error.Not_yet _ | Error.Typing_error _ as exn -> Error.Err exn
+ Result.Ok (f t);
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
in
- Misc.Id_term.Hashtbl.add tbl t x;
+ Misc.Id_term.Hashtbl.replace tbl t x;
x
+ else
+ try Misc.Id_term.Hashtbl.find tbl t
+ with Not_found ->
+ let x =
+ try
+ Result.Ok (f t);
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
+ in
+ Misc.Id_term.Hashtbl.add tbl t x;
+ x
- let memo_dep f t profile =
- try
- Id_term_in_profile.Hashtbl.find dep_tbl (t, profile)
- with Not_found ->
+ let memo_dep ~force_infer f t profile =
+ if force_infer then
let x =
- try Error.Res (f t)
- with Error.Not_yet _ | Error.Typing_error _ as exn -> Error.Err exn
+ try Result.Ok (f t)
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
in
- Id_term_in_profile.Hashtbl.add dep_tbl (t, profile) x;
+ Id_term_in_profile.Hashtbl.replace dep_tbl (t, profile) x;
x
+ else
+ try
+ Id_term_in_profile.Hashtbl.find dep_tbl (t, profile)
+ with Not_found ->
+ let x =
+ try Result.Ok (f t)
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Result.Error exn
+ in
+ Id_term_in_profile.Hashtbl.add dep_tbl (t, profile) x;
+ x
- let memo ~profile f t =
+ let memo ~force_infer ~profile f t =
match profile with
- | [] -> memo_nondep f t
- | _::_ -> memo_dep f t profile
+ | [] -> memo_nondep ~force_infer f t
+ | _::_ -> memo_dep ~force_infer f t profile
let clear () =
Options.feedback ~level:4 "clearing the typing tables";
@@ -636,10 +768,12 @@ let infer_sum_product oper lambda min max = match lambda, min, max with
| Z.Overflow (* if the exponent of \product is too high *) -> top_ival)
| _ -> Error.not_yet "extended quantifiers with non-integer parameters"
-let rec infer ~logic_env t =
+let rec infer ?(force_infer=false) ~logic_env t =
let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in
let get_res = Error.map (fun x -> x) in
let t = Logic_normalizer.get_term t in
+ let infer_full = infer
+ and infer = infer ~force_infer in
let compute t =
match t.term_node with
| TConst (Integer (n, _)) -> singleton n
@@ -777,14 +911,29 @@ let rec infer ~logic_env t =
ignore (infer_predicate ~logic_env p);
Ival Ival.zero_or_one
| LBterm t' ->
- (* No fixpoint for now *)
- let args_ival =
- List.map
- (fun arg -> get_res (infer ~logic_env arg))
- args
- in
- let logic_env = Logic_environment.create li.l_profile args_ival in
- get_res (infer ~logic_env t')
+ if LF_env.is_rec li
+ then
+ let profile,args_ival =
+ let profile =
+ List.map
+ (fun arg -> (get_res (infer ~logic_env arg)))
+ args
+ in
+ profile, (List.map LF_env.interv_of_typ_containing_interv profile)
+ in
+ Memo.add_widened_profile profile t' args_ival;
+ try let res = LF_env.find li args_ival in
+ res;
+ with Not_found ->
+ LF_env.fixpoint ~infer:infer_full li args_ival t' (Ival Ival.bottom)
+ else
+ let args_ival =
+ List.map
+ (fun arg -> get_res (infer ~logic_env arg))
+ args
+ in
+ let logic_env = Logic_environment.create li.l_profile args_ival in
+ get_res (infer ~logic_env t')
| LBnone when li.l_var_info.lv_name = "\\sum" ||
li.l_var_info.lv_name = "\\product" ->
(match args with
@@ -864,7 +1013,11 @@ let rec infer ~logic_env t =
| Ttype _
| Tempty_set ->
Nan
- in Memo.memo ~profile:(Logic_environment.get_profile logic_env) compute t
+ in Memo.memo
+ ~force_infer
+ ~profile:(Logic_environment.get_profile logic_env)
+ compute
+ t
and infer_term_lval ~logic_env (host, offset as tlv) =
match offset with
@@ -1097,6 +1250,12 @@ let get_p ~profile t =
let get ~logic_env =
get_p ~profile:(Logic_environment.get_profile logic_env)
+let get_widened_profile = Memo.get_widened_profile
+
+let clear () =
+ Memo.clear();
+ LF_env.clear()
+
type profile = Profile.t
(*
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index 7e91f22e4b6834fa36555a10d87bcf0228b2eb82..e48971fa400c3ddb8d77aca07a7d83f7ca4aa496 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -143,6 +143,10 @@ val preprocess_code_annot :
val preprocess_term :
logic_env:Logic_environment.t -> Cil_types.term -> unit
+val get_widened_profile : profile -> Cil_types.term -> profile
+
+val clear : unit -> unit
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 3bdd79d845b6973fbf97efd4643a65dc3af471f9..532ea8c1b6663827c161464b21ede47c38a671a1 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -616,6 +616,7 @@ let rec type_term
~profile x))
args;
let new_profile = List.map (Interval.get_p ~profile) args in
+ let new_profile = Interval.get_widened_profile new_profile t_body in
let gmp,ctx_body = match li.l_type with
| Some (Ctype typ) ->
false, Some (number_ty_of_typ ~post:false typ)
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index ea27f3bbfce651d1874e7142d3d0a5ea7a2cb26c..2ab49544212baaa8c2f1889ba3f893bdfea3127c 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -495,6 +495,11 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs =
let gen_fname =
Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
in
+ let params_ival = match li.l_body with
+ | LBterm t -> Interval.get_widened_profile params_ival t
+ | LBpred _ -> params_ival
+ | _ -> assert false
+ in
let vi, e, env =
function_to_exp ~loc ?tapp gen_fname env kf li params_ty params_ival args
in
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index b38e3178766ffb17f3fb1c472b78e599e36e0dbb..fb1832ca1932365758dee4c7644baaca1cd4882a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -11,38 +11,42 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
/*@ logic integer f1(integer n) = n <= 0? 0: f1(n - 1) + n;
*/
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n);
-
void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n);
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n);
+
void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
/*@
logic integer f2(integer n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
-int __gen_e_acsl_f2(int n);
-
int __gen_e_acsl_f2_2(long n);
+int __gen_e_acsl_f2(int n);
+
int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n);
/*@ logic integer g(integer n) = 0;
*/
+int __gen_e_acsl_g_3(long n);
+
+int __gen_e_acsl_g_9(__e_acsl_mpz_struct * n);
+
int __gen_e_acsl_g(int n);
-int __gen_e_acsl_g_3(long n);
+int __gen_e_acsl_g_11(long n);
int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n);
/*@ logic integer f3(integer n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
*/
-int __gen_e_acsl_f3(int n);
-
int __gen_e_acsl_f3_2(long n);
+int __gen_e_acsl_f3(int n);
+
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n);
/*@
@@ -50,19 +54,19 @@ logic integer f4(integer n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-unsigned long __gen_e_acsl_f4(int n);
-
unsigned long __gen_e_acsl_f4_2(long n);
+unsigned long __gen_e_acsl_f4(int n);
+
unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n);
/*@ logic integer f5(integer n) = n >= 0? 0: f5(n + 1) + n;
*/
-void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n);
-
void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n);
+void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n);
+
void __gen_e_acsl_f5_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
int main(void)
@@ -248,40 +252,6 @@ int main(void)
return __retres;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_if_3;
- if (n <= 0) {
- __e_acsl_mpz_t __gen_e_acsl_;
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_clear(__gen_e_acsl_);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_f1_7;
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __gen_e_acsl_f1_2(& __gen_e_acsl_f1_7,n - 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_clear(__gen_e_acsl_f1_7);
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl_add_3);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
- __gmpz_clear(__gen_e_acsl_if_3);
- return;
-}
-
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
@@ -330,6 +300,40 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ if (n <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f1_7;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gen_e_acsl_f1_2(& __gen_e_acsl_f1_7,n - 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_f1_7);
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
@@ -381,51 +385,6 @@ void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
return;
}
-/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_f2(int n)
-{
- int __gen_e_acsl_if_6;
- if (n < 0) __gen_e_acsl_if_6 = 1;
- else {
- int __gen_e_acsl_f2_15;
- int __gen_e_acsl_f2_17;
- int __gen_e_acsl_f2_19;
- __gen_e_acsl_f2_15 = __gen_e_acsl_f2_2(n - 1L);
- __gen_e_acsl_f2_17 = __gen_e_acsl_f2_2(n - 2L);
- __gen_e_acsl_f2_19 = __gen_e_acsl_f2_2(n - 3L);
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
- {.values = (void *)0};
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
- "__gen_e_acsl_f2_19",0,__gen_e_acsl_f2_19);
- __gen_e_acsl_assert_data_7.blocking = 1;
- __gen_e_acsl_assert_data_7.kind = "RTE";
- __gen_e_acsl_assert_data_7.pred_txt = "__gen_e_acsl_f2_19 != 0";
- __gen_e_acsl_assert_data_7.file = "functions_rec.c";
- __gen_e_acsl_assert_data_7.fct = "f2";
- __gen_e_acsl_assert_data_7.line = 13;
- __gen_e_acsl_assert_data_7.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_f2_19 != 0,& __gen_e_acsl_assert_data_7);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_19 != 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 <= __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 <= 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19
- <= 2147483647;
- */
- __gen_e_acsl_if_6 = (__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19;
- }
- return __gen_e_acsl_if_6;
-}
-
/*@ assigns \result;
assigns \result \from n; */
int __gen_e_acsl_f2_2(long n)
@@ -513,6 +472,51 @@ int __gen_e_acsl_f2_2(long n)
return __gen_e_acsl_if_5;
}
+/*@ assigns \result;
+ assigns \result \from n; */
+int __gen_e_acsl_f2(int n)
+{
+ int __gen_e_acsl_if_6;
+ if (n < 0) __gen_e_acsl_if_6 = 1;
+ else {
+ int __gen_e_acsl_f2_15;
+ int __gen_e_acsl_f2_17;
+ int __gen_e_acsl_f2_19;
+ __gen_e_acsl_f2_15 = __gen_e_acsl_f2_2(n - 1L);
+ __gen_e_acsl_f2_17 = __gen_e_acsl_f2_2(n - 2L);
+ __gen_e_acsl_f2_19 = __gen_e_acsl_f2_2(n - 3L);
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
+ {.values = (void *)0};
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_7,
+ "__gen_e_acsl_f2_19",0,__gen_e_acsl_f2_19);
+ __gen_e_acsl_assert_data_7.blocking = 1;
+ __gen_e_acsl_assert_data_7.kind = "RTE";
+ __gen_e_acsl_assert_data_7.pred_txt = "__gen_e_acsl_f2_19 != 0";
+ __gen_e_acsl_assert_data_7.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_7.fct = "f2";
+ __gen_e_acsl_assert_data_7.line = 13;
+ __gen_e_acsl_assert_data_7.name = "division_by_zero";
+ __e_acsl_assert(__gen_e_acsl_f2_19 != 0,& __gen_e_acsl_assert_data_7);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
+ /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_19 != 0; */
+ /*@ assert
+ Eva: signed_overflow:
+ -2147483648 <= __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 <= 2147483647;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19
+ <= 2147483647;
+ */
+ __gen_e_acsl_if_6 = (__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19;
+ }
+ return __gen_e_acsl_if_6;
+}
+
/*@ assigns \result;
assigns \result \from *((__e_acsl_mpz_struct *)n); */
int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
@@ -602,23 +606,23 @@ int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n)
/*@ assigns \result;
assigns \result \from n; */
-int __gen_e_acsl_g(int n)
+int __gen_e_acsl_g_3(long n)
{
int __retres = 0;
return __retres;
}
/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_g_3(long n)
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
+int __gen_e_acsl_g_9(__e_acsl_mpz_struct * n)
{
int __retres = 0;
return __retres;
}
/*@ assigns \result;
- assigns \result \from *((__e_acsl_mpz_struct *)n); */
-int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n)
+ assigns \result \from n; */
+int __gen_e_acsl_g(int n)
{
int __retres = 0;
return __retres;
@@ -626,22 +630,18 @@ int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n)
/*@ assigns \result;
assigns \result \from n; */
-int __gen_e_acsl_f3(int n)
+int __gen_e_acsl_g_11(long n)
{
- int __gen_e_acsl_if_9;
- if (n > 0) {
- int __gen_e_acsl_g_2;
- int __gen_e_acsl_f3_7;
- __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
- __gen_e_acsl_f3_7 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_9 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_7 - 5;
- }
- else {
- int __gen_e_acsl_g_12;
- __gen_e_acsl_g_12 = __gen_e_acsl_g_3(n + 1L);
- __gen_e_acsl_if_9 = __gen_e_acsl_g_12;
- }
- return __gen_e_acsl_if_9;
+ int __retres = 0;
+ return __retres;
+}
+
+/*@ assigns \result;
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
+int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n)
+{
+ int __retres = 0;
+ return __retres;
}
/*@ assigns \result;
@@ -683,7 +683,7 @@ int __gen_e_acsl_f3_2(long n)
__gmpz_add(__gen_e_acsl_add_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
- __gen_e_acsl_g_10 = __gen_e_acsl_g_5((__e_acsl_mpz_struct *)__gen_e_acsl_add_5);
+ __gen_e_acsl_g_10 = __gen_e_acsl_g_9((__e_acsl_mpz_struct *)__gen_e_acsl_add_5);
__gen_e_acsl_if_8 = __gen_e_acsl_g_10;
__gmpz_clear(__gen_e_acsl_n_5);
__gmpz_clear(__gen_e_acsl__21);
@@ -692,6 +692,26 @@ int __gen_e_acsl_f3_2(long n)
return __gen_e_acsl_if_8;
}
+/*@ assigns \result;
+ assigns \result \from n; */
+int __gen_e_acsl_f3(int n)
+{
+ int __gen_e_acsl_if_9;
+ if (n > 0) {
+ int __gen_e_acsl_g_2;
+ int __gen_e_acsl_f3_7;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
+ __gen_e_acsl_f3_7 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_7 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_12;
+ __gen_e_acsl_g_12 = __gen_e_acsl_g_11(n + 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_12;
+ }
+ return __gen_e_acsl_if_9;
+}
+
/*@ assigns \result;
assigns \result \from *((__e_acsl_mpz_struct *)n); */
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n)
@@ -742,25 +762,6 @@ int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * n)
return __gen_e_acsl_if_7;
}
-/*@ assigns \result;
- assigns \result \from n; */
-unsigned long __gen_e_acsl_f4(int n)
-{
- unsigned long __gen_e_acsl_if_15;
- if (n < 100) {
- unsigned long __gen_e_acsl_f4_7;
- __gen_e_acsl_f4_7 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_15 = __gen_e_acsl_f4_7;
- }
- else {
- unsigned long __gen_e_acsl_if_14;
- if ((long)n < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
- else __gen_e_acsl_if_14 = 6UL;
- __gen_e_acsl_if_15 = __gen_e_acsl_if_14;
- }
- return __gen_e_acsl_if_15;
-}
-
/*@ assigns \result;
assigns \result \from n; */
unsigned long __gen_e_acsl_f4_2(long n)
@@ -796,6 +797,25 @@ unsigned long __gen_e_acsl_f4_2(long n)
return __gen_e_acsl_if_13;
}
+/*@ assigns \result;
+ assigns \result \from n; */
+unsigned long __gen_e_acsl_f4(int n)
+{
+ unsigned long __gen_e_acsl_if_15;
+ if (n < 100) {
+ unsigned long __gen_e_acsl_f4_7;
+ __gen_e_acsl_f4_7 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_15 = __gen_e_acsl_f4_7;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_14;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
+ else __gen_e_acsl_if_14 = 6UL;
+ __gen_e_acsl_if_15 = __gen_e_acsl_if_14;
+ }
+ return __gen_e_acsl_if_15;
+}
+
/*@ assigns \result;
assigns \result \from *((__e_acsl_mpz_struct *)n); */
unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n)
@@ -839,40 +859,6 @@ unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * n)
return __gen_e_acsl_if_11;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_if_18;
- if (n >= 0) {
- __e_acsl_mpz_t __gen_e_acsl__26;
- __gmpz_init_set_si(__gen_e_acsl__26,0L);
- __gmpz_init_set(__gen_e_acsl_if_18,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
- __gmpz_clear(__gen_e_acsl__26);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_f5_7;
- __e_acsl_mpz_t __gen_e_acsl_n_8;
- __e_acsl_mpz_t __gen_e_acsl_add_12;
- __gen_e_acsl_f5_2(& __gen_e_acsl_f5_7,n + 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
- __gmpz_init(__gen_e_acsl_add_12);
- __gmpz_add(__gen_e_acsl_add_12,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8));
- __gmpz_init_set(__gen_e_acsl_if_18,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
- __gmpz_clear(__gen_e_acsl_f5_7);
- __gmpz_clear(__gen_e_acsl_n_8);
- __gmpz_clear(__gen_e_acsl_add_12);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_18));
- __gmpz_clear(__gen_e_acsl_if_18);
- return;
-}
-
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n)
@@ -917,6 +903,40 @@ void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
+void __gen_e_acsl_f5(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_18;
+ if (n >= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__26;
+ __gmpz_init_set_si(__gen_e_acsl__26,0L);
+ __gmpz_init_set(__gen_e_acsl_if_18,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
+ __gmpz_clear(__gen_e_acsl__26);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f5_7;
+ __e_acsl_mpz_t __gen_e_acsl_n_8;
+ __e_acsl_mpz_t __gen_e_acsl_add_12;
+ __gen_e_acsl_f5_2(& __gen_e_acsl_f5_7,n + 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
+ __gmpz_init(__gen_e_acsl_add_12);
+ __gmpz_add(__gen_e_acsl_add_12,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8));
+ __gmpz_init_set(__gen_e_acsl_if_18,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_12));
+ __gmpz_clear(__gen_e_acsl_f5_7);
+ __gmpz_clear(__gen_e_acsl_n_8);
+ __gmpz_clear(__gen_e_acsl_add_12);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_18));
+ __gmpz_clear(__gen_e_acsl_if_18);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
index ecb9e3f1e8c4f820254c7696b1173cb4bf5d0988..b1a1f4f23f54b533ae7bebc03525c5ebf687757f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
@@ -13,10 +13,10 @@ logic integer f(integer n) =
n <= 2147483647 + 1 || n >= 9223372036854775807L + 1? 0: f(n + 1) + n;
*/
-void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n);
-
void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n);
+void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n);
+
void __gen_e_acsl_f_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
int main(void)
@@ -79,54 +79,6 @@ int main(void)
return __retres;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n)
-{
- int __gen_e_acsl_or;
- __e_acsl_mpz_t __gen_e_acsl_if_3;
- if ((long)n <= 2147483648L) __gen_e_acsl_or = 1;
- else {
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_ge;
- __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
- __gmpz_init_set_ui(__gen_e_acsl_,9223372036854775807UL + 1UL);
- __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gen_e_acsl_or = __gen_e_acsl_ge >= 0;
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_);
- }
- if (__gen_e_acsl_or) {
- __e_acsl_mpz_t __gen_e_acsl__2;
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_clear(__gen_e_acsl__2);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_f_7;
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
- __gen_e_acsl_f_2(& __gen_e_acsl_f_7,n + 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
- __gmpz_init(__gen_e_acsl_add_5);
- __gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
- __gmpz_clear(__gen_e_acsl_f_7);
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl_add_5);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
- __gmpz_clear(__gen_e_acsl_if_3);
- return;
-}
-
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n)
@@ -189,6 +141,54 @@ void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n)
return;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
+void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n)
+{
+ int __gen_e_acsl_or;
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ if ((long)n <= 2147483648L) __gen_e_acsl_or = 1;
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_ge;
+ __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
+ __gmpz_init_set_ui(__gen_e_acsl_,9223372036854775807UL + 1UL);
+ __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gen_e_acsl_or = __gen_e_acsl_ge >= 0;
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ if (__gen_e_acsl_or) {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f_7;
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __gen_e_acsl_f_2(& __gen_e_acsl_f_7,n + 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ __gmpz_clear(__gen_e_acsl_f_7);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
*/