diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 022f7f94c48a7b130f084747ea95af70a73102f8..6a8454d1f870128ebd5abfa85b2cc9a1daefc381 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -26,6 +26,7 @@ Plugin E-ACSL <next-release>
############################
- E-ACSL [2022-19-07] Improve typing precision of variables appearing in comparisons
+-* E-ACSL [2022-09-08] Fix typing of recursive predicates (frama-c/e-acsl#198)
-* 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 ff6fc08f5e8d05749968825aaf6463db4c5df880..ee5f4bee348d8bc186c54f7bd0c0534b4d9d0860 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml
@@ -420,6 +420,9 @@ module LF_env
let add li profile ival = LFProf.Hashtbl.add tbl (li,profile) ival
+ let add_pred li profile =
+ LFProf.Hashtbl.add tbl (li,profile) (Ival Ival.zero_or_one)
+
exception Recursive
let contain li = object
diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
index 9cafe69c93a70301e49ffe2d73ccf84a3d6120c4..a68b6880da6e645ae0fc22b2fbfc4ee87526fd19 100644
--- a/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
+++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.mli
@@ -105,14 +105,23 @@ end
(** Imperative environment to perform the fixpoint algorithm for recursive
functions *)
module LF_env : sig
+ (** find the currently inferred interval for a call to a logic function *)
val find : logic_info -> Profile.t -> ival
+ (** clear the table of intervals for logic function (to do between typing )
+ each logic function calls *)
val clear : unit -> unit
+ (** add an interval as the current one for a logic function call *)
val add : logic_info -> Profile.t -> ival -> unit
+ (** add 0..1 as the current interval for a predicate call *)
+ val add_pred : logic_info -> Profile.t -> unit
+
+ (** determine whether a logic function or predicate is recursive *)
val is_rec : logic_info -> bool
+ (** replace the current interval for a logic function call *)
val replace : logic_info -> Profile.t -> ival -> unit
end
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 833d84ed21d5755e1b3763d8da9ac37b62d9d232..f2937821bc68e16241c86164a9964f1a9e12c215 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -739,28 +739,36 @@ let rec infer ~force ~logic_env t =
(fun arg -> get_res (infer ~force ~logic_env arg))
args)
in
- (match li.l_body with
- | LBpred p ->
- let logic_env = Logic_env.make profile in
- ignore (infer_predicate ~logic_env p);
- Ival Ival.zero_or_one
- | LBterm t' when LF_env.is_rec li ->
- let widened_profile = widen_profile profile in
- Widened_profile.add profile li widened_profile;
- (try LF_env.find li widened_profile
- with Not_found ->
- fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
- | LBterm t' ->
- let logic_env = Logic_env.make profile in
- (* If the logic function returns a C type, then its application
- ranges inside this C type *)
- (match li.l_type with
- | Some (Ctype typ) ->
- ignore ((infer ~force ~logic_env t'));
- interv_of_typ typ;
- | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
- get_res (infer ~force ~logic_env t'))
- | _ -> assert false)
+ if LF_env.is_rec li then
+ let widened_profile = widen_profile profile in
+ Widened_profile.add profile li widened_profile;
+ (match li.l_body with
+ | LBpred p ->
+ LF_env.add_pred li widened_profile;
+ infer_predicate
+ ~logic_env:(Logic_env.make widened_profile) p;
+ Ival Ival.zero_or_one
+ | LBterm t' ->
+ (try LF_env.find li widened_profile
+ with Not_found ->
+ fixpoint ~infer li widened_profile t' (Ival Ival.bottom))
+ | _ -> assert false)
+ else
+ let logic_env = Logic_env.make profile in
+ (match li.l_body with
+ | LBpred p ->
+ ignore (infer_predicate ~logic_env p);
+ Ival Ival.zero_or_one
+ | LBterm t' ->
+ (* If the logic function returns a C type, then its application
+ ranges inside this C type *)
+ (match li.l_type with
+ | Some (Ctype typ) ->
+ ignore ((infer ~force ~logic_env t'));
+ interv_of_typ typ;
+ | None | Some (Linteger | Lreal | Ltype _ | Lvar _ | Larrow _) ->
+ get_res (infer ~force ~logic_env t'))
+ | _ -> assert false)
| LBnone when li.l_var_info.lv_name = "\\sum" ||
li.l_var_info.lv_name = "\\product" ->
(match args with
@@ -1011,15 +1019,22 @@ and infer_predicate ~logic_env p =
match p.pred_content with
| Pfalse | Ptrue -> ()
| Papp(li, _, args) ->
+ let profile =
+ Profile.make
+ li.l_profile
+ (List.map
+ (fun arg -> get_res (infer ~force:false ~logic_env arg))
+ args)
+ in
(match li.l_body with
+ | LBpred p when LF_env.is_rec li ->
+ let widened_profile = widen_profile profile in
+ Widened_profile.add profile li widened_profile;
+ (try ignore (LF_env.find li widened_profile)
+ with Not_found ->
+ LF_env.add_pred li widened_profile;
+ infer_predicate ~logic_env:(Logic_env.make widened_profile) p)
| LBpred p ->
- let profile =
- Profile.make
- li.l_profile
- (List.map
- (fun arg -> get_res (infer ~force:false ~logic_env arg))
- args)
- in
let logic_env = Logic_env.make profile in
ignore (infer_predicate ~logic_env p)
| LBnone -> ()
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 88a168eb010bc49502d7fa635c930a9e3f5092fa..a0c223cb540acb2432f3cbd39c65f3917e98066f 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -208,6 +208,19 @@ end = struct
end
+module Recursive_pred : sig
+ val add: Profile.t -> logic_info -> unit
+ val is_done: Profile.t -> logic_info -> bool
+end = struct
+ let known = ref LFProf.Set.empty
+
+ let add profile li =
+ known := LFProf.Set.add (li, profile) !known
+
+ let is_done profile li = LFProf.Set.mem (li, profile) !known
+
+end
+
(******************************************************************************)
(** {2 Coercion rules} *)
(******************************************************************************)
@@ -558,6 +571,7 @@ let rec type_term
li.l_profile
(List.map (Interval.get_from_profile ~profile) args)
in
+ let new_profile = Interval.get_widened_profile new_profile li in
Stack.push
(fun () ->
ignore (type_predicate ~profile:new_profile p))
@@ -776,7 +790,11 @@ and type_predicate ~profile p =
li.l_profile
(List.map (Interval.get_from_profile ~profile) args)
in
- type_predicate ~profile:new_profile p;
+ let new_profile = Interval.get_widened_profile new_profile li in
+ if not (Recursive_pred.is_done new_profile li)
+ then
+ (Recursive_pred.add new_profile li;
+ ignore (type_predicate ~profile:new_profile p))
| LBnone -> ()
| LBreads _ -> ()
| LBinductive _ -> ()
diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index 8e39fbc3c6bcb44024412eb1d4c7cb59386a0a5f..e4908775642fe3d3693adbd84352b3e1d5eef3df 100644
--- a/src/plugins/e-acsl/tests/arith/functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/functions_rec.c
@@ -6,6 +6,18 @@
STDOPT: +"-eva-unroll-recursive-calls 100"
*/
+/*@ predicate even (integer n) =
+ n == 0 ? \true :
+ n > 0 ? ! even (n - 1) :
+ ! even (n + 1);
+*/
+
+/*@ predicate even_and_not_negative (integer n) =
+ n == 0 ? \true :
+ n > 0 ? ! even (n - 1) :
+ \false;
+*/
+
/*@ logic integer f1(integer n) =
n <= 0 ? 0 : f1(n - 1) + n; */
@@ -25,9 +37,12 @@
n >= 0 ? 0 : f5(n + 1) + n; */
int main(void) {
+ /*@ assert even(10); @*/;
+ /*@ assert even(-6); @*/;
+ /*@ assert even_and_not_negative(10); */;
/*@ assert f1(0) == 0; */;
/*@ assert f1(1) == 1; */;
- /*@ assert f1(100) == 5050; */;
+ /*@ assert f1(10) == 55; */;
/*@ assert f2(7) == 1; */;
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 d064060bb6adc24506499219f6f10a0afa5ffc35..6332bd48d4b8d961b978cbf1ee83e7f3f568e931 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
@@ -1,32 +1,61 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] functions_rec.c:28: Warning:
+[eva:alarm] functions_rec.c:11: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+[eva:alarm] functions_rec.c:11: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+[eva] functions_rec.c:11: Warning:
+ Using specification of function __gen_e_acsl_even_3 for recursive calls.
+ Analysis of function __gen_e_acsl_even_3 is thus incomplete and its soundness
+ relies on the written specification.
+[eva:alarm] functions_rec.c:12: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
+[eva] functions_rec.c:12: Warning:
+ Using specification of function __gen_e_acsl_even_3 for recursive calls.
+ Analysis of function __gen_e_acsl_even_3 is thus incomplete and its soundness
+ relies on the written specification.
+[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.
+[eva:alarm] functions_rec.c:12: Warning:
+ accessing uninitialized left-value.
+ assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+[eva:alarm] functions_rec.c:41: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] functions_rec.c:41: Warning: assertion got status unknown.
+[eva:alarm] functions_rec.c:42: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] functions_rec.c:42: Warning: assertion got status unknown.
+[eva:alarm] functions_rec.c:43: 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:
+[eva:alarm] functions_rec.c:43: Warning: assertion got status unknown.
+[eva] functions_rec.c:22: 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:
+[eva:alarm] functions_rec.c:44: 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:30: Warning:
+[eva:alarm] functions_rec.c:44: Warning: assertion got status unknown.
+[eva:alarm] functions_rec.c:45: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:30: Warning: assertion got status unknown.
-[eva] functions_rec.c:13: Warning:
+[eva:alarm] functions_rec.c:45: Warning: assertion got status unknown.
+[eva] functions_rec.c:25: Warning:
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] functions_rec.c:13: Warning:
+[eva] functions_rec.c:25: Warning:
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] functions_rec.c:13: Warning:
+[eva] functions_rec.c:25: Warning:
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:
+[eva:alarm] functions_rec.c:25: Warning: assertion 'E_ACSL' got status unknown.
+[eva:alarm] functions_rec.c:25: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:13: Warning:
+[eva:alarm] functions_rec.c:25: Warning:
accessing uninitialized left-value. assert \initialized(&n);
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 95fb94d1c880ce5ac7c7313803b6647c83428c95..7c2bcabacd397e0c75e4c589de4872c23e20b9ff 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
@@ -8,6 +8,23 @@
#include "time.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+/*@
+predicate even(integer n) =
+ n == 0? \true: (n > 0? !even(n - 1): !even(n + 1));
+
+*/
+int __gen_e_acsl_even_2(long n);
+
+int __gen_e_acsl_even(int n);
+
+int __gen_e_acsl_even_3(__e_acsl_mpz_struct * n);
+
+/*@
+predicate even_and_not_negative(integer n) =
+ n == 0? \true: (n > 0? !even(n - 1): \false);
+ */
+int __gen_e_acsl_even_and_not_negative(int n);
+
/*@ 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);
@@ -45,188 +62,242 @@ int main(void)
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
{
- __e_acsl_mpz_t __gen_e_acsl_f1_4;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_eq;
+ int __gen_e_acsl_even_14;
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __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_4));
+ __gen_e_acsl_even_14 = __gen_e_acsl_even(10);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"even(10)",0,
+ __gen_e_acsl_even_14);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
- __gen_e_acsl_assert_data.pred_txt = "f1(0) == 0";
+ __gen_e_acsl_assert_data.pred_txt = "even(10)";
__gen_e_acsl_assert_data.file = "functions_rec.c";
__gen_e_acsl_assert_data.fct = "main";
- __gen_e_acsl_assert_data.line = 28;
- __e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data);
+ __gen_e_acsl_assert_data.line = 40;
+ __e_acsl_assert(__gen_e_acsl_even_14,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- __gmpz_clear(__gen_e_acsl_f1_4);
- __gmpz_clear(__gen_e_acsl__2);
}
- /*@ assert f1(0) == 0; */ ;
+ /*@ assert even(10); */ ;
{
- __e_acsl_mpz_t __gen_e_acsl_f1_6;
- __e_acsl_mpz_t __gen_e_acsl__3;
- int __gen_e_acsl_eq_2;
+ int __gen_e_acsl_even_16;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __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_6));
+ __gen_e_acsl_even_16 = __gen_e_acsl_even(-6);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,"even(-6)",0,
+ __gen_e_acsl_even_16);
__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";
+ __gen_e_acsl_assert_data_2.pred_txt = "even(-6)";
__gen_e_acsl_assert_data_2.file = "functions_rec.c";
__gen_e_acsl_assert_data_2.fct = "main";
- __gen_e_acsl_assert_data_2.line = 29;
- __e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_2);
+ __gen_e_acsl_assert_data_2.line = 41;
+ __e_acsl_assert(__gen_e_acsl_even_16,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- __gmpz_clear(__gen_e_acsl_f1_6);
- __gmpz_clear(__gen_e_acsl__3);
}
- /*@ assert f1(1) == 1; */ ;
+ /*@ assert even(-6); */ ;
{
- __e_acsl_mpz_t __gen_e_acsl_f1_8;
- __e_acsl_mpz_t __gen_e_acsl__4;
- int __gen_e_acsl_eq_3;
+ int __gen_e_acsl_even_and_not_negative_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __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_8));
+ __gen_e_acsl_even_and_not_negative_2 = __gen_e_acsl_even_and_not_negative
+ (10);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
+ "even_and_not_negative(10)",0,
+ __gen_e_acsl_even_and_not_negative_2);
__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";
+ __gen_e_acsl_assert_data_3.pred_txt = "even_and_not_negative(10)";
__gen_e_acsl_assert_data_3.file = "functions_rec.c";
__gen_e_acsl_assert_data_3.fct = "main";
- __gen_e_acsl_assert_data_3.line = 30;
- __e_acsl_assert(__gen_e_acsl_eq_3 == 0,& __gen_e_acsl_assert_data_3);
+ __gen_e_acsl_assert_data_3.line = 42;
+ __e_acsl_assert(__gen_e_acsl_even_and_not_negative_2,
+ & __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
- __gmpz_clear(__gen_e_acsl_f1_8);
- __gmpz_clear(__gen_e_acsl__4);
}
- /*@ assert f1(100) == 5050; */ ;
+ /*@ assert even_and_not_negative(10); */ ;
{
- __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_mpz_t __gen_e_acsl_f1_4;
+ __e_acsl_mpz_t __gen_e_acsl__8;
+ int __gen_e_acsl_eq_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_4 =
{.values = (void *)0};
- __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_f1(& __gen_e_acsl_f1_4,0);
+ __gmpz_init_set_si(__gen_e_acsl__8,0L);
+ __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_4,"f1(0)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_4));
__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.pred_txt = "f1(0) == 0";
__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_eq_4 == 0,& __gen_e_acsl_assert_data_4);
+ __gen_e_acsl_assert_data_4.line = 43;
+ __e_acsl_assert(__gen_e_acsl_eq_2 == 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);
+ __gmpz_clear(__gen_e_acsl_f1_4);
+ __gmpz_clear(__gen_e_acsl__8);
}
- /*@ assert f2(7) == 1; */ ;
+ /*@ assert f1(0) == 0; */ ;
{
- int __gen_e_acsl_f3_4;
+ __e_acsl_mpz_t __gen_e_acsl_f1_6;
+ __e_acsl_mpz_t __gen_e_acsl__9;
+ int __gen_e_acsl_eq_3;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_5 =
+ {.values = (void *)0};
+ __gen_e_acsl_f1(& __gen_e_acsl_f1_6,1);
+ __gmpz_init_set_si(__gen_e_acsl__9,1L);
+ __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_5,"f1(1)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_6));
+ __gen_e_acsl_assert_data_5.blocking = 1;
+ __gen_e_acsl_assert_data_5.kind = "Assertion";
+ __gen_e_acsl_assert_data_5.pred_txt = "f1(1) == 1";
+ __gen_e_acsl_assert_data_5.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_5.fct = "main";
+ __gen_e_acsl_assert_data_5.line = 44;
+ __e_acsl_assert(__gen_e_acsl_eq_3 == 0,& __gen_e_acsl_assert_data_5);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
+ __gmpz_clear(__gen_e_acsl_f1_6);
+ __gmpz_clear(__gen_e_acsl__9);
+ }
+ /*@ assert f1(1) == 1; */ ;
+ {
+ __e_acsl_mpz_t __gen_e_acsl_f1_8;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ int __gen_e_acsl_eq_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_f1(& __gen_e_acsl_f1_8,10);
+ __gmpz_init_set_si(__gen_e_acsl__10,55L);
+ __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_6,"f1(10)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8));
__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.pred_txt = "f1(10) == 55";
__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);
+ __gen_e_acsl_assert_data_6.line = 45;
+ __e_acsl_assert(__gen_e_acsl_eq_4 == 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
+ __gmpz_clear(__gen_e_acsl_f1_8);
+ __gmpz_clear(__gen_e_acsl__10);
}
- /*@ assert f3(6) == -5; */ ;
+ /*@ assert f1(10) == 55; */ ;
{
- unsigned long __gen_e_acsl_f4_4;
+ __e_acsl_mpz_t __gen_e_acsl_f2_8;
+ __e_acsl_mpz_t __gen_e_acsl__13;
+ int __gen_e_acsl_eq_5;
__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_f2(& __gen_e_acsl_f2_8,7);
+ __gmpz_init_set_si(__gen_e_acsl__13,1L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ /*@ assert Eva: initialization: \initialized(&n); */
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,"n",0,n);
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_8,"f2(n - 3)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_7));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_7,"f2(7)",0,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_8));
__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.pred_txt = "f2(7) == 1";
__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);
+ __gen_e_acsl_assert_data_7.line = 47;
+ __e_acsl_assert(__gen_e_acsl_eq_5 == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
+ __gmpz_clear(__gen_e_acsl_f2_8);
+ __gmpz_clear(__gen_e_acsl__13);
+ }
+ /*@ assert f2(7) == 1; */ ;
+ {
+ int __gen_e_acsl_f3_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_9 =
+ {.values = (void *)0};
+ __gen_e_acsl_f3_4 = __gen_e_acsl_f3(6);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,"f3(6)",0,
+ __gen_e_acsl_f3_4);
+ __gen_e_acsl_assert_data_9.blocking = 1;
+ __gen_e_acsl_assert_data_9.kind = "Assertion";
+ __gen_e_acsl_assert_data_9.pred_txt = "f3(6) == -5";
+ __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 = 49;
+ __e_acsl_assert(__gen_e_acsl_f3_4 == -5,& __gen_e_acsl_assert_data_9);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
+ }
+ /*@ assert f3(6) == -5; */ ;
+ {
+ unsigned long __gen_e_acsl_f4_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_10 =
+ {.values = (void *)0};
+ __gen_e_acsl_f4_4 = __gen_e_acsl_f4(9);
+ __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_10,"f4(9)",0,
+ __gen_e_acsl_f4_4);
+ __gen_e_acsl_assert_data_10.blocking = 1;
+ __gen_e_acsl_assert_data_10.kind = "Assertion";
+ __gen_e_acsl_assert_data_10.pred_txt = "f4(9) > 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 = 51;
+ __e_acsl_assert(__gen_e_acsl_f4_4 > 0UL,& __gen_e_acsl_assert_data_10);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
}
/*@ 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 =
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ int __gen_e_acsl_eq_6;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
__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,
+ __gmpz_init_set_si(__gen_e_acsl__15,0L);
+ __gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_11,"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 = "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 = 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);
+ __gen_e_acsl_assert_data_11.blocking = 1;
+ __gen_e_acsl_assert_data_11.kind = "Assertion";
+ __gen_e_acsl_assert_data_11.pred_txt = "f5(0) == 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 = 53;
+ __e_acsl_assert(__gen_e_acsl_eq_6 == 0,& __gen_e_acsl_assert_data_11);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
__gmpz_clear(__gen_e_acsl_f5_4);
- __gmpz_clear(__gen_e_acsl__9);
+ __gmpz_clear(__gen_e_acsl__15);
}
/*@ assert f5(0) == 0; */ ;
{
- long __gen_e_acsl_n_3;
+ long __gen_e_acsl_n_5;
__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 =
+ __e_acsl_mpz_t __gen_e_acsl__17;
+ int __gen_e_acsl_eq_7;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
- __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,
+ __gen_e_acsl_n_5 = 9223372036854775807L;
+ __gen_e_acsl_f5_5(& __gen_e_acsl_f5_8,__gen_e_acsl_n_5);
+ __gmpz_init_set_si(__gen_e_acsl__17,0L);
+ __gen_e_acsl_eq_7 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__17));
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_12,"n",0,
+ __gen_e_acsl_n_5);
+ __e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_12,"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 = "\\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 = 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);
+ __gen_e_acsl_assert_data_12.blocking = 1;
+ __gen_e_acsl_assert_data_12.kind = "Assertion";
+ __gen_e_acsl_assert_data_12.pred_txt = "\\let n = 0 == 0? 0x7fffffffffffffffL: -1; f5(n) == 0";
+ __gen_e_acsl_assert_data_12.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_12.fct = "main";
+ __gen_e_acsl_assert_data_12.line = 55;
+ __e_acsl_assert(__gen_e_acsl_eq_7 == 0,& __gen_e_acsl_assert_data_12);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
__gmpz_clear(__gen_e_acsl_f5_8);
- __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl__17);
}
/*@ assert \let n = 0 == 0? 0x7fffffffffffffffL: -1; f5(n) == 0; */ ;
__retres = 0;
@@ -234,37 +305,193 @@ int main(void)
return __retres;
}
+/*@ assigns \result;
+ assigns \result \from n; */
+int __gen_e_acsl_even_2(long n)
+{
+ int __gen_e_acsl_if_4;
+ if (n == 0L) __gen_e_acsl_if_4 = 1;
+ else {
+ int __gen_e_acsl_if_3;
+ if (n > 0L) {
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ int __gen_e_acsl_even_8;
+ __gmpz_init_set_si(__gen_e_acsl_n,n);
+ __gmpz_init_set_si(__gen_e_acsl_,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_));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ */
+ __gen_e_acsl_even_8 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ __gen_e_acsl_if_3 = ! __gen_e_acsl_even_8;
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_sub);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl__6;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ int __gen_e_acsl_even_10;
+ __gmpz_init_set_si(__gen_e_acsl_n_2,n);
+ __gmpz_init_set_si(__gen_e_acsl__6,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+ */
+ __gen_e_acsl_even_10 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+ __gen_e_acsl_if_3 = ! __gen_e_acsl_even_10;
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl__6);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ }
+ __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
+ }
+ return __gen_e_acsl_if_4;
+}
+
+/*@ assigns \result;
+ assigns \result \from n; */
+int __gen_e_acsl_even(int n)
+{
+ int __gen_e_acsl_if_6;
+ if (n == 0) __gen_e_acsl_if_6 = 1;
+ else {
+ int __gen_e_acsl_if_5;
+ if (n > 0) {
+ int __gen_e_acsl_even_11;
+ __gen_e_acsl_even_11 = __gen_e_acsl_even_2(n - 1L);
+ __gen_e_acsl_if_5 = ! __gen_e_acsl_even_11;
+ }
+ else {
+ int __gen_e_acsl_even_13;
+ __gen_e_acsl_even_13 = __gen_e_acsl_even_2(n + 1L);
+ __gen_e_acsl_if_5 = ! __gen_e_acsl_even_13;
+ }
+ __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+/*@ assigns \result;
+ assigns \result \from *((__e_acsl_mpz_struct *)n); */
+int __gen_e_acsl_even_3(__e_acsl_mpz_struct * n)
+{
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_eq;
+ int __gen_e_acsl_if_2;
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ if (__gen_e_acsl_eq == 0) __gen_e_acsl_if_2 = 1;
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ int __gen_e_acsl_gt;
+ int __gen_e_acsl_if;
+ __gmpz_init_set_si(__gen_e_acsl__3,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+ if (__gen_e_acsl_gt > 0) {
+ __e_acsl_mpz_t __gen_e_acsl__4;
+ __e_acsl_mpz_t __gen_e_acsl_sub_2;
+ int __gen_e_acsl_even_5;
+ __gmpz_init_set_si(__gen_e_acsl__4,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__4));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ */
+ __gen_e_acsl_even_5 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
+ __gen_e_acsl_if = ! __gen_e_acsl_even_5;
+ __gmpz_clear(__gen_e_acsl__4);
+ __gmpz_clear(__gen_e_acsl_sub_2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__5;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ int __gen_e_acsl_even_7;
+ __gmpz_init_set_si(__gen_e_acsl__5,1L);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
+ */
+ __gen_e_acsl_even_7 = __gen_e_acsl_even_3((__e_acsl_mpz_struct *)__gen_e_acsl_add);
+ __gen_e_acsl_if = ! __gen_e_acsl_even_7;
+ __gmpz_clear(__gen_e_acsl__5);
+ __gmpz_clear(__gen_e_acsl_add);
+ }
+ __gen_e_acsl_if_2 = __gen_e_acsl_if;
+ __gmpz_clear(__gen_e_acsl__3);
+ }
+ __gmpz_clear(__gen_e_acsl__2);
+ return __gen_e_acsl_if_2;
+}
+
+/*@ assigns \result;
+ assigns \result \from n; */
+int __gen_e_acsl_even_and_not_negative(int n)
+{
+ int __gen_e_acsl_if_8;
+ if (n == 0) __gen_e_acsl_if_8 = 1;
+ else {
+ int __gen_e_acsl_if_7;
+ if (n > 0) {
+ int __gen_e_acsl_even_18;
+ __gen_e_acsl_even_18 = __gen_e_acsl_even(n - 1);
+ __gen_e_acsl_if_7 = ! __gen_e_acsl_even_18;
+ }
+ else __gen_e_acsl_if_7 = 0;
+ __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ }
+ return __gen_e_acsl_if_8;
+}
+
/*@ 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;
+ __e_acsl_mpz_t __gen_e_acsl_if_9;
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,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_clear(__gen_e_acsl_);
+ __e_acsl_mpz_t __gen_e_acsl__7;
+ __gmpz_init_set_si(__gen_e_acsl__7,0L);
+ __gmpz_init_set(__gen_e_acsl_if_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+ __gmpz_clear(__gen_e_acsl__7);
}
else {
__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;
+ __e_acsl_mpz_t __gen_e_acsl_n_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
__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,
+ __gmpz_init_set_si(__gen_e_acsl_n_3,(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_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));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3));
+ __gmpz_init_set(__gen_e_acsl_if_9,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
__gmpz_clear(__gen_e_acsl_f1_3);
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_n_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
- __gmpz_clear(__gen_e_acsl_if);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_9));
+ __gmpz_clear(__gen_e_acsl_if_9);
return;
}
@@ -272,20 +499,20 @@ void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
{
- __e_acsl_mpz_t __gen_e_acsl_if_2;
+ __e_acsl_mpz_t __gen_e_acsl_if_10;
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);
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __gmpz_init_set_si(__gen_e_acsl__11,1L);
+ __gmpz_init_set(__gen_e_acsl_if_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_clear(__gen_e_acsl__11);
}
else {
__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;
+ __e_acsl_mpz_t __gen_e_acsl__12;
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);
@@ -294,40 +521,40 @@ void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
__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 =
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_8 =
{.values = (void *)0};
__gen_e_acsl_f2(& __gen_e_acsl_f2_7,n - 3);
- __gmpz_init_set_si(__gen_e_acsl__6,0L);
+ __gmpz_init_set_si(__gen_e_acsl__12,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));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
__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;
+ __gen_e_acsl_assert_data_8.blocking = 1;
+ __gen_e_acsl_assert_data_8.kind = "Assertion";
+ __gen_e_acsl_assert_data_8.pred_txt = "f2(n - 3) != 0";
+ __gen_e_acsl_assert_data_8.file = "functions_rec.c";
+ __gen_e_acsl_assert_data_8.fct = "f2";
+ __gen_e_acsl_assert_data_8.line = 25;
__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);
+ & __gen_e_acsl_assert_data_8);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
}
__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,
+ __gmpz_init_set(__gen_e_acsl_if_10,
(__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__12);
__gmpz_clear(__gen_e_acsl_div);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gmpz_clear(__gen_e_acsl_if_2);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_10));
+ __gmpz_clear(__gen_e_acsl_if_10);
return;
}
@@ -351,72 +578,72 @@ int __gen_e_acsl_g(unsigned int n)
assigns \result \from n; */
int __gen_e_acsl_f3(int n)
{
- int __gen_e_acsl_if_3;
+ int __gen_e_acsl_if_11;
if (n > 0) {
int __gen_e_acsl_g_2;
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;
+ __gen_e_acsl_if_11 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_3 - 5;
}
else {
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;
+ __gen_e_acsl_if_11 = __gen_e_acsl_g_4;
}
- return __gen_e_acsl_if_3;
+ return __gen_e_acsl_if_11;
}
/*@ assigns \result;
assigns \result \from n; */
unsigned long __gen_e_acsl_f4(int n)
{
- unsigned long __gen_e_acsl_if_5;
+ unsigned long __gen_e_acsl_if_13;
if (n < 100) {
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;
+ __gen_e_acsl_if_13 = __gen_e_acsl_f4_3;
}
else {
- 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;
+ unsigned long __gen_e_acsl_if_12;
+ if ((unsigned long)n < 9223372036854775807UL) __gen_e_acsl_if_12 = 9223372036854775807UL;
+ else __gen_e_acsl_if_12 = 6UL;
+ __gen_e_acsl_if_13 = __gen_e_acsl_if_12;
}
- return __gen_e_acsl_if_5;
+ return __gen_e_acsl_if_13;
}
/*@ assigns (*__retres_arg)[0];
assigns (*__retres_arg)[0] \from n; */
void __gen_e_acsl_f5_5(__e_acsl_mpz_t *__retres_arg, long n)
{
- __e_acsl_mpz_t __gen_e_acsl_if_7;
+ __e_acsl_mpz_t __gen_e_acsl_if_15;
if (n >= 0L) {
- __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);
+ __e_acsl_mpz_t __gen_e_acsl__16;
+ __gmpz_init_set_si(__gen_e_acsl__16,0L);
+ __gmpz_init_set(__gen_e_acsl_if_15,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__16));
+ __gmpz_clear(__gen_e_acsl__16);
}
else {
__e_acsl_mpz_t __gen_e_acsl_f5_7;
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl_n_6;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
__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,
+ __gmpz_init_set_si(__gen_e_acsl_n_6,n);
+ __gmpz_init(__gen_e_acsl_add_5);
+ __gmpz_add(__gen_e_acsl_add_5,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_7),
- (__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));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6));
+ __gmpz_init_set(__gen_e_acsl_if_15,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
__gmpz_clear(__gen_e_acsl_f5_7);
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl_n_6);
+ __gmpz_clear(__gen_e_acsl_add_5);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
- __gmpz_clear(__gen_e_acsl_if_7);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_15));
+ __gmpz_clear(__gen_e_acsl_if_15);
return;
}
@@ -424,33 +651,33 @@ void __gen_e_acsl_f5_5(__e_acsl_mpz_t *__retres_arg, long 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_if_6;
+ __e_acsl_mpz_t __gen_e_acsl_if_14;
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);
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ __gmpz_init_set_si(__gen_e_acsl__14,0L);
+ __gmpz_init_set(__gen_e_acsl_if_14,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ __gmpz_clear(__gen_e_acsl__14);
}
else {
__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;
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
__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,
+ __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,
(__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));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
+ __gmpz_init_set(__gen_e_acsl_if_14,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
__gmpz_clear(__gen_e_acsl_f5_3);
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl_add_4);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
- __gmpz_clear(__gen_e_acsl_if_6);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_14));
+ __gmpz_clear(__gen_e_acsl_if_14);
return;
}