Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
f00d8524
Commit
f00d8524
authored
Apr 01, 2019
by
Julien Signoles
Browse files
[tests] update oracles because of the new hash function
parent
bcf4c0dd
Changes
4
Hide whitespace changes
Inline
Side-by-side
src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
View file @
f00d8524
...
...
@@ -15,25 +15,25 @@ int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
*/
int
__gen_e_acsl_p2
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
);
int
__gen_e_acsl_p2_3
(
int
__gen_e_acsl_x_arg
,
long
__gen_e_acsl_y_arg
);
int
__gen_e_acsl_p2
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
);
int
__gen_e_acsl_p2_2
(
int
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
);
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
);
long
__gen_e_acsl_f1
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
);
void
__gen_e_acsl_f1_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
);
long
__gen_e_acsl_f1
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
);
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
);
/*@ logic char h_char(char c) = c;
*/
...
...
@@ -283,11 +283,27 @@ char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg)
return
__retres
;
}
long
__gen_e_acsl_f1
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
)
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
)
{
long
__retres
;
__retres
=
__gen_e_acsl_x_arg
+
(
long
)
__gen_e_acsl_y_arg
;
return
__retres
;
__e_acsl_mpz_t
__gen_e_acsl_x_4
;
__e_acsl_mpz_t
__gen_e_acsl_y_4
;
__e_acsl_mpz_t
__gen_e_acsl_add_4
;
__gmpz_init_set
(
__gen_e_acsl_x_4
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_arg
));
__gmpz_init_set
(
__gen_e_acsl_y_4
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_arg
));
__gmpz_init
(
__gen_e_acsl_add_4
);
__gmpz_add
(
__gen_e_acsl_add_4
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_4
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_4
));
__gmpz_init_set
(
__retres_arg
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_4
));
__gmpz_clear
(
__gen_e_acsl_x_4
);
__gmpz_clear
(
__gen_e_acsl_y_4
);
__gmpz_clear
(
__gen_e_acsl_add_4
);
return
;
}
void
__gen_e_acsl_f1_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
...
...
@@ -312,27 +328,11 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
return
;
}
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
)
long
__gen_e_acsl_f1
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
)
{
__e_acsl_mpz_t
__gen_e_acsl_x_4
;
__e_acsl_mpz_t
__gen_e_acsl_y_4
;
__e_acsl_mpz_t
__gen_e_acsl_add_4
;
__gmpz_init_set
(
__gen_e_acsl_x_4
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_arg
));
__gmpz_init_set
(
__gen_e_acsl_y_4
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_arg
));
__gmpz_init
(
__gen_e_acsl_add_4
);
__gmpz_add
(
__gen_e_acsl_add_4
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_4
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_4
));
__gmpz_init_set
(
__retres_arg
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_4
));
__gmpz_clear
(
__gen_e_acsl_x_4
);
__gmpz_clear
(
__gen_e_acsl_y_4
);
__gmpz_clear
(
__gen_e_acsl_add_4
);
return
;
long
__retres
;
__retres
=
__gen_e_acsl_x_arg
+
(
long
)
__gen_e_acsl_y_arg
;
return
__retres
;
}
int
__gen_e_acsl_p2_2
(
int
__gen_e_acsl_x_arg
,
...
...
@@ -361,6 +361,13 @@ int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
return
__retres
;
}
int
__gen_e_acsl_p2
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
)
{
int
__retres
;
__retres
=
__gen_e_acsl_x_arg
+
(
long
)
__gen_e_acsl_y_arg
>
0L
;
return
__retres
;
}
int
__gen_e_acsl_p2_3
(
int
__gen_e_acsl_x_arg
,
long
__gen_e_acsl_y_arg
)
{
int
__retres
;
...
...
@@ -386,13 +393,6 @@ int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg)
return
__retres
;
}
int
__gen_e_acsl_p2
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
)
{
int
__retres
;
__retres
=
__gen_e_acsl_x_arg
+
(
long
)
__gen_e_acsl_y_arg
>
0L
;
return
__retres
;
}
int
__gen_e_acsl_p1
(
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
)
{
int
__retres
;
...
...
src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
View file @
f00d8524
...
...
@@ -23,10 +23,6 @@ int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
);
void
__gen_e_acsl_f1
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_x_arg
,
int
__gen_e_acsl_y_arg
);
...
...
@@ -34,6 +30,10 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
int
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
);
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
);
/*@ logic char h_char(char c) = c;
*/
char
__gen_e_acsl_h_char
(
int
__gen_e_acsl_c_arg
);
...
...
@@ -352,6 +352,29 @@ char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg)
return
__retres
;
}
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
)
{
__e_acsl_mpz_t
__gen_e_acsl_x_6
;
__e_acsl_mpz_t
__gen_e_acsl_y_6
;
__e_acsl_mpz_t
__gen_e_acsl_add_6
;
__gmpz_init_set
(
__gen_e_acsl_x_6
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_arg
));
__gmpz_init_set
(
__gen_e_acsl_y_6
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_arg
));
__gmpz_init
(
__gen_e_acsl_add_6
);
__gmpz_add
(
__gen_e_acsl_add_6
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_6
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_6
));
__gmpz_init_set
(
__retres_arg
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_6
));
__gmpz_clear
(
__gen_e_acsl_x_6
);
__gmpz_clear
(
__gen_e_acsl_y_6
);
__gmpz_clear
(
__gen_e_acsl_add_6
);
return
;
}
void
__gen_e_acsl_f1_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
)
...
...
@@ -394,29 +417,6 @@ void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
return
;
}
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
)
{
__e_acsl_mpz_t
__gen_e_acsl_x_6
;
__e_acsl_mpz_t
__gen_e_acsl_y_6
;
__e_acsl_mpz_t
__gen_e_acsl_add_6
;
__gmpz_init_set
(
__gen_e_acsl_x_6
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_arg
));
__gmpz_init_set
(
__gen_e_acsl_y_6
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_arg
));
__gmpz_init
(
__gen_e_acsl_add_6
);
__gmpz_add
(
__gen_e_acsl_add_6
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_x_6
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_y_6
));
__gmpz_init_set
(
__retres_arg
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_6
));
__gmpz_clear
(
__gen_e_acsl_x_6
);
__gmpz_clear
(
__gen_e_acsl_y_6
);
__gmpz_clear
(
__gen_e_acsl_add_6
);
return
;
}
int
__gen_e_acsl_p2_2
(
int
__gen_e_acsl_x_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_y_arg
)
{
...
...
src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
View file @
f00d8524
...
...
@@ -4,40 +4,40 @@
/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
*/
void
__gen_e_acsl_f1
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_n_arg
);
void
__gen_e_acsl_f1_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
long
__gen_e_acsl_n_arg
);
void
__gen_e_acsl_f1
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_n_arg
);
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
);
/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
int
__gen_e_acsl_f2
(
int
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_f2_2
(
long
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_f2
(
int
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_f2_3
(
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
);
/*@ logic ℤ g(ℤ n) = 0;
*/
int
__gen_e_acsl_g
(
int
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_g_2
(
long
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_g
(
int
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_g_3
(
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
);
/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
*/
int
__gen_e_acsl_f3
(
int
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_f3_2
(
long
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_f3
(
int
__gen_e_acsl_n_arg
);
int
__gen_e_acsl_f3_3
(
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
);
/*@
...
...
@@ -45,10 +45,10 @@ logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
unsigned
long
__gen_e_acsl_f4
(
int
__gen_e_acsl_n_arg
);
unsigned
long
__gen_e_acsl_f4_2
(
long
__gen_e_acsl_n_arg
);
unsigned
long
__gen_e_acsl_f4
(
int
__gen_e_acsl_n_arg
);
unsigned
long
__gen_e_acsl_f4_3
(
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
);
int
main
(
void
)
...
...
@@ -173,6 +173,25 @@ unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return
__retres
;
}
unsigned
long
__gen_e_acsl_f4
(
int
__gen_e_acsl_n_arg
)
{
unsigned
long
__retres
;
unsigned
long
__gen_e_acsl_if_15
;
if
(
__gen_e_acsl_n_arg
<
100
)
{
unsigned
long
__gen_e_acsl_f4_tapp_2
;
__gen_e_acsl_f4_tapp_2
=
__gen_e_acsl_f4_2
(
__gen_e_acsl_n_arg
+
1L
);
__gen_e_acsl_if_15
=
__gen_e_acsl_f4_tapp_2
;
}
else
{
unsigned
long
__gen_e_acsl_if_14
;
if
((
long
)
__gen_e_acsl_n_arg
<
9223372036854775807L
)
__gen_e_acsl_if_14
=
9223372036854775807UL
;
else
__gen_e_acsl_if_14
=
6UL
;
__gen_e_acsl_if_15
=
__gen_e_acsl_if_14
;
}
__retres
=
__gen_e_acsl_if_15
;
return
__retres
;
}
unsigned
long
__gen_e_acsl_f4_2
(
long
__gen_e_acsl_n_arg
)
{
unsigned
long
__retres
;
...
...
@@ -204,25 +223,6 @@ unsigned long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
return
__retres
;
}
unsigned
long
__gen_e_acsl_f4
(
int
__gen_e_acsl_n_arg
)
{
unsigned
long
__retres
;
unsigned
long
__gen_e_acsl_if_15
;
if
(
__gen_e_acsl_n_arg
<
100
)
{
unsigned
long
__gen_e_acsl_f4_tapp_2
;
__gen_e_acsl_f4_tapp_2
=
__gen_e_acsl_f4_2
(
__gen_e_acsl_n_arg
+
1L
);
__gen_e_acsl_if_15
=
__gen_e_acsl_f4_tapp_2
;
}
else
{
unsigned
long
__gen_e_acsl_if_14
;
if
((
long
)
__gen_e_acsl_n_arg
<
9223372036854775807L
)
__gen_e_acsl_if_14
=
9223372036854775807UL
;
else
__gen_e_acsl_if_14
=
6UL
;
__gen_e_acsl_if_15
=
__gen_e_acsl_if_14
;
}
__retres
=
__gen_e_acsl_if_15
;
return
__retres
;
}
int
__gen_e_acsl_f3_3
(
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
)
{
int
__retres
;
...
...
@@ -271,6 +271,26 @@ int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return
__retres
;
}
int
__gen_e_acsl_f3
(
int
__gen_e_acsl_n_arg
)
{
int
__retres
;
int
__gen_e_acsl_if_9
;
if
(
__gen_e_acsl_n_arg
>
0
)
{
int
__gen_e_acsl_g_tapp
;
int
__gen_e_acsl_f3_tapp_2
;
__gen_e_acsl_g_tapp
=
__gen_e_acsl_g
(
__gen_e_acsl_n_arg
);
__gen_e_acsl_f3_tapp_2
=
__gen_e_acsl_f3_2
(
__gen_e_acsl_n_arg
-
1L
);
__gen_e_acsl_if_9
=
__gen_e_acsl_g_tapp
*
__gen_e_acsl_f3_tapp_2
-
5
;
}
else
{
int
__gen_e_acsl_g_tapp_6
;
__gen_e_acsl_g_tapp_6
=
__gen_e_acsl_g_2
(
__gen_e_acsl_n_arg
+
1L
);
__gen_e_acsl_if_9
=
__gen_e_acsl_g_tapp_6
;
}
__retres
=
__gen_e_acsl_if_9
;
return
__retres
;
}
int
__gen_e_acsl_f3_2
(
long
__gen_e_acsl_n_arg
)
{
int
__retres
;
...
...
@@ -315,26 +335,6 @@ int __gen_e_acsl_f3_2(long __gen_e_acsl_n_arg)
return
__retres
;
}
int
__gen_e_acsl_f3
(
int
__gen_e_acsl_n_arg
)
{
int
__retres
;
int
__gen_e_acsl_if_9
;
if
(
__gen_e_acsl_n_arg
>
0
)
{
int
__gen_e_acsl_g_tapp
;
int
__gen_e_acsl_f3_tapp_2
;
__gen_e_acsl_g_tapp
=
__gen_e_acsl_g
(
__gen_e_acsl_n_arg
);
__gen_e_acsl_f3_tapp_2
=
__gen_e_acsl_f3_2
(
__gen_e_acsl_n_arg
-
1L
);
__gen_e_acsl_if_9
=
__gen_e_acsl_g_tapp
*
__gen_e_acsl_f3_tapp_2
-
5
;
}
else
{
int
__gen_e_acsl_g_tapp_6
;
__gen_e_acsl_g_tapp_6
=
__gen_e_acsl_g_2
(
__gen_e_acsl_n_arg
+
1L
);
__gen_e_acsl_if_9
=
__gen_e_acsl_g_tapp_6
;
}
__retres
=
__gen_e_acsl_if_9
;
return
__retres
;
}
int
__gen_e_acsl_g_3
(
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
)
{
int
__retres
;
...
...
@@ -346,14 +346,14 @@ int __gen_e_acsl_g_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return
__retres
;
}
int
__gen_e_acsl_g
_2
(
long
__gen_e_acsl_n_arg
)
int
__gen_e_acsl_g
(
int
__gen_e_acsl_n_arg
)
{
int
__retres
;
__retres
=
0
;
return
__retres
;
}
int
__gen_e_acsl_g
(
int
__gen_e_acsl_n_arg
)
int
__gen_e_acsl_g
_2
(
long
__gen_e_acsl_n_arg
)
{
int
__retres
;
__retres
=
0
;
...
...
@@ -418,6 +418,27 @@ int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return
__retres
;
}
int
__gen_e_acsl_f2
(
int
__gen_e_acsl_n_arg
)
{
int
__retres
;
int
__gen_e_acsl_if_6
;
if
(
__gen_e_acsl_n_arg
<
0
)
__gen_e_acsl_if_6
=
1
;
else
{
int
__gen_e_acsl_f2_tapp_2
;
int
__gen_e_acsl_f2_tapp_9
;
int
__gen_e_acsl_f2_tapp_10
;
__gen_e_acsl_f2_tapp_2
=
__gen_e_acsl_f2_2
(
__gen_e_acsl_n_arg
-
1L
);
__gen_e_acsl_f2_tapp_9
=
__gen_e_acsl_f2_2
(
__gen_e_acsl_n_arg
-
2L
);
__gen_e_acsl_f2_tapp_10
=
__gen_e_acsl_f2_2
(
__gen_e_acsl_n_arg
-
3L
);
__e_acsl_assert
(
__gen_e_acsl_f2_tapp_10
!=
0
,(
char
*
)
"RTE"
,(
char
*
)
"f2"
,
(
char
*
)
"division_by_zero: __gen_e_acsl_f2_tapp_10 != 0"
,
9
);
__gen_e_acsl_if_6
=
(
__gen_e_acsl_f2_tapp_2
*
__gen_e_acsl_f2_tapp_9
)
/
__gen_e_acsl_f2_tapp_10
;
}
__retres
=
__gen_e_acsl_if_6
;
return
__retres
;
}
int
__gen_e_acsl_f2_2
(
long
__gen_e_acsl_n_arg
)
{
int
__retres
;
...
...
@@ -469,27 +490,6 @@ int __gen_e_acsl_f2_2(long __gen_e_acsl_n_arg)
return
__retres
;
}
int
__gen_e_acsl_f2
(
int
__gen_e_acsl_n_arg
)
{
int
__retres
;
int
__gen_e_acsl_if_6
;
if
(
__gen_e_acsl_n_arg
<
0
)
__gen_e_acsl_if_6
=
1
;
else
{
int
__gen_e_acsl_f2_tapp_2
;
int
__gen_e_acsl_f2_tapp_9
;
int
__gen_e_acsl_f2_tapp_10
;
__gen_e_acsl_f2_tapp_2
=
__gen_e_acsl_f2_2
(
__gen_e_acsl_n_arg
-
1L
);
__gen_e_acsl_f2_tapp_9
=
__gen_e_acsl_f2_2
(
__gen_e_acsl_n_arg
-
2L
);
__gen_e_acsl_f2_tapp_10
=
__gen_e_acsl_f2_2
(
__gen_e_acsl_n_arg
-
3L
);
__e_acsl_assert
(
__gen_e_acsl_f2_tapp_10
!=
0
,(
char
*
)
"RTE"
,(
char
*
)
"f2"
,
(
char
*
)
"division_by_zero: __gen_e_acsl_f2_tapp_10 != 0"
,
9
);
__gen_e_acsl_if_6
=
(
__gen_e_acsl_f2_tapp_2
*
__gen_e_acsl_f2_tapp_9
)
/
__gen_e_acsl_f2_tapp_10
;
}
__retres
=
__gen_e_acsl_if_6
;
return
__retres
;
}
void
__gen_e_acsl_f1_3
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
)
{
...
...
@@ -541,6 +541,41 @@ void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
return
;
}
void
__gen_e_acsl_f1
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_n_arg
)
{
__e_acsl_mpz_t
__gen_e_acsl_if_3
;
if
(
__gen_e_acsl_n_arg
<=
0
)
{
__e_acsl_mpz_t
__gen_e_acsl_
;
__gmpz_init_set_si
(
__gen_e_acsl_
,
0L
);
__gmpz_init_set
(
__gen_e_acsl_if_3
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_
));
__gmpz_clear
(
__gen_e_acsl_
);
}
else
{
__e_acsl_mpz_t
__gen_e_acsl_f1_tapp_2
;
__e_acsl_mpz_t
__gen_e_acsl_n_3
;
__e_acsl_mpz_t
__gen_e_acsl_add_3
;
__gmpz_init
(
__gen_e_acsl_f1_tapp_2
);
__gen_e_acsl_f1_2
((
__e_acsl_mpz_struct
*
)
__gen_e_acsl_f1_tapp_2
,
__gen_e_acsl_n_arg
-
1L
);
__gmpz_init_set_si
(
__gen_e_acsl_n_3
,(
long
)
__gen_e_acsl_n_arg
);
__gmpz_init
(
__gen_e_acsl_add_3
);
__gmpz_add
(
__gen_e_acsl_add_3
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_f1_tapp_2
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_n_3
));
__gmpz_init_set
(
__gen_e_acsl_if_3
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_3
));
__gmpz_clear
(
__gen_e_acsl_f1_tapp_2
);
__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_3
));
__gmpz_clear
(
__gen_e_acsl_if_3
);
return
;
}
void
__gen_e_acsl_f1_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
long
__gen_e_acsl_n_arg
)
{
...
...
@@ -585,39 +620,4 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
return
;
}
void
__gen_e_acsl_f1
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_n_arg
)
{
__e_acsl_mpz_t
__gen_e_acsl_if_3
;
if
(
__gen_e_acsl_n_arg
<=
0
)
{
__e_acsl_mpz_t
__gen_e_acsl_
;
__gmpz_init_set_si
(
__gen_e_acsl_
,
0L
);
__gmpz_init_set
(
__gen_e_acsl_if_3
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_
));
__gmpz_clear
(
__gen_e_acsl_
);
}
else
{
__e_acsl_mpz_t
__gen_e_acsl_f1_tapp_2
;
__e_acsl_mpz_t
__gen_e_acsl_n_3
;
__e_acsl_mpz_t
__gen_e_acsl_add_3
;
__gmpz_init
(
__gen_e_acsl_f1_tapp_2
);
__gen_e_acsl_f1_2
((
__e_acsl_mpz_struct
*
)
__gen_e_acsl_f1_tapp_2
,
__gen_e_acsl_n_arg
-
1L
);
__gmpz_init_set_si
(
__gen_e_acsl_n_3
,(
long
)
__gen_e_acsl_n_arg
);
__gmpz_init
(
__gen_e_acsl_add_3
);
__gmpz_add
(
__gen_e_acsl_add_3
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_f1_tapp_2
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_n_3
));
__gmpz_init_set
(
__gen_e_acsl_if_3
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_add_3
));
__gmpz_clear
(
__gen_e_acsl_f1_tapp_2
);
__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_3
));
__gmpz_clear
(
__gen_e_acsl_if_3
);
return
;
}
src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
View file @
f00d8524
...
...
@@ -42,12 +42,12 @@ logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
void
__gen_e_acsl_f4_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
);
void
__gen_e_acsl_f4
(
__e_acsl_mpz_struct
*
__retres_arg
,
int
__gen_e_acsl_n_arg
);
void
__gen_e_acsl_f4_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
);
int
main
(
void
)
{
int
__retres
;
...
...
@@ -155,6 +155,70 @@ int main(void)
return
__retres
;
}
void
__gen_e_acsl_f4_2
(
__e_acsl_mpz_struct
*
__retres_arg
,
__e_acsl_mpz_struct
*
__gen_e_acsl_n_arg
)
{
__e_acsl_mpz_t
__gen_e_acsl_n_14
;
__e_acsl_mpz_t
__gen_e_acsl__36
;
int
__gen_e_acsl_lt_4
;
__e_acsl_mpz_t
__gen_e_acsl_if_8
;
__gmpz_init_set
(
__gen_e_acsl_n_14
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_n_arg
));
__gmpz_init_set_si
(
__gen_e_acsl__36
,
100L
);
__gen_e_acsl_lt_4
=
__gmpz_cmp
((
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_n_14
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__36
));
if
(
__gen_e_acsl_lt_4
<
0
)
{
__e_acsl_mpz_t
__gen_e_acsl__37
;
__e_acsl_mpz_t
__gen_e_acsl_add_6
;
__e_acsl_mpz_t
__gen_e_acsl_f4_tapp_3
;
__gmpz_init_set_si
(
__gen_e_acsl__37
,
1L
);
__gmpz_init
(
__gen_e_acsl_add_6
);
__gmpz_add
(
__gen_e_acsl_add_6
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_n_14
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__37
));
__gmpz_init
(
__gen_e_acsl_f4_tapp_3
);
__gen_e_acsl_f4_2
((
__e_acsl_mpz_struct
*
)
__gen_e_acsl_f4_tapp_3
,
(
__e_acsl_mpz_struct
*
)
__gen_e_acsl_add_6
);
__gmpz_init_set
(
__gen_e_acsl_if_8
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_f4_tapp_3
));
__gmpz_clear
(
__gen_e_acsl__37
);
__gmpz_clear
(
__gen_e_acsl_add_6
);
__gmpz_clear
(
__gen_e_acsl_f4_tapp_3
);
}
else
{
__e_acsl_mpz_t
__gen_e_acsl__38
;
int
__gen_e_acsl_lt_5
;
__e_acsl_mpz_t
__gen_e_acsl_if_7
;
__gmpz_init_set_ui
(
__gen_e_acsl__38
,
9223372036854775807UL
);
__gen_e_acsl_lt_5
=
__gmpz_cmp
((
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_n_14
),
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__38
));
if
(
__gen_e_acsl_lt_5
<
0
)
{
__e_acsl_mpz_t
__gen_e_acsl__39
;
__gmpz_init_set_ui
(
__gen_e_acsl__39
,
9223372036854775807UL
);
__gmpz_init_set
(
__gen_e_acsl_if_7
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__39
));
__gmpz_clear
(
__gen_e_acsl__39
);
}
else
{
__e_acsl_mpz_t
__gen_e_acsl__40
;
__gmpz_init_set_si
(
__gen_e_acsl__40
,
6L
);
__gmpz_init_set
(
__gen_e_acsl_if_7
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl__40
));
__gmpz_clear
(
__gen_e_acsl__40
);
}
__gmpz_init_set
(
__gen_e_acsl_if_8
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_if_7
));
__gmpz_clear
(
__gen_e_acsl__38
);
__gmpz_clear
(
__gen_e_acsl_if_7
);
}
__gmpz_init_set
(
__retres_arg
,
(
__e_acsl_mpz_struct
const
*
)(
__gen_e_acsl_if_8
));
__gmpz_clear
(
__gen_e_acsl_n_14
);
__gmpz_clear
(
__gen_e_acsl__36
);
__gmpz_clear
(
__gen_e_acsl_if_8
);
return
;
}