Skip to content
Snippets Groups Projects
Commit 8fa22b8e authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] add one missing oracle file

parent 87969dbc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c 0 → 100644
+ 659
− 0
View file @ 8fa22b8e
/* Generated by Frama-C */
typedef unsigned long size_t;
typedef unsigned long mp_limb_t;
struct __anonstruct___mpz_struct_6 {
int _mp_alloc ;
int _mp_size ;
mp_limb_t *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_6 __mpz_struct;
typedef __mpz_struct mpz_t[1];
typedef mp_limb_t *mp_ptr;
typedef mp_limb_t const *mp_srcptr;
typedef long mp_size_t;
struct __anonstruct___mpq_struct_7 {
__mpz_struct _mp_num ;
__mpz_struct _mp_den ;
};
typedef struct __anonstruct___mpq_struct_7 __mpq_struct;
typedef __mpz_struct const *mpz_srcptr;
typedef __mpz_struct *mpz_ptr;
typedef __mpq_struct const *mpq_srcptr;
typedef __mpq_struct *mpq_ptr;
/* compiler builtin:
long __builtin_expect(long, long); */
/*@ assigns \nothing; */
extern int printf(char const * __restrict __format , ...);
__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
assigns *z1;
*/
extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(x);
assigns *x; */
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2) __attribute__((
__pure__));
__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z) __attribute__((
__pure__));
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
mp_size_t __gmp_n) __attribute__((
__pure__));
/*@ ensures \valid(\old(x));
assigns *x; */
extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
/*@ ensures \valid(\old(z));
assigns *z; */
extern void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
/*@ ensures \valid(\old(z));
assigns *z;
assigns *z \from n; */
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
__pure__));
__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
__pure__));
extern void __gmpz_set(mpz_ptr, mpz_srcptr);
__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u);
__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
__pure__));
extern void __gmpz_tdiv_q(mpz_ptr, mpz_srcptr, mpz_srcptr);
__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u);
extern void __gmpq_set(mpq_ptr, mpq_srcptr);
__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
mp_size_t __gmp_xsize,
mp_srcptr __gmp_yp,
mp_size_t __gmp_ysize);
__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
mp_size_t __gmp_size,
mp_limb_t __gmp_n);
extern mp_limb_t __gmpn_add_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
mp_size_t __gmp_size) __attribute__((__pure__));
__inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
mp_size_t __gmp_n);
extern int __gmpn_perfect_square_p(mp_srcptr, mp_size_t) __attribute__((
__pure__));
extern unsigned long __gmpn_popcount(mp_srcptr, mp_size_t) __attribute__((
__pure__));
__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
mp_size_t __gmp_xsize,
mp_srcptr __gmp_yp,
mp_size_t __gmp_ysize);
__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
mp_size_t __gmp_size,
mp_limb_t __gmp_n);
extern mp_limb_t __gmpn_sub_n(mp_ptr, mp_srcptr, mp_srcptr, mp_size_t);
__inline static void __gmpz_abs(mpz_ptr __gmp_w, mpz_srcptr __gmp_u)
{
if (__gmp_w != __gmp_u) { __gmpz_set(__gmp_w,__gmp_u); }
if (__gmp_w->_mp_size >= 0) { __gmp_w->_mp_size = __gmp_w->_mp_size; }
else { __gmp_w->_mp_size = - __gmp_w->_mp_size; }
return;
}
__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static int __gmpz_fits_uint_p(mpz_srcptr __gmp_z)
{
int __retres;
mp_size_t __gmp_n;
mp_ptr __gmp_p;
int tmp;
__gmp_n = (long)__gmp_z->_mp_size;
__gmp_p = __gmp_z->_mp_d;
if (__gmp_n == (mp_size_t)0) { tmp = 1; }
else {
if (__gmp_n == (mp_size_t)1) {
if (*(__gmp_p + 0) <= (mp_limb_t)(~ ((unsigned int)0))) { tmp = 1; }
else { tmp = 0; }
}
else { tmp = 0; }
}
__retres = tmp;
goto return_label;
return_label: /* internal */
return (__retres);
}
__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static int __gmpz_fits_ulong_p(mpz_srcptr __gmp_z)
{
int __retres;
mp_size_t __gmp_n;
mp_ptr __gmp_p;
int tmp;
__gmp_n = (long)__gmp_z->_mp_size;
__gmp_p = __gmp_z->_mp_d;
if (__gmp_n == (mp_size_t)0) { tmp = 1; }
else {
if (__gmp_n == (mp_size_t)1) {
if (*(__gmp_p + 0) <= ~ ((unsigned long)0)) { tmp = 1; }
else { tmp = 0; }
}
else { tmp = 0; }
}
__retres = tmp;
goto return_label;
return_label: /* internal */
return (__retres);
}
__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static int __gmpz_fits_ushort_p(mpz_srcptr __gmp_z)
{
int __retres;
mp_size_t __gmp_n;
mp_ptr __gmp_p;
int tmp;
__gmp_n = (long)__gmp_z->_mp_size;
__gmp_p = __gmp_z->_mp_d;
if (__gmp_n == (mp_size_t)0) { tmp = 1; }
else {
if (__gmp_n == (mp_size_t)1) {
if (*(__gmp_p + 0) <= (mp_limb_t)((unsigned short)(~ 0))) { tmp = 1; }
else { tmp = 0; }
}
else { tmp = 0; }
}
__retres = tmp;
goto return_label;
return_label: /* internal */
return (__retres);
}
/*@ requires \valid(z);
assigns \nothing; */
__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z) __attribute__((
__pure__));
__inline static unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z)
{
mp_ptr __gmp_p;
mp_size_t __gmp_n;
mp_limb_t __gmp_l;
mp_limb_t tmp;
__gmp_p = z->_mp_d;
__gmp_n = (long)z->_mp_size;
__gmp_l = *(__gmp_p + 0);
if (__gmp_n != (mp_size_t)0) { tmp = __gmp_l; }
else { tmp = (unsigned long)0; }
return (tmp);
}
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
mp_size_t __gmp_n) __attribute__((
__pure__));
__inline static mp_limb_t __gmpz_getlimbn(mpz_srcptr __gmp_z,
mp_size_t __gmp_n)
{
mp_limb_t __gmp_result;
long tmp_1;
int tmp_0;
__gmp_result = (unsigned long)0;
{ /*undefined sequence*/
if (__gmp_n >= (mp_size_t)0) {
int tmp;
{ /*undefined sequence*/
if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
else { tmp = - __gmp_z->_mp_size; }
;
}
if (__gmp_n < (mp_size_t)tmp) { tmp_0 = 1; }
else { tmp_0 = 0; }
}
else { tmp_0 = 0; }
tmp_1 = __builtin_expect((long)(tmp_0 != 0),(long)1);
}
if (tmp_1) { __gmp_result = *(__gmp_z->_mp_d + __gmp_n); }
return (__gmp_result);
}
/*@ requires \valid(z1);
requires \valid(z2);
assigns *z1; */
__inline static void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2)
{
if (z1 != z2) { __gmpz_set(z1,z2); }
z1->_mp_size = - z1->_mp_size;
return;
}
__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a) __attribute__((
__pure__));
__inline static int __gmpz_perfect_square_p(mpz_srcptr __gmp_a)
{
mp_size_t __gmp_asize;
int __gmp_result;
long tmp;
__gmp_asize = (long)__gmp_a->_mp_size;
__gmp_result = __gmp_asize >= (mp_size_t)0;
tmp = __builtin_expect((long)((__gmp_asize > (mp_size_t)0) != 0),(long)1);
if (tmp) {
__gmp_result = __gmpn_perfect_square_p((mp_limb_t const *)__gmp_a->_mp_d,
__gmp_asize);
}
return (__gmp_result);
}
__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u) __attribute__((
__pure__));
__inline static unsigned long __gmpz_popcount(mpz_srcptr __gmp_u)
{
mp_size_t __gmp_usize;
unsigned long __gmp_result;
long tmp;
__gmp_usize = (long)__gmp_u->_mp_size;
if (__gmp_usize < (mp_size_t)0) { __gmp_result = ~ ((unsigned long)0); }
else { __gmp_result = (unsigned long)0; }
tmp = __builtin_expect((long)((__gmp_usize > (mp_size_t)0) != 0),(long)1);
if (tmp) {
__gmp_result = __gmpn_popcount((mp_limb_t const *)__gmp_u->_mp_d,
__gmp_usize);
}
return (__gmp_result);
}
__inline static void __gmpz_set_q(mpz_ptr __gmp_w, mpq_srcptr __gmp_u)
{
__gmpz_tdiv_q(__gmp_w,& __gmp_u->_mp_num,& __gmp_u->_mp_den);
return;
}
__inline static size_t __gmpz_size(mpz_srcptr __gmp_z) __attribute__((
__pure__));
__inline static size_t __gmpz_size(mpz_srcptr __gmp_z)
{
size_t __retres;
int tmp;
if (__gmp_z->_mp_size >= 0) { tmp = __gmp_z->_mp_size; }
else { tmp = - __gmp_z->_mp_size; }
__retres = (unsigned long)tmp;
return (__retres);
}
__inline static void __gmpq_abs(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
{
if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
if (__gmp_w->_mp_num._mp_size >= 0) {
__gmp_w->_mp_num._mp_size = __gmp_w->_mp_num._mp_size;
}
else { __gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size; }
return;
}
__inline static void __gmpq_neg(mpq_ptr __gmp_w, mpq_srcptr __gmp_u)
{
if (__gmp_w != __gmp_u) { __gmpq_set(__gmp_w,__gmp_u); }
__gmp_w->_mp_num._mp_size = - __gmp_w->_mp_num._mp_size;
return;
}
__inline static mp_limb_t __gmpn_add(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
mp_size_t __gmp_xsize,
mp_srcptr __gmp_yp,
mp_size_t __gmp_ysize)
{
mp_limb_t __gmp_c;
while (1) {
{ mp_size_t __gmp_i; mp_limb_t __gmp_x; __gmp_i = __gmp_ysize;
if (__gmp_i != (mp_size_t)0) {
mp_limb_t tmp_1;
tmp_1 = __gmpn_add_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
if (tmp_1) {
while (1) {
mp_size_t tmp;
mp_limb_t tmp_0;
if (__gmp_i >= __gmp_xsize) {
__gmp_c = (unsigned long)1;
goto __gmp_done;
}
__gmp_x = *(__gmp_xp + __gmp_i);
{ /*undefined sequence*/
tmp = __gmp_i;
__gmp_i += (mp_size_t)1;
tmp_0 = (__gmp_x + (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
*(__gmp_wp + tmp) = tmp_0;
}
if (! (tmp_0 == (mp_limb_t)0)) { break; }
}
}
}
if (__gmp_wp != __gmp_xp) {
while (1) {
{ mp_size_t __gmp_j; __gmp_j = __gmp_i;
while (__gmp_j < __gmp_xsize) {
*(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
__gmp_j += (mp_size_t)1;
}
}
break;
}
} __gmp_c = (unsigned long)0; __gmp_done: ;
}
break;
}
return (__gmp_c);
}
__inline static mp_limb_t __gmpn_add_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
mp_size_t __gmp_size,
mp_limb_t __gmp_n)
{
mp_limb_t __gmp_c;
while (1) {
{ mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_r;
__gmp_x = *(__gmp_src + 0); __gmp_r = __gmp_x + __gmp_n;
*(__gmp_dst + 0) = __gmp_r;
if (__gmp_r < __gmp_n) {
__gmp_c = (unsigned long)1;
__gmp_i = (long)1;
while (__gmp_i < __gmp_size) {
__gmp_x = *(__gmp_src + __gmp_i);
__gmp_r = __gmp_x + (mp_limb_t)1;
*(__gmp_dst + __gmp_i) = __gmp_r;
__gmp_i += (mp_size_t)1;
if (! (__gmp_r < (mp_limb_t)1)) {
if (__gmp_src != __gmp_dst) {
while (1) {
{ mp_size_t __gmp_j; __gmp_j = __gmp_i;
while (__gmp_j < __gmp_size) {
*(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
__gmp_j += (mp_size_t)1;
}
}
break;
}
}
__gmp_c = (unsigned long)0;
break;
}
}
}
else {
if (__gmp_src != __gmp_dst) {
while (1) {
{ mp_size_t __gmp_j_0; __gmp_j_0 = (long)1;
while (__gmp_j_0 < __gmp_size) {
*(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
__gmp_j_0 += (mp_size_t)1;
}
}
break;
}
}
__gmp_c = (unsigned long)0;
}
}
break;
}
return (__gmp_c);
}
__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
mp_size_t __gmp_size) __attribute__((__pure__));
__inline static int __gmpn_cmp(mp_srcptr __gmp_xp, mp_srcptr __gmp_yp,
mp_size_t __gmp_size)
{
int __gmp_result;
while (1) {
{ mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_y;
__gmp_result = 0; __gmp_i = __gmp_size;
while (1) {
__gmp_i -= (mp_size_t)1;
if (! (__gmp_i >= (mp_size_t)0)) { break; }
__gmp_x = *(__gmp_xp + __gmp_i);
__gmp_y = *(__gmp_yp + __gmp_i);
if (__gmp_x != __gmp_y) {
if (__gmp_x > __gmp_y) { __gmp_result = 1; }
else { __gmp_result = -1; }
break;
}
}
}
break;
}
return (__gmp_result);
}
__inline static mp_limb_t __gmpn_sub(mp_ptr __gmp_wp, mp_srcptr __gmp_xp,
mp_size_t __gmp_xsize,
mp_srcptr __gmp_yp,
mp_size_t __gmp_ysize)
{
mp_limb_t __gmp_c;
while (1) {
{ mp_size_t __gmp_i; mp_limb_t __gmp_x; __gmp_i = __gmp_ysize;
if (__gmp_i != (mp_size_t)0) {
mp_limb_t tmp_0;
tmp_0 = __gmpn_sub_n(__gmp_wp,__gmp_xp,__gmp_yp,__gmp_i);
if (tmp_0) {
while (1) {
mp_size_t tmp;
if (__gmp_i >= __gmp_xsize) {
__gmp_c = (unsigned long)1;
goto __gmp_done;
}
__gmp_x = *(__gmp_xp + __gmp_i);
{ /*undefined sequence*/
tmp = __gmp_i;
__gmp_i += (mp_size_t)1;
*(__gmp_wp + tmp) = (__gmp_x - (mp_limb_t)1) & (~ ((unsigned long)0) >> 0);
}
if (! (__gmp_x == (mp_limb_t)0)) { break; }
}
}
}
if (__gmp_wp != __gmp_xp) {
while (1) {
{ mp_size_t __gmp_j; __gmp_j = __gmp_i;
while (__gmp_j < __gmp_xsize) {
*(__gmp_wp + __gmp_j) = *(__gmp_xp + __gmp_j);
__gmp_j += (mp_size_t)1;
}
}
break;
}
} __gmp_c = (unsigned long)0; __gmp_done: ;
}
break;
}
return (__gmp_c);
}
__inline static mp_limb_t __gmpn_sub_1(mp_ptr __gmp_dst, mp_srcptr __gmp_src,
mp_size_t __gmp_size,
mp_limb_t __gmp_n)
{
mp_limb_t __gmp_c;
while (1) {
{ mp_size_t __gmp_i; mp_limb_t __gmp_x; mp_limb_t __gmp_r;
__gmp_x = *(__gmp_src + 0); __gmp_r = __gmp_x - __gmp_n;
*(__gmp_dst + 0) = __gmp_r;
if (__gmp_x < __gmp_n) {
__gmp_c = (unsigned long)1;
__gmp_i = (long)1;
while (__gmp_i < __gmp_size) {
__gmp_x = *(__gmp_src + __gmp_i);
__gmp_r = __gmp_x - (mp_limb_t)1;
*(__gmp_dst + __gmp_i) = __gmp_r;
__gmp_i += (mp_size_t)1;
if (! (__gmp_x < (mp_limb_t)1)) {
if (__gmp_src != __gmp_dst) {
while (1) {
{ mp_size_t __gmp_j; __gmp_j = __gmp_i;
while (__gmp_j < __gmp_size) {
*(__gmp_dst + __gmp_j) = *(__gmp_src + __gmp_j);
__gmp_j += (mp_size_t)1;
}
}
break;
}
}
__gmp_c = (unsigned long)0;
break;
}
}
}
else {
if (__gmp_src != __gmp_dst) {
while (1) {
{ mp_size_t __gmp_j_0; __gmp_j_0 = (long)1;
while (__gmp_j_0 < __gmp_size) {
*(__gmp_dst + __gmp_j_0) = *(__gmp_src + __gmp_j_0);
__gmp_j_0 += (mp_size_t)1;
}
}
break;
}
}
__gmp_c = (unsigned long)0;
}
}
break;
}
return (__gmp_c);
}
__inline static mp_limb_t __gmpn_neg_n(mp_ptr __gmp_rp, mp_srcptr __gmp_up,
mp_size_t __gmp_n)
{
mp_limb_t __gmp_ul;
mp_limb_t __gmp_cy;
__gmp_cy = (unsigned long)0;
while (1) {
{ mp_srcptr tmp; mp_ptr tmp_0;
{ /*undefined sequence*/ tmp = __gmp_up; __gmp_up ++; __gmp_ul = *tmp;
}
{ /*undefined sequence*/
tmp_0 = __gmp_rp;
__gmp_rp ++;
*tmp_0 = - __gmp_ul - __gmp_cy;
} __gmp_cy |= (unsigned long)(__gmp_ul != (mp_limb_t)0);
}
__gmp_n -= (mp_size_t)1;
if (! (__gmp_n != (mp_size_t)0)) { break; }
}
return (__gmp_cy);
}
/*@ terminates \false;
ensures \false;
assigns \nothing; */
extern void exit(int status);
void e_acsl_fail(char *msg)
{
printf("%s\n",msg);
exit(1);
return;
}
int main(void)
{
int __retres;
int x;
int e_acsl_4;
mpz_t e_acsl_11;
int e_acsl_14;
x = 0;
L: e_acsl_14 = x;
{ mpz_t e_acsl_8; mpz_t e_acsl_9; mpz_t e_acsl_10;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)x);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)1);
__gmpz_init((__mpz_struct *)(e_acsl_10));
__gmpz_add((__mpz_struct *)(e_acsl_10),(__mpz_struct const *)(e_acsl_8),
(__mpz_struct const *)(e_acsl_9));
__gmpz_init_set((__mpz_struct *)(e_acsl_11),
(__mpz_struct const *)(e_acsl_10));
__gmpz_clear((__mpz_struct *)(e_acsl_8));
__gmpz_clear((__mpz_struct *)(e_acsl_9));
__gmpz_clear((__mpz_struct *)(e_acsl_10));
}
e_acsl_4 = x;
/*@ assert x ≡ 0; */ ;
{ mpz_t e_acsl_1; mpz_t e_acsl_2; int e_acsl_3;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)x);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
(__mpz_struct const *)(e_acsl_2));
if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(x == 0)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_1));
__gmpz_clear((__mpz_struct *)(e_acsl_2));
}
x = 1;
x = 2;
/*@ assert \at(x,L) ≡ 0; */ ;
{ mpz_t e_acsl_5; mpz_t e_acsl_6; int e_acsl_7;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)e_acsl_4);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_6),(long)0);
e_acsl_7 = __gmpz_cmp((__mpz_struct const *)(e_acsl_5),
(__mpz_struct const *)(e_acsl_6));
if (! (e_acsl_7 == 0)) { e_acsl_fail((char *)"(\\at(x,L) == 0)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_5));
__gmpz_clear((__mpz_struct *)(e_acsl_6));
}
/*@ assert \at(x+1,L) ≡ 1; */ ;
{ mpz_t e_acsl_12; int e_acsl_13;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_12),(long)1);
e_acsl_13 = __gmpz_cmp((__mpz_struct const *)(e_acsl_11),
(__mpz_struct const *)(e_acsl_12));
if (! (e_acsl_13 == 0)) { e_acsl_fail((char *)"(\\at(x+1,L) == 1)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_12));
}
/*@ assert \at(x,L)+1 ≡ 1; */ ;
{ mpz_t e_acsl_15; mpz_t e_acsl_16; mpz_t e_acsl_17; int e_acsl_18;
__gmpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)e_acsl_14);
__gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)1);
__gmpz_init((__mpz_struct *)(e_acsl_17));
__gmpz_add((__mpz_struct *)(e_acsl_17),(__mpz_struct const *)(e_acsl_15),
(__mpz_struct const *)(e_acsl_16));
e_acsl_18 = __gmpz_cmp((__mpz_struct const *)(e_acsl_17),
(__mpz_struct const *)(e_acsl_16));
if (! (e_acsl_18 == 0)) { e_acsl_fail((char *)"(\\at(x,L)+1 == 1)"); }
__gmpz_clear((__mpz_struct *)(e_acsl_15));
__gmpz_clear((__mpz_struct *)(e_acsl_16));
__gmpz_clear((__mpz_struct *)(e_acsl_17));
}
__retres = 0;
__gmpz_clear((__mpz_struct *)(e_acsl_11));
return (__retres);
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment