diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 26e2eec5466422874246fdf59d6117dd6a789cb5..022f7f94c48a7b130f084747ea95af70a73102f8 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,7 @@
Plugin E-ACSL <next-release>
############################
+- E-ACSL [2022-19-07] Improve typing precision of variables appearing in comparisons
-* E-ACSL [2022-17-06] Fix wrong cast from pointer to integer (frama-c/frama-c#1119)
##############################
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
index 473ce5547af126a357533a79d850e3fe18e452d3..ff6fc08f5e8d05749968825aaf6463db4c5df880 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -364,6 +364,11 @@ module Logic_env
type t = { profile : Profile.t;
let_quantif_bind : Profile.t}
+ (* forward reference to meet of intervals *)
+ let ival_meet_ref
+ : (ival -> ival -> ival) ref
+ = ref (fun _i1 _i2 -> Extlib.mk_labeled_fun "ival_meet_ref")
+
let add env x i =
{ env with let_quantif_bind = Logic_var.Map.add x i env.let_quantif_bind}
@@ -382,6 +387,24 @@ module Logic_env
let get_profile env = env.profile
+ let refine env x ival =
+ let update = function
+ | None -> raise Not_found
+ | Some i -> Some (!ival_meet_ref i ival)
+ in
+ let new_lq_bind =
+ try Logic_var.Map.update x update env.let_quantif_bind
+ with Not_found ->
+ match Logic_var.Map.find_opt x env.profile with
+ | Some i ->
+ (* The profile must remain unchanged, so if the variable is bound in
+ the profile, we add the refined interval in the other bindings,
+ which are checked first when finding the interval *)
+ Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
+ | None -> Options.abort "updating a variable not in environment"
+ in
+ {env with let_quantif_bind = new_lq_bind}
+
end
(* Imperative environment to perform fixpoint algorithm for recursive
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 008856976aa48dc11e4b8ac6c5459ca3c8e5870d..9cafe69c93a70301e49ffe2d73ccf84a3d6120c4 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -76,17 +76,29 @@ module LFProf: Datatype.S_with_collections
- an association list for variables bound by a let or a quantification *)
module Logic_env : sig
type t
- (* add a new binding for a let or a quantification binder only *)
+
+ (** forward reference to meet of intervals *)
+ val ival_meet_ref : (ival -> ival -> ival) ref
+
+ (** add a new binding for a let or a quantification binder only *)
val add : t -> logic_var -> ival -> t
- (* the empty environment *)
+
+ (** the empty environment *)
val empty : t
- (* create a new environment from a profile, for function calls *)
+
+ (** create a new environment from a profile, for function calls *)
val make : Profile.t -> t
- (* find a logic variable in the environment *)
+
+ (** find a logic variable in the environment *)
val find : t -> logic_var -> ival
- (* get the profile of the logic environment, i.e. bindings through function
- arguments *)
+
+ (** get the profile of the logic environment, i.e. bindings through function
+ arguments *)
val get_profile : t -> Profile.t
+
+ (** refine the interval of a logic variable: replace an interval with a more
+ precise one *)
+ val refine : t -> logic_var -> ival -> t
end
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index f68cae7dcf7b99d17e06792c8fc7208ba865af0c..833d84ed21d5755e1b3763d8da9ac37b62d9d232 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -216,6 +216,8 @@ let meet i1 i2 = match i1, i2 with
| Nan, (Ival _ | Float _ | Rational | Real) ->
Nan
+let () = Logic_env.ival_meet_ref := meet
+
let is_singleton_int = function
| Ival iv -> Ival.is_singleton_int iv
| Float _ | Rational | Real | Nan -> false
@@ -372,7 +374,8 @@ let rec fixpoint ~(infer : force:bool ->
then
ival
else
- fixpoint ~infer li args_ival t' inferred_ival
+ let assumed_ival = interv_of_typ_containing_interv inferred_ival in
+ fixpoint ~infer li args_ival t' assumed_ival
(* Memoization module which retrieves the computed info of some terms *)
@@ -683,8 +686,11 @@ let rec infer ~force ~logic_env t =
Error.map (fun src -> cast ~src ~dst) src
| Tif (t1, t2, t3) ->
ignore (infer ~force ~logic_env t1);
- let i2 = infer ~force ~logic_env t2 in
- let i3 = infer ~force ~logic_env t3 in
+ let logic_env_tbranch, logic_env_fbranch =
+ compute_logic_env_if_branches logic_env t1
+ in
+ let i2 = infer ~force ~logic_env:logic_env_tbranch t2 in
+ let i3 = infer ~force ~logic_env:logic_env_fbranch t3 in
Error.map2 join i2 i3
| Tat (t, _) ->
get_res (infer ~force ~logic_env t)
@@ -873,7 +879,6 @@ and infer_term_host ~force ~logic_env thost =
Printer.pp_typ ty
Printer.pp_term t
-
and infer_term_offset ~force ~logic_env t =
match t with
| TNoOffset -> ()
@@ -883,6 +888,65 @@ and infer_term_offset ~force ~logic_env t =
ignore (infer ~force ~logic_env t);
infer_term_offset ~force ~logic_env toff
+(* Update the interval of variables when they appear in a comparison of the form
+ [x op t] or [t op x] *)
+and compute_logic_env_if_branches logic_env t =
+ let get_res = Error.map (fun x -> x) in
+ let ival v = infer ~force:false ~logic_env v in
+ let add_ub logic_env x v =
+ let max = Ival.max_int (Error.map extract_ival (ival v)) in
+ Logic_env.refine logic_env x (Ival (Ival.inject_range None max))
+ in
+ let add_lb logic_env x v =
+ let min = Ival.min_int (Error.map extract_ival (ival v)) in
+ Logic_env.refine logic_env x (Ival (Ival.inject_range min None))
+ in
+ let add_eq logic_env x v = Logic_env.refine logic_env x (get_res (ival v)) in
+ let t_branch, f_branch =
+ (* we do not discriminate between strict and weak inequalities. This is
+ slighlty less precise but allow for better reusing of the code in the
+ case of recursive functions, the main advantage in typing
+ conditionals is for recursive functions. *)
+ match t.term_node with
+ | TBinOp(op, {term_node = TLval(TVar x, TNoOffset)}, v) ->
+ begin
+ match op with
+ | Lt | Le ->
+ add_ub logic_env x v,
+ add_lb logic_env x v
+ | Gt | Ge ->
+ add_lb logic_env x v,
+ add_ub logic_env x v
+ | Eq ->
+ add_eq logic_env x v,
+ logic_env
+ | Ne ->
+ logic_env,
+ add_eq logic_env x v
+ | _ -> logic_env, logic_env
+ end
+ | _ -> logic_env, logic_env
+ in
+ match t.term_node with
+ | TBinOp(op, u, {term_node = TLval(TVar y, TNoOffset)}) ->
+ begin
+ match op with
+ | Lt | Le ->
+ add_lb t_branch y u,
+ add_ub f_branch y u
+ | Gt | Ge ->
+ add_ub t_branch y u,
+ add_lb f_branch y u
+ | Eq ->
+ add_eq t_branch y u,
+ logic_env
+ | Ne ->
+ logic_env,
+ add_eq f_branch y u
+ | _ -> t_branch, f_branch
+ end
+ | _ -> t_branch, f_branch
+
(* [type_bound_variables] infers an interval associated with each of
the provided bounds of a quantified variable, and provides a term
accordingly. It could happen that the bounds provided for a quantifier
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
index 5ce2b09c6a5151a2f4f4784de94a3f912ba7603b..dfb2831b7e1fb2c512075fbb37544a05759f0641 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
@@ -55,7 +55,7 @@
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +
+ (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 26) +
(int)(__gen_e_acsl_v_5 - -4)));
[eva:alarm] at_on-purely-logic-variables.c:44: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
index 7293519451467d7b3861614cf3e118233b83f1bd..d064060bb6adc24506499219f6f10a0afa5ffc35 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
@@ -3,127 +3,30 @@
[eva:alarm] functions_rec.c:28: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions_rec.c:28: Warning: assertion got status unknown.
+[eva] functions_rec.c:10: Warning:
+ Using specification of function __gen_e_acsl_f1 for recursive calls.
+ Analysis of function __gen_e_acsl_f1 is thus incomplete and its soundness
+ relies on the written specification.
[eva:alarm] functions_rec.c:29: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions_rec.c:29: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:10: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
-[eva:alarm] functions_rec.c:10: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
-[eva] functions_rec.c:10: Warning:
- Using specification of function __gen_e_acsl_f1_3 for recursive calls.
- Analysis of function __gen_e_acsl_f1_3 is thus incomplete and its soundness
- relies on the written specification.
[eva:alarm] functions_rec.c:30: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions_rec.c:30: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:13: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
-[eva:alarm] functions_rec.c:13: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
[eva] functions_rec.c:13: Warning:
- Using specification of function __gen_e_acsl_f2_3 for recursive calls.
- Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
+ Using specification of function __gen_e_acsl_f2 for recursive calls.
+ Analysis of function __gen_e_acsl_f2 is thus incomplete and its soundness
relies on the written specification.
-[eva:alarm] functions_rec.c:13: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
[eva] functions_rec.c:13: Warning:
- Using specification of function __gen_e_acsl_f2_3 for recursive calls.
- Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
+ Using specification of function __gen_e_acsl_f2 for recursive calls.
+ Analysis of function __gen_e_acsl_f2 is thus incomplete and its soundness
relies on the written specification.
-[eva:alarm] functions_rec.c:13: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
[eva] functions_rec.c:13: Warning:
- Using specification of function __gen_e_acsl_f2_3 for recursive calls.
- Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
+ Using specification of function __gen_e_acsl_f2 for recursive calls.
+ Analysis of function __gen_e_acsl_f2 is thus incomplete and its soundness
relies on the written specification.
+[eva:alarm] functions_rec.c:13: Warning: assertion 'E_ACSL' got status unknown.
[eva:alarm] functions_rec.c:13: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions_rec.c:13: Warning:
- division by zero. assert __gen_e_acsl_f2_9 != 0;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow. assert -2147483648 <= __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow. assert __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7 <= 2147483647;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow.
- assert
- (int)(__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9 <=
- 2147483647;
-[eva:alarm] functions_rec.c:13: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
-[eva:alarm] functions_rec.c:13: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
-[eva:alarm] functions_rec.c:13: Warning:
- division by zero. assert __gen_e_acsl_f2_14 != 0;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow.
- assert -2147483648 <= __gen_e_acsl_f2_10 * __gen_e_acsl_f2_12;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow.
- assert __gen_e_acsl_f2_10 * __gen_e_acsl_f2_12 <= 2147483647;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow.
- assert
- (int)(__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14 <=
- 2147483647;
-[eva:alarm] functions_rec.c:13: Warning:
- division by zero. assert __gen_e_acsl_f2_19 != 0;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow.
- assert -2147483648 <= __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow.
- assert __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 <= 2147483647;
-[eva:alarm] functions_rec.c:13: Warning:
- signed overflow.
- assert
- (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19 <=
- 2147483647;
-[eva:alarm] functions_rec.c:32: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:32: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:17: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
-[eva:alarm] functions_rec.c:17: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
-[eva] functions_rec.c:17: Warning:
- Using specification of function __gen_e_acsl_f3_3 for recursive calls.
- Analysis of function __gen_e_acsl_f3_3 is thus incomplete and its soundness
- relies on the written specification.
-[eva:alarm] functions_rec.c:17: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
-[eva:alarm] functions_rec.c:34: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:20: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
-[eva:alarm] functions_rec.c:20: Warning:
- accessing uninitialized left-value.
- assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
-[eva] functions_rec.c:20: Warning:
- Using specification of function __gen_e_acsl_f4_3 for recursive calls.
- Analysis of function __gen_e_acsl_f4_3 is thus incomplete and its soundness
- relies on the written specification.
-[eva:alarm] functions_rec.c:36: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:36: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:38: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:38: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:40: Warning:
- function __e_acsl_assert_register_mpz: precondition data->values == \null ||
- \valid(data->values) got status unknown.
-[eva:alarm] functions_rec.c:40: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:40: Warning: assertion got status unknown.
+ accessing uninitialized left-value. assert \initialized(&n);
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
index 3c3a420f8486821f434161ac28104f028b301c80..54abb67f00134052a63240bbff4b4cf8de25563b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
@@ -113,7 +113,7 @@ int main(void)
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
__gen_e_acsl_at_8 = (long *)malloc(64UL);
__gen_e_acsl_at_7 = (int *)malloc(12000UL);
- __gen_e_acsl_at_6 = (long *)malloc(3072UL);
+ __gen_e_acsl_at_6 = (long *)malloc(2496UL);
__gen_e_acsl_at_5 = (int *)malloc(528UL);
__gen_e_acsl_at_3 = (int *)malloc(12UL);
__gen_e_acsl_at_2 = (long *)malloc(8UL);
@@ -182,7 +182,7 @@ int main(void)
else __gen_e_acsl_if_2 = 3;
if (__gen_e_acsl_v_2 <= __gen_e_acsl_if_2) ; else break;
}
- *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_2 - 9) * 32 + (__gen_e_acsl_v_2 - -4))) =
+ *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_2 - 9) * 26 + (__gen_e_acsl_v_2 - -4))) =
(n + (long)__gen_e_acsl_u_2) + __gen_e_acsl_v_2;
__gen_e_acsl_v_2 ++;
}
@@ -547,7 +547,7 @@ int main(void)
__gen_e_acsl_at_6 + (int)(
(long)((int)(
(long)((int)(
- __gen_e_acsl_u_7 - 9L)) * 32L)) + (int)(
+ __gen_e_acsl_u_7 - 9L)) * 26L)) + (int)(
__gen_e_acsl_v_5 - -4L))),
sizeof(long),
(void *)__gen_e_acsl_at_6,
@@ -565,7 +565,7 @@ int main(void)
"sizeof(long)",0,sizeof(long));
__gen_e_acsl_assert_data_12.blocking = 1;
__gen_e_acsl_assert_data_12.kind = "RTE";
- __gen_e_acsl_assert_data_12.pred_txt = "\\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +\n (int)(__gen_e_acsl_v_5 - -4)))";
+ __gen_e_acsl_assert_data_12.pred_txt = "\\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 26) +\n (int)(__gen_e_acsl_v_5 - -4)))";
__gen_e_acsl_assert_data_12.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 46;
@@ -576,10 +576,10 @@ int main(void)
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_6 +
- (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32)
+ (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 26)
+ (int)(__gen_e_acsl_v_5 - -4)));
*/
- if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_7 - 9) * 32 + (
+ if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_7 - 9) * 26 + (
__gen_e_acsl_v_5 - -4))) > 0L)
;
else {
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 fb1832ca1932365758dee4c7644baaca1cd4882a..95fb94d1c880ce5ac7c7313803b6647c83428c95 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
@@ -9,81 +9,52 @@
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_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_2(long n);
-
-int __gen_e_acsl_f2(int n);
-
-int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * n);
+ */
+void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n);
/*@ logic integer g(integer n) = 0;
+ */
+int __gen_e_acsl_g_3(int n);
-*/
-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_11(long n);
-
-int __gen_e_acsl_g_5(__e_acsl_mpz_struct * n);
+int __gen_e_acsl_g(unsigned int n);
/*@ logic integer f3(integer n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
-
-*/
-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);
-
/*@
logic integer f4(integer n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
-
-*/
-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_2(__e_acsl_mpz_t *__retres_arg, long n);
+void __gen_e_acsl_f5_5(__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)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
{
- __e_acsl_mpz_t __gen_e_acsl_f1_8;
- __e_acsl_mpz_t __gen_e_acsl__7;
+ __e_acsl_mpz_t __gen_e_acsl_f1_4;
+ __e_acsl_mpz_t __gen_e_acsl__2;
int __gen_e_acsl_eq;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __gen_e_acsl_f1(& __gen_e_acsl_f1_8,0);
- __gmpz_init_set_si(__gen_e_acsl__7,0L);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_4,0);
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data,"f1(0)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
__gen_e_acsl_assert_data.pred_txt = "f1(0) == 0";
@@ -92,22 +63,22 @@ int main(void)
__gen_e_acsl_assert_data.line = 28;
__e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- __gmpz_clear(__gen_e_acsl_f1_8);
- __gmpz_clear(__gen_e_acsl__7);
+ __gmpz_clear(__gen_e_acsl_f1_4);
+ __gmpz_clear(__gen_e_acsl__2);
}
/*@ assert f1(0) == 0; */ ;
{
- __e_acsl_mpz_t __gen_e_acsl_f1_10;
- __e_acsl_mpz_t __gen_e_acsl__8;
+ __e_acsl_mpz_t __gen_e_acsl_f1_6;
+ __e_acsl_mpz_t __gen_e_acsl__3;
int __gen_e_acsl_eq_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_f1(& __gen_e_acsl_f1_10,1);
- __gmpz_init_set_si(__gen_e_acsl__8,1L);
- __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_6,1);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_2,"f1(1)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_10));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
__gen_e_acsl_assert_data_2.pred_txt = "f1(1) == 1";
@@ -116,22 +87,22 @@ int main(void)
__gen_e_acsl_assert_data_2.line = 29;
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- __gmpz_clear(__gen_e_acsl_f1_10);
- __gmpz_clear(__gen_e_acsl__8);
+ __gmpz_clear(__gen_e_acsl_f1_6);
+ __gmpz_clear(__gen_e_acsl__3);
}
/*@ assert f1(1) == 1; */ ;
{
- __e_acsl_mpz_t __gen_e_acsl_f1_12;
- __e_acsl_mpz_t __gen_e_acsl__9;
+ __e_acsl_mpz_t __gen_e_acsl_f1_8;
+ __e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __gen_e_acsl_f1(& __gen_e_acsl_f1_12,100);
- __gmpz_init_set_si(__gen_e_acsl__9,5050L);
- __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_12),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_8,100);
+ __gmpz_init_set_si(__gen_e_acsl__4,5050L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,"f1(100)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_12));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8));
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Assertion";
__gen_e_acsl_assert_data_3.pred_txt = "f1(100) == 5050";
@@ -140,111 +111,122 @@ int main(void)
__gen_e_acsl_assert_data_3.line = 30;
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
- __gmpz_clear(__gen_e_acsl_f1_12);
- __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl_f1_8);
+ __gmpz_clear(__gen_e_acsl__4);
}
/*@ assert f1(100) == 5050; */ ;
{
- int __gen_e_acsl_f2_20;
+ __e_acsl_mpz_t __gen_e_acsl_f2_8;
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ int __gen_e_acsl_eq_4;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __gen_e_acsl_f2_20 = __gen_e_acsl_f2(7);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,"f2(7)",0,
- __gen_e_acsl_f2_20);
+ __gen_e_acsl_f2(& __gen_e_acsl_f2_8,7);
+ __gmpz_init_set_si(__gen_e_acsl__7,1L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ /*@ assert Eva: initialization: \initialized(&n); */
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,"n",0,n);
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_5,"f2(n - 3)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_7));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_4,"f2(7)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8));
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "Assertion";
__gen_e_acsl_assert_data_4.pred_txt = "f2(7) == 1";
__gen_e_acsl_assert_data_4.file = "functions_rec.c";
__gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 32;
- __e_acsl_assert(__gen_e_acsl_f2_20 == 1,& __gen_e_acsl_assert_data_4);
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
+ __gmpz_clear(__gen_e_acsl_f2_8);
+ __gmpz_clear(__gen_e_acsl__7);
}
/*@ assert f2(7) == 1; */ ;
{
- int __gen_e_acsl_f3_8;
+ int __gen_e_acsl_f3_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
+ {.values = (void *)0};
+ __gen_e_acsl_f3_4 = __gen_e_acsl_f3(6);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,"f3(6)",0,
+ __gen_e_acsl_f3_4);
+ __gen_e_acsl_assert_data_6.blocking = 1;
+ __gen_e_acsl_assert_data_6.kind = "Assertion";
+ __gen_e_acsl_assert_data_6.pred_txt = "f3(6) == -5";
+ __gen_e_acsl_assert_data_6.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_6.fct = "main";
+ __gen_e_acsl_assert_data_6.line = 34;
+ __e_acsl_assert(__gen_e_acsl_f3_4 == -5,& __gen_e_acsl_assert_data_6);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
+ }
+ /*@ assert f3(6) == -5; */ ;
+ {
+ unsigned long __gen_e_acsl_f4_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_7 =
+ {.values = (void *)0};
+ __gen_e_acsl_f4_4 = __gen_e_acsl_f4(9);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_7,"f4(9)",0,
+ __gen_e_acsl_f4_4);
+ __gen_e_acsl_assert_data_7.blocking = 1;
+ __gen_e_acsl_assert_data_7.kind = "Assertion";
+ __gen_e_acsl_assert_data_7.pred_txt = "f4(9) > 0";
+ __gen_e_acsl_assert_data_7.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_7.fct = "main";
+ __gen_e_acsl_assert_data_7.line = 36;
+ __e_acsl_assert(__gen_e_acsl_f4_4 > 0UL,& __gen_e_acsl_assert_data_7);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
+ }
+ /*@ assert f4(9) > 0; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f5_4;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_eq_5;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
- __gen_e_acsl_f3_8 = __gen_e_acsl_f3(6);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,"f3(6)",0,
- __gen_e_acsl_f3_8);
+ __gen_e_acsl_f5(& __gen_e_acsl_f5_4,0);
+ __gmpz_init_set_si(__gen_e_acsl__9,0L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_8,"f5(0)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_4));
__gen_e_acsl_assert_data_8.blocking = 1;
__gen_e_acsl_assert_data_8.kind = "Assertion";
- __gen_e_acsl_assert_data_8.pred_txt = "f3(6) == -5";
+ __gen_e_acsl_assert_data_8.pred_txt = "f5(0) == 0";
__gen_e_acsl_assert_data_8.file = "functions_rec.c";
__gen_e_acsl_assert_data_8.fct = "main";
- __gen_e_acsl_assert_data_8.line = 34;
- __e_acsl_assert(__gen_e_acsl_f3_8 == -5,& __gen_e_acsl_assert_data_8);
+ __gen_e_acsl_assert_data_8.line = 38;
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
+ __gmpz_clear(__gen_e_acsl_f5_4);
+ __gmpz_clear(__gen_e_acsl__9);
}
- /*@ assert f3(6) == -5; */ ;
+ /*@ assert f5(0) == 0; */ ;
{
- unsigned long __gen_e_acsl_f4_8;
+ long __gen_e_acsl_n_3;
+ __e_acsl_mpz_t __gen_e_acsl_f5_8;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ int __gen_e_acsl_eq_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
{.values = (void *)0};
- __gen_e_acsl_f4_8 = __gen_e_acsl_f4(9);
- __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_9,"f4(9)",0,
- __gen_e_acsl_f4_8);
+ __gen_e_acsl_n_3 = 9223372036854775807L;
+ __gen_e_acsl_f5_5(& __gen_e_acsl_f5_8,__gen_e_acsl_n_3);
+ __gmpz_init_set_si(__gen_e_acsl__11,0L);
+ __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_9,"n",0,
+ __gen_e_acsl_n_3);
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_9,"f5(n)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8));
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "Assertion";
- __gen_e_acsl_assert_data_9.pred_txt = "f4(9) > 0";
+ __gen_e_acsl_assert_data_9.pred_txt = "\\let n = 0 == 0? 0x7fffffffffffffffL: -1; f5(n) == 0";
__gen_e_acsl_assert_data_9.file = "functions_rec.c";
__gen_e_acsl_assert_data_9.fct = "main";
- __gen_e_acsl_assert_data_9.line = 36;
- __e_acsl_assert(__gen_e_acsl_f4_8 > 0UL,& __gen_e_acsl_assert_data_9);
+ __gen_e_acsl_assert_data_9.line = 40;
+ __e_acsl_assert(__gen_e_acsl_eq_6 == 0,& __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
- }
- /*@ assert f4(9) > 0; */ ;
- {
- __e_acsl_mpz_t __gen_e_acsl_f5_8;
- __e_acsl_mpz_t __gen_e_acsl__32;
- int __gen_e_acsl_eq_4;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
- {.values = (void *)0};
- __gen_e_acsl_f5(& __gen_e_acsl_f5_8,0);
- __gmpz_init_set_si(__gen_e_acsl__32,0L);
- __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
- __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_10,"f5(0)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8));
- __gen_e_acsl_assert_data_10.blocking = 1;
- __gen_e_acsl_assert_data_10.kind = "Assertion";
- __gen_e_acsl_assert_data_10.pred_txt = "f5(0) == 0";
- __gen_e_acsl_assert_data_10.file = "functions_rec.c";
- __gen_e_acsl_assert_data_10.fct = "main";
- __gen_e_acsl_assert_data_10.line = 38;
- __e_acsl_assert(__gen_e_acsl_eq_4 == 0,& __gen_e_acsl_assert_data_10);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
__gmpz_clear(__gen_e_acsl_f5_8);
- __gmpz_clear(__gen_e_acsl__32);
- }
- /*@ assert f5(0) == 0; */ ;
- {
- long __gen_e_acsl_n_9;
- __e_acsl_mpz_t __gen_e_acsl_f5_10;
- __e_acsl_mpz_t __gen_e_acsl__33;
- int __gen_e_acsl_eq_5;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
- {.values = (void *)0};
- __gen_e_acsl_n_9 = 9223372036854775807L;
- __gen_e_acsl_f5_2(& __gen_e_acsl_f5_10,__gen_e_acsl_n_9);
- __gmpz_init_set_si(__gen_e_acsl__33,0L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_11,"n",0,
- __gen_e_acsl_n_9);
- __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_11,"f5(n)",0,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_10));
- __gen_e_acsl_assert_data_11.blocking = 1;
- __gen_e_acsl_assert_data_11.kind = "Assertion";
- __gen_e_acsl_assert_data_11.pred_txt = "\\let n = 0 == 0? 0x7fffffffffffffffL: -1; f5(n) == 0";
- __gen_e_acsl_assert_data_11.file = "functions_rec.c";
- __gen_e_acsl_assert_data_11.fct = "main";
- __gen_e_acsl_assert_data_11.line = 40;
- __e_acsl_assert(__gen_e_acsl_eq_5 == 0,& __gen_e_acsl_assert_data_11);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
- __gmpz_clear(__gen_e_acsl_f5_10);
- __gmpz_clear(__gen_e_acsl__33);
+ __gmpz_clear(__gen_e_acsl__11);
}
/*@ assert \let n = 0 == 0? 0x7fffffffffffffffL: -1; f5(n) == 0; */ ;
__retres = 0;
@@ -252,377 +234,106 @@ int main(void)
return __retres;
}
-/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f1_2(__e_acsl_mpz_t *__retres_arg, long n)
-{
- __e_acsl_mpz_t __gen_e_acsl_if_2;
- if (n <= 0L) {
- __e_acsl_mpz_t __gen_e_acsl__2;
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_clear(__gen_e_acsl__2);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl_f1_6;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __gmpz_init_set_si(__gen_e_acsl_n,n);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- */
- __gen_e_acsl_f1_3(& __gen_e_acsl_f1_6,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
- __gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl_f1_6);
- __gmpz_clear(__gen_e_acsl_add_2);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gmpz_clear(__gen_e_acsl_if_2);
- 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;
+ __e_acsl_mpz_t __gen_e_acsl_if;
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,
+ __gmpz_init_set(__gen_e_acsl_if,
(__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);
- */
-void __gen_e_acsl_f1_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
-{
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_le;
- __e_acsl_mpz_t __gen_e_acsl_if;
- __gmpz_init_set_si(__gen_e_acsl__4,0L);
- __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
- if (__gen_e_acsl_le <= 0) {
- __e_acsl_mpz_t __gen_e_acsl__5;
- __gmpz_init_set_si(__gen_e_acsl__5,0L);
- __gmpz_init_set(__gen_e_acsl_if,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
- __gmpz_clear(__gen_e_acsl__5);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__6;
- __e_acsl_mpz_t __gen_e_acsl_sub_2;
- __e_acsl_mpz_t __gen_e_acsl_f1_5;
+ __e_acsl_mpz_t __gen_e_acsl_f1_3;
+ __e_acsl_mpz_t __gen_e_acsl_n;
__e_acsl_mpz_t __gen_e_acsl_add;
- __gmpz_init_set_si(__gen_e_acsl__6,1L);
- __gmpz_init(__gen_e_acsl_sub_2);
- __gmpz_sub(__gen_e_acsl_sub_2,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
- */
- __gen_e_acsl_f1_3(& __gen_e_acsl_f1_5,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_3,n - 1);
+ __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_5),
- (__e_acsl_mpz_struct const *)(n));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n));
__gmpz_init_set(__gen_e_acsl_if,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
- __gmpz_clear(__gen_e_acsl__6);
- __gmpz_clear(__gen_e_acsl_sub_2);
- __gmpz_clear(__gen_e_acsl_f1_5);
+ __gmpz_clear(__gen_e_acsl_f1_3);
+ __gmpz_clear(__gen_e_acsl_n);
__gmpz_clear(__gen_e_acsl_add);
}
__gmpz_init_set(*__retres_arg,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
- __gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_if);
return;
}
-/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_f2_2(long n)
-{
- int __gen_e_acsl_if_5;
- if (n < 0L) __gen_e_acsl_if_5 = 1;
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_3;
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl_sub_3;
- int __gen_e_acsl_f2_10;
- __e_acsl_mpz_t __gen_e_acsl__15;
- __e_acsl_mpz_t __gen_e_acsl_sub_7;
- int __gen_e_acsl_f2_12;
- __e_acsl_mpz_t __gen_e_acsl__16;
- __e_acsl_mpz_t __gen_e_acsl_sub_8;
- int __gen_e_acsl_f2_14;
- __gmpz_init_set_si(__gen_e_acsl_n_3,n);
- __gmpz_init_set_si(__gen_e_acsl__10,1L);
- __gmpz_init(__gen_e_acsl_sub_3);
- __gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
- */
- __gen_e_acsl_f2_10 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
- __gmpz_init_set_si(__gen_e_acsl__15,2L);
- __gmpz_init(__gen_e_acsl_sub_7);
- __gmpz_sub(__gen_e_acsl_sub_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
- */
- __gen_e_acsl_f2_12 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
- __gmpz_init_set_si(__gen_e_acsl__16,3L);
- __gmpz_init(__gen_e_acsl_sub_8);
- __gmpz_sub(__gen_e_acsl_sub_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
- */
- __gen_e_acsl_f2_14 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_6 =
- {.values = (void *)0};
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_6,
- "__gen_e_acsl_f2_14",0,__gen_e_acsl_f2_14);
- __gen_e_acsl_assert_data_6.blocking = 1;
- __gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "__gen_e_acsl_f2_14 != 0";
- __gen_e_acsl_assert_data_6.file = "functions_rec.c";
- __gen_e_acsl_assert_data_6.fct = "f2_2";
- __gen_e_acsl_assert_data_6.line = 13;
- __gen_e_acsl_assert_data_6.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_f2_14 != 0,& __gen_e_acsl_assert_data_6);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_14 != 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 <= __gen_e_acsl_f2_10 * __gen_e_acsl_f2_12;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_10 * __gen_e_acsl_f2_12 <= 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14
- <= 2147483647;
- */
- __gen_e_acsl_if_5 = (__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14;
- __gmpz_clear(__gen_e_acsl_n_3);
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl_sub_3);
- __gmpz_clear(__gen_e_acsl__15);
- __gmpz_clear(__gen_e_acsl_sub_7);
- __gmpz_clear(__gen_e_acsl__16);
- __gmpz_clear(__gen_e_acsl_sub_8);
- }
- return __gen_e_acsl_if_5;
-}
-
-/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_f2(int n)
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from n; */
+void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, 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;
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ if (n < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ __gmpz_clear(__gen_e_acsl__5);
}
- 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)
-{
- __e_acsl_mpz_t __gen_e_acsl__11;
- int __gen_e_acsl_lt;
- int __gen_e_acsl_if_4;
- __gmpz_init_set_si(__gen_e_acsl__11,0L);
- __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- if (__gen_e_acsl_lt < 0) __gen_e_acsl_if_4 = 1;
else {
- __e_acsl_mpz_t __gen_e_acsl__12;
- __e_acsl_mpz_t __gen_e_acsl_sub_4;
- int __gen_e_acsl_f2_5;
- __e_acsl_mpz_t __gen_e_acsl__13;
- __e_acsl_mpz_t __gen_e_acsl_sub_5;
- int __gen_e_acsl_f2_7;
- __e_acsl_mpz_t __gen_e_acsl__14;
- __e_acsl_mpz_t __gen_e_acsl_sub_6;
- int __gen_e_acsl_f2_9;
- __gmpz_init_set_si(__gen_e_acsl__12,1L);
- __gmpz_init(__gen_e_acsl_sub_4);
- __gmpz_sub(__gen_e_acsl_sub_4,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
- */
- __gen_e_acsl_f2_5 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
- __gmpz_init_set_si(__gen_e_acsl__13,2L);
- __gmpz_init(__gen_e_acsl_sub_5);
- __gmpz_sub(__gen_e_acsl_sub_5,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
- */
- __gen_e_acsl_f2_7 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
- __gmpz_init_set_si(__gen_e_acsl__14,3L);
- __gmpz_init(__gen_e_acsl_sub_6);
- __gmpz_sub(__gen_e_acsl_sub_6,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
- */
- __gen_e_acsl_f2_9 = __gen_e_acsl_f2_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+ __e_acsl_mpz_t __gen_e_acsl_f2_3;
+ __e_acsl_mpz_t __gen_e_acsl_f2_5;
+ __e_acsl_mpz_t __gen_e_acsl_mul;
+ __e_acsl_mpz_t __gen_e_acsl_f2_7;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ int __gen_e_acsl_div_guard;
+ __e_acsl_mpz_t __gen_e_acsl_div;
+ __gen_e_acsl_f2(& __gen_e_acsl_f2_3,n - 1);
+ __gen_e_acsl_f2(& __gen_e_acsl_f2_5,n - 2);
+ __gmpz_init(__gen_e_acsl_mul);
+ __gmpz_mul(__gen_e_acsl_mul,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_5));
__e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
{.values = (void *)0};
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_5,
- "__gen_e_acsl_f2_9",0,__gen_e_acsl_f2_9);
- __gen_e_acsl_assert_data_5.blocking = 1;
- __gen_e_acsl_assert_data_5.kind = "RTE";
- __gen_e_acsl_assert_data_5.pred_txt = "__gen_e_acsl_f2_9 != 0";
- __gen_e_acsl_assert_data_5.file = "functions_rec.c";
- __gen_e_acsl_assert_data_5.fct = "f2_3";
- __gen_e_acsl_assert_data_5.line = 13;
- __gen_e_acsl_assert_data_5.name = "division_by_zero";
- __e_acsl_assert(__gen_e_acsl_f2_9 != 0,& __gen_e_acsl_assert_data_5);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_9 != 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 <= __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7 <= 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9 <=
- 2147483647;
- */
- __gen_e_acsl_if_4 = (__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9;
- __gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl_sub_4);
- __gmpz_clear(__gen_e_acsl__13);
- __gmpz_clear(__gen_e_acsl_sub_5);
- __gmpz_clear(__gen_e_acsl__14);
- __gmpz_clear(__gen_e_acsl_sub_6);
+ __gen_e_acsl_f2(& __gen_e_acsl_f2_7,n - 3);
+ __gmpz_init_set_si(__gen_e_acsl__6,0L);
+ __gen_e_acsl_div_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ __gmpz_init(__gen_e_acsl_div);
+ /*@ assert E_ACSL: f2(n - 3) != 0; */
+ {
+ __gen_e_acsl_assert_data_5.blocking = 1;
+ __gen_e_acsl_assert_data_5.kind = "Assertion";
+ __gen_e_acsl_assert_data_5.pred_txt = "f2(n - 3) != 0";
+ __gen_e_acsl_assert_data_5.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_5.fct = "f2";
+ __gen_e_acsl_assert_data_5.line = 13;
+ __e_acsl_assert(__gen_e_acsl_div_guard != 0,
+ & __gen_e_acsl_assert_data_5);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
+ }
+ __gmpz_tdiv_q(__gen_e_acsl_div,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_7));
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
+ __gmpz_clear(__gen_e_acsl_f2_3);
+ __gmpz_clear(__gen_e_acsl_f2_5);
+ __gmpz_clear(__gen_e_acsl_mul);
+ __gmpz_clear(__gen_e_acsl_f2_7);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_div);
}
- __gmpz_clear(__gen_e_acsl__11);
- return __gen_e_acsl_if_4;
-}
-
-/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_g_3(long n)
-{
- int __retres = 0;
- return __retres;
-}
-
-/*@ assigns \result;
- assigns \result \from *((__e_acsl_mpz_struct *)n); */
-int __gen_e_acsl_g_9(__e_acsl_mpz_struct * n)
-{
- int __retres = 0;
- return __retres;
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gmpz_clear(__gen_e_acsl_if_2);
+ return;
}
/*@ assigns \result;
assigns \result \from n; */
-int __gen_e_acsl_g(int n)
+int __gen_e_acsl_g_3(int n)
{
int __retres = 0;
return __retres;
@@ -630,357 +341,116 @@ int __gen_e_acsl_g(int n)
/*@ assigns \result;
assigns \result \from n; */
-int __gen_e_acsl_g_11(long 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)
+int __gen_e_acsl_g(unsigned int n)
{
int __retres = 0;
return __retres;
}
-/*@ assigns \result;
- assigns \result \from n; */
-int __gen_e_acsl_f3_2(long n)
-{
- int __gen_e_acsl_if_8;
- if (n > 0L) {
- int __gen_e_acsl_g_4;
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl__17;
- __e_acsl_mpz_t __gen_e_acsl_sub_9;
- int __gen_e_acsl_f3_6;
- __gen_e_acsl_g_4 = __gen_e_acsl_g_3(n);
- __gmpz_init_set_si(__gen_e_acsl_n_4,n);
- __gmpz_init_set_si(__gen_e_acsl__17,1L);
- __gmpz_init(__gen_e_acsl_sub_9);
- __gmpz_sub(__gen_e_acsl_sub_9,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
- */
- __gen_e_acsl_f3_6 = __gen_e_acsl_f3_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
- __gen_e_acsl_if_8 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_6 - 5;
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl__17);
- __gmpz_clear(__gen_e_acsl_sub_9);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_5;
- __e_acsl_mpz_t __gen_e_acsl__21;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
- int __gen_e_acsl_g_10;
- __gmpz_init_set_si(__gen_e_acsl_n_5,n);
- __gmpz_init_set_si(__gen_e_acsl__21,1L);
- __gmpz_init(__gen_e_acsl_add_5);
- __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_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);
- __gmpz_clear(__gen_e_acsl_add_5);
- }
- 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;
+ int __gen_e_acsl_if_3;
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;
+ int __gen_e_acsl_f3_3;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g((unsigned int)n);
+ __gen_e_acsl_f3_3 = __gen_e_acsl_f3(n - 1);
+ __gen_e_acsl_if_3 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_3 - 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)
-{
- __e_acsl_mpz_t __gen_e_acsl__18;
- int __gen_e_acsl_gt;
- int __gen_e_acsl_if_7;
- __gmpz_init_set_si(__gen_e_acsl__18,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__18));
- if (__gen_e_acsl_gt > 0) {
- int __gen_e_acsl_g_6;
- __e_acsl_mpz_t __gen_e_acsl__19;
- __e_acsl_mpz_t __gen_e_acsl_sub_10;
- int __gen_e_acsl_f3_5;
- __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n);
- __gmpz_init_set_si(__gen_e_acsl__19,1L);
- __gmpz_init(__gen_e_acsl_sub_10);
- __gmpz_sub(__gen_e_acsl_sub_10,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
- */
- __gen_e_acsl_f3_5 = __gen_e_acsl_f3_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
- __gen_e_acsl_if_7 = __gen_e_acsl_g_6 * __gen_e_acsl_f3_5 - 5;
- __gmpz_clear(__gen_e_acsl__19);
- __gmpz_clear(__gen_e_acsl_sub_10);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__20;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- int __gen_e_acsl_g_8;
- __gmpz_init_set_si(__gen_e_acsl__20,1L);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
- */
- __gen_e_acsl_g_8 = __gen_e_acsl_g_5((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
- __gen_e_acsl_if_7 = __gen_e_acsl_g_8;
- __gmpz_clear(__gen_e_acsl__20);
- __gmpz_clear(__gen_e_acsl_add_4);
- }
- __gmpz_clear(__gen_e_acsl__18);
- return __gen_e_acsl_if_7;
-}
-
-/*@ assigns \result;
- assigns \result \from n; */
-unsigned long __gen_e_acsl_f4_2(long n)
-{
- unsigned long __gen_e_acsl_if_13;
- if (n < 100L) {
- __e_acsl_mpz_t __gen_e_acsl_n_6;
- __e_acsl_mpz_t __gen_e_acsl__22;
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- unsigned long __gen_e_acsl_f4_6;
- __gmpz_init_set_si(__gen_e_acsl_n_6,n);
- __gmpz_init_set_si(__gen_e_acsl__22,1L);
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
- */
- __gen_e_acsl_f4_6 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
- __gen_e_acsl_if_13 = __gen_e_acsl_f4_6;
- __gmpz_clear(__gen_e_acsl_n_6);
- __gmpz_clear(__gen_e_acsl__22);
- __gmpz_clear(__gen_e_acsl_add_6);
- }
- else {
- unsigned long __gen_e_acsl_if_12;
- if (n < 9223372036854775807L) __gen_e_acsl_if_12 = 9223372036854775807UL;
- else __gen_e_acsl_if_12 = 6UL;
- __gen_e_acsl_if_13 = __gen_e_acsl_if_12;
+ int __gen_e_acsl_g_4;
+ __gen_e_acsl_g_4 = __gen_e_acsl_g_3(n + 1);
+ __gen_e_acsl_if_3 = __gen_e_acsl_g_4;
}
- return __gen_e_acsl_if_13;
+ return __gen_e_acsl_if_3;
}
/*@ assigns \result;
assigns \result \from n; */
unsigned long __gen_e_acsl_f4(int n)
{
- unsigned long __gen_e_acsl_if_15;
+ unsigned long __gen_e_acsl_if_5;
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;
+ unsigned long __gen_e_acsl_f4_3;
+ __gen_e_acsl_f4_3 = __gen_e_acsl_f4(n + 1);
+ __gen_e_acsl_if_5 = __gen_e_acsl_f4_3;
}
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;
+ unsigned long __gen_e_acsl_if_4;
+ if ((unsigned long)n < 9223372036854775807UL) __gen_e_acsl_if_4 = 9223372036854775807UL;
+ else __gen_e_acsl_if_4 = 6UL;
+ __gen_e_acsl_if_5 = __gen_e_acsl_if_4;
}
- 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)
-{
- __e_acsl_mpz_t __gen_e_acsl__23;
- int __gen_e_acsl_lt_2;
- unsigned long __gen_e_acsl_if_11;
- __gmpz_init_set_si(__gen_e_acsl__23,100L);
- __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
- if (__gen_e_acsl_lt_2 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__24;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- unsigned long __gen_e_acsl_f4_5;
- __gmpz_init_set_si(__gen_e_acsl__24,1L);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
- */
- __gen_e_acsl_f4_5 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
- __gen_e_acsl_if_11 = __gen_e_acsl_f4_5;
- __gmpz_clear(__gen_e_acsl__24);
- __gmpz_clear(__gen_e_acsl_add_7);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__25;
- int __gen_e_acsl_lt_3;
- unsigned long __gen_e_acsl_if_10;
- __gmpz_init_set_ui(__gen_e_acsl__25,9223372036854775807UL);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
- if (__gen_e_acsl_lt_3 < 0) __gen_e_acsl_if_10 = 9223372036854775807UL;
- else __gen_e_acsl_if_10 = 6UL;
- __gen_e_acsl_if_11 = __gen_e_acsl_if_10;
- __gmpz_clear(__gen_e_acsl__25);
- }
- __gmpz_clear(__gen_e_acsl__23);
- return __gen_e_acsl_if_11;
+ return __gen_e_acsl_if_5;
}
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
-void __gen_e_acsl_f5_2(__e_acsl_mpz_t *__retres_arg, long n)
+void __gen_e_acsl_f5_5(__e_acsl_mpz_t *__retres_arg, long n)
{
- __e_acsl_mpz_t __gen_e_acsl_if_17;
+ __e_acsl_mpz_t __gen_e_acsl_if_7;
if (n >= 0L) {
- __e_acsl_mpz_t __gen_e_acsl__27;
- __gmpz_init_set_si(__gen_e_acsl__27,0L);
- __gmpz_init_set(__gen_e_acsl_if_17,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
- __gmpz_clear(__gen_e_acsl__27);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_7;
- __e_acsl_mpz_t __gen_e_acsl__28;
- __e_acsl_mpz_t __gen_e_acsl_add_8;
- __e_acsl_mpz_t __gen_e_acsl_f5_6;
- __e_acsl_mpz_t __gen_e_acsl_add_11;
- __gmpz_init_set_si(__gen_e_acsl_n_7,n);
- __gmpz_init_set_si(__gen_e_acsl__28,1L);
- __gmpz_init(__gen_e_acsl_add_8);
- __gmpz_add(__gen_e_acsl_add_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
- __gen_e_acsl_f5_3(& __gen_e_acsl_f5_6,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_8);
- __gmpz_init(__gen_e_acsl_add_11);
- __gmpz_add(__gen_e_acsl_add_11,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7));
- __gmpz_init_set(__gen_e_acsl_if_17,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_11));
- __gmpz_clear(__gen_e_acsl_n_7);
- __gmpz_clear(__gen_e_acsl__28);
- __gmpz_clear(__gen_e_acsl_add_8);
- __gmpz_clear(__gen_e_acsl_f5_6);
- __gmpz_clear(__gen_e_acsl_add_11);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_17));
- __gmpz_clear(__gen_e_acsl_if_17);
- 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);
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __gmpz_init_set_si(__gen_e_acsl__10,0L);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gmpz_clear(__gen_e_acsl__10);
}
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_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gen_e_acsl_f5_5(& __gen_e_acsl_f5_7,n + 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_4,n);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
(__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));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
__gmpz_clear(__gen_e_acsl_f5_7);
- __gmpz_clear(__gen_e_acsl_n_8);
- __gmpz_clear(__gen_e_acsl_add_12);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl_add_3);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_18));
- __gmpz_clear(__gen_e_acsl_if_18);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
+ __gmpz_clear(__gen_e_acsl_if_7);
return;
}
/*@ assigns (*__retres_arg)[0];
- assigns (*__retres_arg)[0] \from *((__e_acsl_mpz_struct *)n);
- */
-void __gen_e_acsl_f5_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+ 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__29;
- int __gen_e_acsl_ge;
- __e_acsl_mpz_t __gen_e_acsl_if_16;
- __gmpz_init_set_si(__gen_e_acsl__29,0L);
- __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
- if (__gen_e_acsl_ge >= 0) {
- __e_acsl_mpz_t __gen_e_acsl__30;
- __gmpz_init_set_si(__gen_e_acsl__30,0L);
- __gmpz_init_set(__gen_e_acsl_if_16,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
- __gmpz_clear(__gen_e_acsl__30);
+ __e_acsl_mpz_t __gen_e_acsl_if_6;
+ if (n >= 0) {
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __gmpz_clear(__gen_e_acsl__8);
}
else {
- __e_acsl_mpz_t __gen_e_acsl__31;
- __e_acsl_mpz_t __gen_e_acsl_add_9;
- __e_acsl_mpz_t __gen_e_acsl_f5_5;
- __e_acsl_mpz_t __gen_e_acsl_add_10;
- __gmpz_init_set_si(__gen_e_acsl__31,1L);
- __gmpz_init(__gen_e_acsl_add_9);
- __gmpz_add(__gen_e_acsl_add_9,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
- __gen_e_acsl_f5_3(& __gen_e_acsl_f5_5,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_9);
- __gmpz_init(__gen_e_acsl_add_10);
- __gmpz_add(__gen_e_acsl_add_10,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_5),
- (__e_acsl_mpz_struct const *)(n));
- __gmpz_init_set(__gen_e_acsl_if_16,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_10));
- __gmpz_clear(__gen_e_acsl__31);
- __gmpz_clear(__gen_e_acsl_add_9);
- __gmpz_clear(__gen_e_acsl_f5_5);
- __gmpz_clear(__gen_e_acsl_add_10);
+ __e_acsl_mpz_t __gen_e_acsl_f5_3;
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __gen_e_acsl_f5(& __gen_e_acsl_f5_3,n + 1);
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2));
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2));
+ __gmpz_clear(__gen_e_acsl_f5_3);
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_16));
- __gmpz_clear(__gen_e_acsl__29);
- __gmpz_clear(__gen_e_acsl_if_16);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
+ __gmpz_clear(__gen_e_acsl_if_6);
return;
}