Newer
Older
long A = (long)0;
int main(void)
{
int __retres;
/*@ assert A + (long)((long)(3 * A) - 1) ≡ -1; */
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
{
__e_acsl_mpz_t __gen_e_acsl_A;
__e_acsl_mpz_t __gen_e_acsl_;
__e_acsl_mpz_t __gen_e_acsl_mul;
long __gen_e_acsl__2;
__e_acsl_mpz_t __gen_e_acsl__3;
__e_acsl_mpz_t __gen_e_acsl_add;
__e_acsl_mpz_t __gen_e_acsl__4;
int __gen_e_acsl_eq;
__gmpz_init_set_si(__gen_e_acsl_A,A);
__gmpz_init_set_si(__gen_e_acsl_,3L);
__gmpz_init(__gen_e_acsl_mul);
__gmpz_mul(__gen_e_acsl_mul,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_A));
__gen_e_acsl__2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
/*@ assert
Value: signed_overflow:
-9223372036854775808 ≤ __gen_e_acsl__2 - 1;
*/
__gmpz_init_set_si(__gen_e_acsl__3,__gen_e_acsl__2 - 1L);
__gmpz_init(__gen_e_acsl_add);
__gmpz_add(__gen_e_acsl_add,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_A),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
__gmpz_init_set_si(__gen_e_acsl__4,(long)(-1));
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",
(char *)"main",
(char *)"A + (long)((long)(3 * A) - 1) == -1",8);
__gmpz_clear(__gen_e_acsl_A);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl_mul);
__gmpz_clear(__gen_e_acsl__3);
__gmpz_clear(__gen_e_acsl_add);
__gmpz_clear(__gen_e_acsl__4);
}
}
__retres = 0;
return __retres;
}