diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
index 6e9dcf927c6c35f582ba096b6110bac745916d37..43a8772bda98cc2556f3bf6ea733553d86bdaf28 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
@@ -235,11 +235,11 @@ void __initialize (void * ptr, size_t size) {
unsigned i;
for(i = 0; i < size; i++) {
- int byte_offset = (size_t)ptr - tmp->ptr + i;
- int ind = byte_offset / 8;
- unsigned char mask_bit = 1U << (7 - (byte_offset % 8));
- if((tmp->init_ptr[ind] & mask_bit) == 0) tmp->init_cpt++;
- tmp->init_ptr[ind] |= mask_bit;
+ size_t offset = (uintptr_t)ptr - tmp->ptr + i;
+ int byte = offset/8;
+ int bit = offset%8;
+ tmp->init_ptr[byte] |= 1 << bit;
+ tmp->init_cpt++;
}
/* now fully initialized */
@@ -405,7 +405,7 @@ void __e_acsl_print_block (struct _block * ptr) {
ptr->is_readonly ? "" : "not ", ptr->init_cpt);
if(ptr->init_ptr != NULL) {
unsigned i;
- for(i = 0; i < ptr->size/8; i++)
+ for(i = 0; i < ptr->size/8; i++)
DLOG("%b ", ptr->init_ptr[i]);
}
DLOG("\n");
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
index 143514ebbcd2d183f2dedcb8d4e64ee93c191b64..f3719fb1be94ead3b43a2c806efc5deff77cf6d4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
@@ -7,6 +7,8 @@
int A = 0;
int B;
+#define ODD(_n) (_n%2 != 0)
+
int main(void) {
/* All globals are initialized, even if the initializer is not given */
int *p = &A;
@@ -74,4 +76,26 @@ int main(void) {
p = NULL;
/*@assert ! \initialized(p); */
+
+ /* Partial initialization */
+ int size = 100;
+ char *partsc = malloc(size*sizeof(char));
+ char *partsi = malloc(size*sizeof(int));
+
+ for (int i = 0; i < size; i++) {
+ if (ODD(i))
+ partsc[i] = '0';
+ else
+ partsi[i] = 0;
+ }
+
+ for (int i = 0; i < size; i++) {
+ if (ODD(i)) {
+ /* @assert \initialized(partsc + i); */
+ /* @assert ! \initialized(partsi + i); */
+ } else {
+ /* @assert \initialized(partsi + i); */
+ /* @assert ! \initialized(partsc + i); */
+ }
+ }
}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..49f3ff5f2987d0c2c433e7027dad0aeb2bbc084e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/block_length.res.oracle
@@ -0,0 +1,23 @@
+[e-acsl] beginning translation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+ Ignoring annotation.
+tests/e-acsl-runtime/block_length.c:12:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/block_length.c:45:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/block_length.c:46:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/block_length.c:48:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/block_length.c:54:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/block_length.c:56:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
new file mode 100644
index 0000000000000000000000000000000000000000..41fd1e98e531b2ec3e626c3cdd0f52d945d99c40
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_block_length.c
@@ -0,0 +1,421 @@
+/* Generated by Frama-C */
+struct Zero {
+
+};
+int A[4] = {1, 2, 3, 4};
+int *PA;
+struct Zero ZERO;
+void __e_acsl_globals_init(void)
+{
+ __store_block((void *)(& ZERO),0UL);
+ __full_init((void *)(& ZERO));
+ __store_block((void *)(& PA),8UL);
+ __full_init((void *)(& PA));
+ __store_block((void *)(A),16UL);
+ __full_init((void *)(& A));
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ int a[4];
+ int *pa;
+ long l;
+ char *pl;
+ int *pi;
+ size_t size;
+ char *p;
+ long *q;
+ struct Zero zero;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_globals_init();
+ __store_block((void *)(& zero),0UL);
+ __store_block((void *)(& q),8UL);
+ __store_block((void *)(& p),8UL);
+ __store_block((void *)(& pi),8UL);
+ __store_block((void *)(& pl),8UL);
+ __store_block((void *)(& l),8UL);
+ __store_block((void *)(& pa),8UL);
+ __store_block((void *)(a),16UL);
+ PA = (int *)(& A);
+ /*@ assert \block_length((int *)A) ≡ sizeof(A); */
+ {
+ unsigned long __e_acsl_block_length;
+ mpz_t __e_acsl_block_length_2;
+ mpz_t __e_acsl_sizeof;
+ int __e_acsl_eq;
+ __e_acsl_block_length = __block_length((void *)(A));
+ __gmpz_init_set_ui(__e_acsl_block_length_2,__e_acsl_block_length);
+ __gmpz_init_set_si(__e_acsl_sizeof,16L);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_2),
+ (__mpz_struct const *)(__e_acsl_sizeof));
+ __e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length((int *)A) == sizeof(A)",15);
+ __gmpz_clear(__e_acsl_block_length_2);
+ __gmpz_clear(__e_acsl_sizeof);
+ }
+ /*@ assert \block_length(&A[3]) ≡ sizeof(A); */
+ {
+ unsigned long __e_acsl_block_length_3;
+ mpz_t __e_acsl_block_length_4;
+ mpz_t __e_acsl_sizeof_2;
+ int __e_acsl_eq_2;
+ __e_acsl_block_length_3 = __block_length((void *)(& A[3]));
+ __gmpz_init_set_ui(__e_acsl_block_length_4,__e_acsl_block_length_3);
+ __gmpz_init_set_si(__e_acsl_sizeof_2,16L);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_4),
+ (__mpz_struct const *)(__e_acsl_sizeof_2));
+ __e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(&A[3]) == sizeof(A)",16);
+ __gmpz_clear(__e_acsl_block_length_4);
+ __gmpz_clear(__e_acsl_sizeof_2);
+ }
+ /*@ assert \block_length(PA) ≡ sizeof(A); */
+ {
+ unsigned long __e_acsl_block_length_5;
+ mpz_t __e_acsl_block_length_6;
+ mpz_t __e_acsl_sizeof_3;
+ int __e_acsl_eq_3;
+ __e_acsl_block_length_5 = __block_length((void *)PA);
+ __gmpz_init_set_ui(__e_acsl_block_length_6,__e_acsl_block_length_5);
+ __gmpz_init_set_si(__e_acsl_sizeof_3,16L);
+ __e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_6),
+ (__mpz_struct const *)(__e_acsl_sizeof_3));
+ __e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(PA) == sizeof(A)",17);
+ __gmpz_clear(__e_acsl_block_length_6);
+ __gmpz_clear(__e_acsl_sizeof_3);
+ }
+ PA ++;
+ /*@ assert \block_length(PA+1) ≡ \block_length(&A[1]); */
+ {
+ unsigned long __e_acsl_block_length_7;
+ mpz_t __e_acsl_block_length_8;
+ unsigned long __e_acsl_block_length_9;
+ mpz_t __e_acsl_block_length_10;
+ int __e_acsl_eq_4;
+ __e_acsl_block_length_7 = __block_length((void *)(PA + 1));
+ __gmpz_init_set_ui(__e_acsl_block_length_8,__e_acsl_block_length_7);
+ __e_acsl_block_length_9 = __block_length((void *)(& A[1]));
+ __gmpz_init_set_ui(__e_acsl_block_length_10,__e_acsl_block_length_9);
+ __e_acsl_eq_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_8),
+ (__mpz_struct const *)(__e_acsl_block_length_10));
+ __e_acsl_assert(__e_acsl_eq_4 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(PA+1) == \\block_length(&A[1])",
+ 19);
+ __gmpz_clear(__e_acsl_block_length_8);
+ __gmpz_clear(__e_acsl_block_length_10);
+ }
+ __initialize((void *)(a),sizeof(int));
+ a[0] = 1;
+ __initialize((void *)(& a[1]),sizeof(int));
+ a[1] = 2;
+ __initialize((void *)(& a[2]),sizeof(int));
+ a[2] = 3;
+ __initialize((void *)(& a[3]),sizeof(int));
+ a[3] = 4;
+ __full_init((void *)(& pa));
+ pa = (int *)(& a);
+ /*@ assert \block_length((int *)a) ≡ sizeof(a); */
+ {
+ unsigned long __e_acsl_block_length_11;
+ mpz_t __e_acsl_block_length_12;
+ mpz_t __e_acsl_sizeof_4;
+ int __e_acsl_eq_5;
+ __e_acsl_block_length_11 = __block_length((void *)(a));
+ __gmpz_init_set_ui(__e_acsl_block_length_12,__e_acsl_block_length_11);
+ __gmpz_init_set_si(__e_acsl_sizeof_4,16L);
+ __e_acsl_eq_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_12),
+ (__mpz_struct const *)(__e_acsl_sizeof_4));
+ __e_acsl_assert(__e_acsl_eq_5 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length((int *)a) == sizeof(a)",24);
+ __gmpz_clear(__e_acsl_block_length_12);
+ __gmpz_clear(__e_acsl_sizeof_4);
+ }
+ /*@ assert \block_length(&a[3]) ≡ sizeof(a); */
+ {
+ unsigned long __e_acsl_block_length_13;
+ mpz_t __e_acsl_block_length_14;
+ mpz_t __e_acsl_sizeof_5;
+ int __e_acsl_eq_6;
+ __e_acsl_block_length_13 = __block_length((void *)(& a[3]));
+ __gmpz_init_set_ui(__e_acsl_block_length_14,__e_acsl_block_length_13);
+ __gmpz_init_set_si(__e_acsl_sizeof_5,16L);
+ __e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_14),
+ (__mpz_struct const *)(__e_acsl_sizeof_5));
+ __e_acsl_assert(__e_acsl_eq_6 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(&a[3]) == sizeof(a)",25);
+ __gmpz_clear(__e_acsl_block_length_14);
+ __gmpz_clear(__e_acsl_sizeof_5);
+ }
+ /*@ assert \block_length(pa) ≡ sizeof(a); */
+ {
+ unsigned long __e_acsl_block_length_15;
+ mpz_t __e_acsl_block_length_16;
+ mpz_t __e_acsl_sizeof_6;
+ int __e_acsl_eq_7;
+ __e_acsl_block_length_15 = __block_length((void *)pa);
+ __gmpz_init_set_ui(__e_acsl_block_length_16,__e_acsl_block_length_15);
+ __gmpz_init_set_si(__e_acsl_sizeof_6,16L);
+ __e_acsl_eq_7 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_16),
+ (__mpz_struct const *)(__e_acsl_sizeof_6));
+ __e_acsl_assert(__e_acsl_eq_7 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(pa) == sizeof(a)",26);
+ __gmpz_clear(__e_acsl_block_length_16);
+ __gmpz_clear(__e_acsl_sizeof_6);
+ }
+ __full_init((void *)(& pa));
+ pa ++;
+ /*@ assert \block_length(pa+1) ≡ \block_length(&a[1]); */
+ {
+ unsigned long __e_acsl_block_length_17;
+ mpz_t __e_acsl_block_length_18;
+ unsigned long __e_acsl_block_length_19;
+ mpz_t __e_acsl_block_length_20;
+ int __e_acsl_eq_8;
+ __e_acsl_block_length_17 = __block_length((void *)(pa + 1));
+ __gmpz_init_set_ui(__e_acsl_block_length_18,__e_acsl_block_length_17);
+ __e_acsl_block_length_19 = __block_length((void *)(& a[1]));
+ __gmpz_init_set_ui(__e_acsl_block_length_20,__e_acsl_block_length_19);
+ __e_acsl_eq_8 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_18),
+ (__mpz_struct const *)(__e_acsl_block_length_20));
+ __e_acsl_assert(__e_acsl_eq_8 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(pa+1) == \\block_length(&a[1])",
+ 28);
+ __gmpz_clear(__e_acsl_block_length_18);
+ __gmpz_clear(__e_acsl_block_length_20);
+ }
+ __full_init((void *)(& l));
+ l = (long)4;
+ __full_init((void *)(& pl));
+ pl = (char *)(& l);
+ /*@ assert \block_length(&l) ≡ sizeof(long); */
+ {
+ unsigned long __e_acsl_block_length_21;
+ mpz_t __e_acsl_block_length_22;
+ mpz_t __e_acsl_sizeof_7;
+ int __e_acsl_eq_9;
+ __e_acsl_block_length_21 = __block_length((void *)(& l));
+ __gmpz_init_set_ui(__e_acsl_block_length_22,__e_acsl_block_length_21);
+ __gmpz_init_set_si(__e_acsl_sizeof_7,8L);
+ __e_acsl_eq_9 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_22),
+ (__mpz_struct const *)(__e_acsl_sizeof_7));
+ __e_acsl_assert(__e_acsl_eq_9 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(&l) == sizeof(long)",34);
+ __gmpz_clear(__e_acsl_block_length_22);
+ __gmpz_clear(__e_acsl_sizeof_7);
+ }
+ /*@ assert \block_length(pl) ≡ sizeof(long); */
+ {
+ unsigned long __e_acsl_block_length_23;
+ mpz_t __e_acsl_block_length_24;
+ mpz_t __e_acsl_sizeof_8;
+ int __e_acsl_eq_10;
+ __e_acsl_block_length_23 = __block_length((void *)pl);
+ __gmpz_init_set_ui(__e_acsl_block_length_24,__e_acsl_block_length_23);
+ __gmpz_init_set_si(__e_acsl_sizeof_8,8L);
+ __e_acsl_eq_10 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_24),
+ (__mpz_struct const *)(__e_acsl_sizeof_8));
+ __e_acsl_assert(__e_acsl_eq_10 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(pl) == sizeof(long)",35);
+ __gmpz_clear(__e_acsl_block_length_24);
+ __gmpz_clear(__e_acsl_sizeof_8);
+ }
+ /*@ assert \block_length(pl+7) ≡ sizeof(long); */
+ {
+ unsigned long __e_acsl_block_length_25;
+ mpz_t __e_acsl_block_length_26;
+ mpz_t __e_acsl_sizeof_9;
+ int __e_acsl_eq_11;
+ __e_acsl_block_length_25 = __block_length((void *)(pl + 7));
+ __gmpz_init_set_ui(__e_acsl_block_length_26,__e_acsl_block_length_25);
+ __gmpz_init_set_si(__e_acsl_sizeof_9,8L);
+ __e_acsl_eq_11 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_26),
+ (__mpz_struct const *)(__e_acsl_sizeof_9));
+ __e_acsl_assert(__e_acsl_eq_11 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(pl+7) == sizeof(long)",36);
+ __gmpz_clear(__e_acsl_block_length_26);
+ __gmpz_clear(__e_acsl_sizeof_9);
+ }
+ __full_init((void *)(& pi));
+ pi = (int *)(& l);
+ /*@ assert \block_length(pi) ≡ \block_length(&l); */
+ {
+ unsigned long __e_acsl_block_length_27;
+ mpz_t __e_acsl_block_length_28;
+ unsigned long __e_acsl_block_length_29;
+ mpz_t __e_acsl_block_length_30;
+ int __e_acsl_eq_12;
+ __e_acsl_block_length_27 = __block_length((void *)pi);
+ __gmpz_init_set_ui(__e_acsl_block_length_28,__e_acsl_block_length_27);
+ __e_acsl_block_length_29 = __block_length((void *)(& l));
+ __gmpz_init_set_ui(__e_acsl_block_length_30,__e_acsl_block_length_29);
+ __e_acsl_eq_12 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_28),
+ (__mpz_struct const *)(__e_acsl_block_length_30));
+ __e_acsl_assert(__e_acsl_eq_12 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(pi) == \\block_length(&l)",38);
+ __gmpz_clear(__e_acsl_block_length_28);
+ __gmpz_clear(__e_acsl_block_length_30);
+ }
+ __full_init((void *)(& pi));
+ pi ++;
+ /*@ assert \block_length(pi) ≡ \block_length(&l); */
+ {
+ unsigned long __e_acsl_block_length_31;
+ mpz_t __e_acsl_block_length_32;
+ unsigned long __e_acsl_block_length_33;
+ mpz_t __e_acsl_block_length_34;
+ int __e_acsl_eq_13;
+ __e_acsl_block_length_31 = __block_length((void *)pi);
+ __gmpz_init_set_ui(__e_acsl_block_length_32,__e_acsl_block_length_31);
+ __e_acsl_block_length_33 = __block_length((void *)(& l));
+ __gmpz_init_set_ui(__e_acsl_block_length_34,__e_acsl_block_length_33);
+ __e_acsl_eq_13 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_32),
+ (__mpz_struct const *)(__e_acsl_block_length_34));
+ __e_acsl_assert(__e_acsl_eq_13 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(pi) == \\block_length(&l)",40);
+ __gmpz_clear(__e_acsl_block_length_32);
+ __gmpz_clear(__e_acsl_block_length_34);
+ }
+ size = (unsigned long)12;
+ __full_init((void *)(& p));
+ p = (char *)__e_acsl_malloc(size);
+ /*@ assert \block_length(p) ≡ size; */
+ {
+ unsigned long __e_acsl_block_length_35;
+ mpz_t __e_acsl_block_length_36;
+ mpz_t __e_acsl_size;
+ int __e_acsl_eq_14;
+ __e_acsl_block_length_35 = __block_length((void *)p);
+ __gmpz_init_set_ui(__e_acsl_block_length_36,__e_acsl_block_length_35);
+ __gmpz_init_set_ui(__e_acsl_size,size);
+ __e_acsl_eq_14 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_36),
+ (__mpz_struct const *)(__e_acsl_size));
+ __e_acsl_assert(__e_acsl_eq_14 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(p) == size",45);
+ __gmpz_clear(__e_acsl_block_length_36);
+ __gmpz_clear(__e_acsl_size);
+ }
+ /*@ assert \block_length(p+11) ≡ size; */
+ {
+ unsigned long __e_acsl_block_length_37;
+ mpz_t __e_acsl_block_length_38;
+ mpz_t __e_acsl_size_2;
+ int __e_acsl_eq_15;
+ __e_acsl_block_length_37 = __block_length((void *)(p + 11));
+ __gmpz_init_set_ui(__e_acsl_block_length_38,__e_acsl_block_length_37);
+ __gmpz_init_set_ui(__e_acsl_size_2,size);
+ __e_acsl_eq_15 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_38),
+ (__mpz_struct const *)(__e_acsl_size_2));
+ __e_acsl_assert(__e_acsl_eq_15 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(p+11) == size",46);
+ __gmpz_clear(__e_acsl_block_length_38);
+ __gmpz_clear(__e_acsl_size_2);
+ }
+ __full_init((void *)(& p));
+ p += 5;
+ /*@ assert \block_length(p+5) ≡ \block_length(p-5); */
+ {
+ unsigned long __e_acsl_block_length_39;
+ mpz_t __e_acsl_block_length_40;
+ unsigned long __e_acsl_block_length_41;
+ mpz_t __e_acsl_block_length_42;
+ int __e_acsl_eq_16;
+ __e_acsl_block_length_39 = __block_length((void *)(p + 5));
+ __gmpz_init_set_ui(__e_acsl_block_length_40,__e_acsl_block_length_39);
+ __e_acsl_block_length_41 = __block_length((void *)(p - 5));
+ __gmpz_init_set_ui(__e_acsl_block_length_42,__e_acsl_block_length_41);
+ __e_acsl_eq_16 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_40),
+ (__mpz_struct const *)(__e_acsl_block_length_42));
+ __e_acsl_assert(__e_acsl_eq_16 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(p+5) == \\block_length(p-5)",48);
+ __gmpz_clear(__e_acsl_block_length_40);
+ __gmpz_clear(__e_acsl_block_length_42);
+ }
+ size = (unsigned long)30 * sizeof(long);
+ __full_init((void *)(& q));
+ q = (long *)__e_acsl_malloc(size);
+ /*@ assert \block_length(q) ≡ size; */
+ {
+ unsigned long __e_acsl_block_length_43;
+ mpz_t __e_acsl_block_length_44;
+ mpz_t __e_acsl_size_3;
+ int __e_acsl_eq_17;
+ __e_acsl_block_length_43 = __block_length((void *)q);
+ __gmpz_init_set_ui(__e_acsl_block_length_44,__e_acsl_block_length_43);
+ __gmpz_init_set_ui(__e_acsl_size_3,size);
+ __e_acsl_eq_17 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_44),
+ (__mpz_struct const *)(__e_acsl_size_3));
+ __e_acsl_assert(__e_acsl_eq_17 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(q) == size",54);
+ __gmpz_clear(__e_acsl_block_length_44);
+ __gmpz_clear(__e_acsl_size_3);
+ }
+ __full_init((void *)(& q));
+ q += 4;
+ /*@ assert \block_length(q) ≡ size; */
+ {
+ unsigned long __e_acsl_block_length_45;
+ mpz_t __e_acsl_block_length_46;
+ mpz_t __e_acsl_size_4;
+ int __e_acsl_eq_18;
+ __e_acsl_block_length_45 = __block_length((void *)q);
+ __gmpz_init_set_ui(__e_acsl_block_length_46,__e_acsl_block_length_45);
+ __gmpz_init_set_ui(__e_acsl_size_4,size);
+ __e_acsl_eq_18 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_46),
+ (__mpz_struct const *)(__e_acsl_size_4));
+ __e_acsl_assert(__e_acsl_eq_18 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(q) == size",56);
+ __gmpz_clear(__e_acsl_block_length_46);
+ __gmpz_clear(__e_acsl_size_4);
+ }
+ /*@ assert \block_length(&ZERO) ≡ 0; */
+ {
+ unsigned long __e_acsl_block_length_47;
+ mpz_t __e_acsl_block_length_48;
+ mpz_t __e_acsl;
+ int __e_acsl_eq_19;
+ __e_acsl_block_length_47 = __block_length((void *)(& ZERO));
+ __gmpz_init_set_ui(__e_acsl_block_length_48,__e_acsl_block_length_47);
+ __gmpz_init_set_si(__e_acsl,(long)0);
+ __e_acsl_eq_19 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_48),
+ (__mpz_struct const *)(__e_acsl));
+ __e_acsl_assert(__e_acsl_eq_19 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(&ZERO) == 0",60);
+ __gmpz_clear(__e_acsl_block_length_48);
+ __gmpz_clear(__e_acsl);
+ }
+ /*@ assert \block_length(&zero) ≡ 0; */
+ {
+ unsigned long __e_acsl_block_length_49;
+ mpz_t __e_acsl_block_length_50;
+ mpz_t __e_acsl_2;
+ int __e_acsl_eq_20;
+ __e_acsl_block_length_49 = __block_length((void *)(& zero));
+ __gmpz_init_set_ui(__e_acsl_block_length_50,__e_acsl_block_length_49);
+ __gmpz_init_set_si(__e_acsl_2,(long)0);
+ __e_acsl_eq_20 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_block_length_50),
+ (__mpz_struct const *)(__e_acsl_2));
+ __e_acsl_assert(__e_acsl_eq_20 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"\\block_length(&zero) == 0",61);
+ __gmpz_clear(__e_acsl_block_length_50);
+ __gmpz_clear(__e_acsl_2);
+ }
+ __retres = 0;
+ __delete_block((void *)(& ZERO));
+ __delete_block((void *)(& PA));
+ __delete_block((void *)(A));
+ __delete_block((void *)(& zero));
+ __delete_block((void *)(& q));
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& pi));
+ __delete_block((void *)(& pl));
+ __delete_block((void *)(& l));
+ __delete_block((void *)(& pa));
+ __delete_block((void *)(a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+