diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index cdc707e9ec8846a5a4fafcc30d86d28541dfc968..8f683ce6a6a8cc08073ac168759770839f8856a4 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -29,6 +29,8 @@ Plugin E-ACSL <next-release>
Plugin E-ACSL 22.0 (Titanium)
#############################
+-* E-ACSL [2020-11-16] Fix soundness bug when checking
+ initialization of a chunk of heap memory block.
- E-ACSL [2020-10-14] Add Support for Variadic generated functions in
the AST (frama-c/e-acsl#128).
- E-ACSL [2020-10-06] Add support for the `\separated` predicate.
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index 083d015a3016899debff7f46273890665e035425..852f1447084e3b2569b4c28eb681abfe3f7bb06b 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -744,19 +744,76 @@ void* realloc(void *ptr, size_t size) {
* shadow block to the size of the new allocation */
if (old_size > size) {
clearbits_right(
- old_alloc_size - size,
- old_init_shadow + old_alloc_size/8);
+ old_alloc_size - size, // size in bits
+ old_init_shadow + old_alloc_size/8); // end of the old init shadow
}
- /* Now init shadow can be moved (if needed), keep in mind that
- * segment base addresses are aligned at a boundary of something
- * divisible by 8, so instead of moving actual bits here the
- * segments are moved to avoid dealing with bit-level operations
- * on incomplete bytes. */
+ /* Keep in mind that there is a ratio of 8 between the actual heap
+ * memory and the init shadow memory. So a byte in the actual memory
+ * corresponds to a bit in the shadow memory.
+ */
+
+ /* We need to keep the status of the init shadow up to `old_size` bits
+ * (or `size` if `size < old_size`), and we need to make sure that the
+ * bits of the init shadow correspondings to the bytes between
+ * `old_size` and `size` are set to zero if `size > old_size`. */
+
+ /* First of all, determine the number of bits in the init shadow that
+ * must be kept */
+ size_t keep_bits = (size < old_size) ? size : old_size;
+
+ /* To avoid doing too much bitwise operations, separate this size in
+ * the amount of bytes of init shadow that must be kept including any
+ * incomplete byte, and the number of bits that must be kept in the last
+ * byte if it is incomplete */
+ size_t rem_keep_bits = keep_bits%8;
+ size_t keep_bytes = keep_bits/8 + (rem_keep_bits > 0 ? 1 : 0);
+
+ /* If the pointer has been moved, then we need to copy `keep_bytes`
+ * from the old shadow to the new shadow to carry over all the needed
+ * information. Then the old init shadow can be reset. */
if (res != ptr) {
- size_t copy_size = (old_size > size) ? alloc_size : old_alloc_size;
- memcpy(new_init_shadow, old_init_shadow, copy_size);
- memset(old_init_shadow, 0, copy_size);
+ DVASSERT(keep_bytes <= alloc_size/8 && keep_bytes < old_alloc_size/8,
+ "Attempt to access out of bound init shadow. Accessing %lu bytes, \
+ old init shadow size: %lu bytes, new init shadow size: %lu bytes.",
+ keep_bytes, old_alloc_size/8, alloc_size/8);
+ memcpy(new_init_shadow, old_init_shadow, keep_bytes);
+ memset(old_init_shadow, 0, old_alloc_size/8);
+ }
+
+ if (size > old_size) {
+ // Last kept byte index
+ size_t idx = keep_bytes - 1; // idx < init_shadow_size by construction
+
+ /* If the new size is greater than the old size and the last kept byte
+ * is incomplete (`rem_keep_bits > 0`), then reset the unkept bits of
+ * the last byte in the new init shadow */
+ if (rem_keep_bits > 0) {
+ DVASSERT(idx < alloc_size/8,
+ "Attempt to access out of bound init shadow. Accessing index %lu \
+ with init shadow of size %lu bytes.", idx, alloc_size/8);
+ unsigned char mask = 0;
+ setbits64(rem_keep_bits, mask);
+ *(new_init_shadow + idx) &= mask;
+ }
+
+ /* Finally, if the new size is greater than the old size and the
+ * pointer hasn't been moved, then we need to make sure that the
+ * remaining bits of the init shadow corresponding to the memory
+ * between `old_size` and `size` are set to zero. */
+ if (res == ptr) {
+ // Index of the byte after the last kept byte
+ ++idx;
+ // Number of bytes between the index and the end of the init
+ // shadow corresponding to the new allocated memory
+ size_t count = size/8 - idx;
+
+ DVASSERT((idx+count) <= alloc_size/8,
+ "Attempt to access out of bound init shadow. Accessing %lu bytes \
+ from index %lu with init shadow of size %lu bytes.",
+ count, idx, alloc_size/8);
+ memset(new_init_shadow+idx, 0, count);
+ }
}
}
} else {
@@ -895,7 +952,7 @@ int heap_initialized(uintptr_t addr, long len) {
unsigned char mask = 0;
setbits64_skip(set,mask,skip);
- if (*shadow != mask)
+ if ((*shadow & mask) != mask)
return 0;
}
if (len > 0)
diff --git a/src/plugins/e-acsl/tests/memory/initialized.c b/src/plugins/e-acsl/tests/memory/initialized.c
index 4af4918caa2b7445e02f84fe3e115ef369e3f150..34f53edb19e059c2a8ff498d9e54d9c052536f36 100644
--- a/src/plugins/e-acsl/tests/memory/initialized.c
+++ b/src/plugins/e-acsl/tests/memory/initialized.c
@@ -84,6 +84,52 @@ int main(void) {
/*@assert ! \initialized(p); */
/*@assert ! \initialized(q); */
+ /* Specially crafted calloc and realloc calls to check corner cases of
+ * initialization */
+ q = calloc(3, sizeof(int));
+ /*@ assert \initialized(&q[0..2]); */
+ q = realloc(q, 6 * sizeof(int));
+ /*@ assert \initialized(&q[0..2]); */
+ /*@ assert ! \initialized(&q[3]); */
+ /*@ assert ! \initialized(&q[4]); */
+ /*@ assert ! \initialized(&q[5]); */
+ free(q);
+ q = calloc(7, sizeof(int));
+ /*@ assert \initialized(&q[0..6]); */
+ q = realloc(q, 8 * sizeof(int));
+ /*@ assert \initialized(&q[0..6]); */
+ /*@ assert ! \initialized(&q[7]); */
+ q = realloc(q, 10 * sizeof(int));
+ /*@ assert \initialized(&q[0..6]); */
+ /*@ assert ! \initialized(&q[7]); */
+ /*@ assert ! \initialized(&q[8]); */
+ /*@ assert ! \initialized(&q[9]); */
+ free(q);
+ q = calloc(2, sizeof(int));
+ /*@ assert \initialized(&q[0..1]); */
+ q = realloc(q, 4 * sizeof(int));
+ /*@ assert \initialized(&q[0..1]); */
+ /*@ assert ! \initialized(&q[2]); */
+ /*@ assert ! \initialized(&q[3]); */
+ free(q);
+ q = calloc(6, sizeof(int));
+ /*@ assert \initialized(&q[0..5]); */
+ q = realloc(q, 3 * sizeof(int));
+ /*@ assert \initialized(&q[0..2]); */
+ free(q);
+ q = malloc(6 * sizeof(int));
+ /*@ assert ! \initialized(&q[0]); */
+ /*@ assert ! \initialized(&q[1]); */
+ /*@ assert ! \initialized(&q[2]); */
+ /*@ assert ! \initialized(&q[3]); */
+ /*@ assert ! \initialized(&q[4]); */
+ /*@ assert ! \initialized(&q[5]); */
+ q = realloc(q, 3 * sizeof(int));
+ /*@ assert ! \initialized(&q[0]); */
+ /*@ assert ! \initialized(&q[1]); */
+ /*@ assert ! \initialized(&q[2]); */
+ free(q);
+
/* Spoofing access to a non-existing stack address */
q = (int*)(&q - 1024*5);
/*assert ! \initialized(q); */
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
index 2fc7f4ff02452f9cf5ec262dc1a11a7dff556df0..dec94db6533f1ddb8db1ab53e6913dab01393817 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
@@ -319,23 +319,329 @@ int main(void)
}
/*@ assert ¬\initialized(q); */ ;
__e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)3,sizeof(int));
+ {
+ int __gen_e_acsl_size;
+ int __gen_e_acsl_if;
+ int __gen_e_acsl_initialized_32;
+ __gen_e_acsl_size = 4 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size <= 0) __gen_e_acsl_if = 0;
+ else __gen_e_acsl_if = __gen_e_acsl_size;
+ __gen_e_acsl_initialized_32 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if);
+ __e_acsl_assert(__gen_e_acsl_initialized_32,"Assertion","main",
+ "\\initialized(q + (0 .. 2))",
+ "tests/memory/initialized.c",90);
+ }
+ /*@ assert \initialized(q + (0 .. 2)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)6 * sizeof(int));
+ {
+ int __gen_e_acsl_size_2;
+ int __gen_e_acsl_if_2;
+ int __gen_e_acsl_initialized_33;
+ __gen_e_acsl_size_2 = 4 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_2 <= 0) __gen_e_acsl_if_2 = 0;
+ else __gen_e_acsl_if_2 = __gen_e_acsl_size_2;
+ __gen_e_acsl_initialized_33 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_2);
+ __e_acsl_assert(__gen_e_acsl_initialized_33,"Assertion","main",
+ "\\initialized(q + (0 .. 2))",
+ "tests/memory/initialized.c",92);
+ }
+ /*@ assert \initialized(q + (0 .. 2)); */ ;
+ {
+ int __gen_e_acsl_initialized_34;
+ __gen_e_acsl_initialized_34 = __e_acsl_initialized((void *)(q + 3),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_34,"Assertion","main",
+ "!\\initialized(q + 3)","tests/memory/initialized.c",93);
+ }
+ /*@ assert ¬\initialized(q + 3); */ ;
+ {
+ int __gen_e_acsl_initialized_35;
+ __gen_e_acsl_initialized_35 = __e_acsl_initialized((void *)(q + 4),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_35,"Assertion","main",
+ "!\\initialized(q + 4)","tests/memory/initialized.c",94);
+ }
+ /*@ assert ¬\initialized(q + 4); */ ;
+ {
+ int __gen_e_acsl_initialized_36;
+ __gen_e_acsl_initialized_36 = __e_acsl_initialized((void *)(q + 5),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_36,"Assertion","main",
+ "!\\initialized(q + 5)","tests/memory/initialized.c",95);
+ }
+ /*@ assert ¬\initialized(q + 5); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)7,sizeof(int));
+ {
+ int __gen_e_acsl_size_3;
+ int __gen_e_acsl_if_3;
+ int __gen_e_acsl_initialized_37;
+ __gen_e_acsl_size_3 = 4 * ((6 - 0) + 1);
+ if (__gen_e_acsl_size_3 <= 0) __gen_e_acsl_if_3 = 0;
+ else __gen_e_acsl_if_3 = __gen_e_acsl_size_3;
+ __gen_e_acsl_initialized_37 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_3);
+ __e_acsl_assert(__gen_e_acsl_initialized_37,"Assertion","main",
+ "\\initialized(q + (0 .. 6))",
+ "tests/memory/initialized.c",98);
+ }
+ /*@ assert \initialized(q + (0 .. 6)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)8 * sizeof(int));
+ {
+ int __gen_e_acsl_size_4;
+ int __gen_e_acsl_if_4;
+ int __gen_e_acsl_initialized_38;
+ __gen_e_acsl_size_4 = 4 * ((6 - 0) + 1);
+ if (__gen_e_acsl_size_4 <= 0) __gen_e_acsl_if_4 = 0;
+ else __gen_e_acsl_if_4 = __gen_e_acsl_size_4;
+ __gen_e_acsl_initialized_38 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_4);
+ __e_acsl_assert(__gen_e_acsl_initialized_38,"Assertion","main",
+ "\\initialized(q + (0 .. 6))",
+ "tests/memory/initialized.c",100);
+ }
+ /*@ assert \initialized(q + (0 .. 6)); */ ;
+ {
+ int __gen_e_acsl_initialized_39;
+ __gen_e_acsl_initialized_39 = __e_acsl_initialized((void *)(q + 7),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_39,"Assertion","main",
+ "!\\initialized(q + 7)","tests/memory/initialized.c",101);
+ }
+ /*@ assert ¬\initialized(q + 7); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)10 * sizeof(int));
+ {
+ int __gen_e_acsl_size_5;
+ int __gen_e_acsl_if_5;
+ int __gen_e_acsl_initialized_40;
+ __gen_e_acsl_size_5 = 4 * ((6 - 0) + 1);
+ if (__gen_e_acsl_size_5 <= 0) __gen_e_acsl_if_5 = 0;
+ else __gen_e_acsl_if_5 = __gen_e_acsl_size_5;
+ __gen_e_acsl_initialized_40 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_5);
+ __e_acsl_assert(__gen_e_acsl_initialized_40,"Assertion","main",
+ "\\initialized(q + (0 .. 6))",
+ "tests/memory/initialized.c",103);
+ }
+ /*@ assert \initialized(q + (0 .. 6)); */ ;
+ {
+ int __gen_e_acsl_initialized_41;
+ __gen_e_acsl_initialized_41 = __e_acsl_initialized((void *)(q + 7),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_41,"Assertion","main",
+ "!\\initialized(q + 7)","tests/memory/initialized.c",104);
+ }
+ /*@ assert ¬\initialized(q + 7); */ ;
+ {
+ int __gen_e_acsl_initialized_42;
+ __gen_e_acsl_initialized_42 = __e_acsl_initialized((void *)(q + 8),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_42,"Assertion","main",
+ "!\\initialized(q + 8)","tests/memory/initialized.c",105);
+ }
+ /*@ assert ¬\initialized(q + 8); */ ;
+ {
+ int __gen_e_acsl_initialized_43;
+ __gen_e_acsl_initialized_43 = __e_acsl_initialized((void *)(q + 9),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_43,"Assertion","main",
+ "!\\initialized(q + 9)","tests/memory/initialized.c",106);
+ }
+ /*@ assert ¬\initialized(q + 9); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)2,sizeof(int));
+ {
+ int __gen_e_acsl_size_6;
+ int __gen_e_acsl_if_6;
+ int __gen_e_acsl_initialized_44;
+ __gen_e_acsl_size_6 = 4 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_6 <= 0) __gen_e_acsl_if_6 = 0;
+ else __gen_e_acsl_if_6 = __gen_e_acsl_size_6;
+ __gen_e_acsl_initialized_44 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_6);
+ __e_acsl_assert(__gen_e_acsl_initialized_44,"Assertion","main",
+ "\\initialized(q + (0 .. 1))",
+ "tests/memory/initialized.c",109);
+ }
+ /*@ assert \initialized(q + (0 .. 1)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)4 * sizeof(int));
+ {
+ int __gen_e_acsl_size_7;
+ int __gen_e_acsl_if_7;
+ int __gen_e_acsl_initialized_45;
+ __gen_e_acsl_size_7 = 4 * ((1 - 0) + 1);
+ if (__gen_e_acsl_size_7 <= 0) __gen_e_acsl_if_7 = 0;
+ else __gen_e_acsl_if_7 = __gen_e_acsl_size_7;
+ __gen_e_acsl_initialized_45 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_7);
+ __e_acsl_assert(__gen_e_acsl_initialized_45,"Assertion","main",
+ "\\initialized(q + (0 .. 1))",
+ "tests/memory/initialized.c",111);
+ }
+ /*@ assert \initialized(q + (0 .. 1)); */ ;
+ {
+ int __gen_e_acsl_initialized_46;
+ __gen_e_acsl_initialized_46 = __e_acsl_initialized((void *)(q + 2),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_46,"Assertion","main",
+ "!\\initialized(q + 2)","tests/memory/initialized.c",112);
+ }
+ /*@ assert ¬\initialized(q + 2); */ ;
+ {
+ int __gen_e_acsl_initialized_47;
+ __gen_e_acsl_initialized_47 = __e_acsl_initialized((void *)(q + 3),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_47,"Assertion","main",
+ "!\\initialized(q + 3)","tests/memory/initialized.c",113);
+ }
+ /*@ assert ¬\initialized(q + 3); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)calloc((unsigned long)6,sizeof(int));
+ {
+ int __gen_e_acsl_size_8;
+ int __gen_e_acsl_if_8;
+ int __gen_e_acsl_initialized_48;
+ __gen_e_acsl_size_8 = 4 * ((5 - 0) + 1);
+ if (__gen_e_acsl_size_8 <= 0) __gen_e_acsl_if_8 = 0;
+ else __gen_e_acsl_if_8 = __gen_e_acsl_size_8;
+ __gen_e_acsl_initialized_48 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_8);
+ __e_acsl_assert(__gen_e_acsl_initialized_48,"Assertion","main",
+ "\\initialized(q + (0 .. 5))",
+ "tests/memory/initialized.c",116);
+ }
+ /*@ assert \initialized(q + (0 .. 5)); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)3 * sizeof(int));
+ {
+ int __gen_e_acsl_size_9;
+ int __gen_e_acsl_if_9;
+ int __gen_e_acsl_initialized_49;
+ __gen_e_acsl_size_9 = 4 * ((2 - 0) + 1);
+ if (__gen_e_acsl_size_9 <= 0) __gen_e_acsl_if_9 = 0;
+ else __gen_e_acsl_if_9 = __gen_e_acsl_size_9;
+ __gen_e_acsl_initialized_49 = __e_acsl_initialized((void *)((char *)q +
+ 4 * 0),
+ (size_t)__gen_e_acsl_if_9);
+ __e_acsl_assert(__gen_e_acsl_initialized_49,"Assertion","main",
+ "\\initialized(q + (0 .. 2))",
+ "tests/memory/initialized.c",118);
+ }
+ /*@ assert \initialized(q + (0 .. 2)); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)malloc((unsigned long)6 * sizeof(int));
+ {
+ int __gen_e_acsl_initialized_50;
+ __gen_e_acsl_initialized_50 = __e_acsl_initialized((void *)(q + 0),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_50,"Assertion","main",
+ "!\\initialized(q + 0)","tests/memory/initialized.c",121);
+ }
+ /*@ assert ¬\initialized(q + 0); */ ;
+ {
+ int __gen_e_acsl_initialized_51;
+ __gen_e_acsl_initialized_51 = __e_acsl_initialized((void *)(q + 1),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_51,"Assertion","main",
+ "!\\initialized(q + 1)","tests/memory/initialized.c",122);
+ }
+ /*@ assert ¬\initialized(q + 1); */ ;
+ {
+ int __gen_e_acsl_initialized_52;
+ __gen_e_acsl_initialized_52 = __e_acsl_initialized((void *)(q + 2),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_52,"Assertion","main",
+ "!\\initialized(q + 2)","tests/memory/initialized.c",123);
+ }
+ /*@ assert ¬\initialized(q + 2); */ ;
+ {
+ int __gen_e_acsl_initialized_53;
+ __gen_e_acsl_initialized_53 = __e_acsl_initialized((void *)(q + 3),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_53,"Assertion","main",
+ "!\\initialized(q + 3)","tests/memory/initialized.c",124);
+ }
+ /*@ assert ¬\initialized(q + 3); */ ;
+ {
+ int __gen_e_acsl_initialized_54;
+ __gen_e_acsl_initialized_54 = __e_acsl_initialized((void *)(q + 4),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_54,"Assertion","main",
+ "!\\initialized(q + 4)","tests/memory/initialized.c",125);
+ }
+ /*@ assert ¬\initialized(q + 4); */ ;
+ {
+ int __gen_e_acsl_initialized_55;
+ __gen_e_acsl_initialized_55 = __e_acsl_initialized((void *)(q + 5),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_55,"Assertion","main",
+ "!\\initialized(q + 5)","tests/memory/initialized.c",126);
+ }
+ /*@ assert ¬\initialized(q + 5); */ ;
+ __e_acsl_full_init((void *)(& q));
+ q = (int *)realloc((void *)q,(unsigned long)3 * sizeof(int));
+ {
+ int __gen_e_acsl_initialized_56;
+ __gen_e_acsl_initialized_56 = __e_acsl_initialized((void *)(q + 0),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_56,"Assertion","main",
+ "!\\initialized(q + 0)","tests/memory/initialized.c",128);
+ }
+ /*@ assert ¬\initialized(q + 0); */ ;
+ {
+ int __gen_e_acsl_initialized_57;
+ __gen_e_acsl_initialized_57 = __e_acsl_initialized((void *)(q + 1),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_57,"Assertion","main",
+ "!\\initialized(q + 1)","tests/memory/initialized.c",129);
+ }
+ /*@ assert ¬\initialized(q + 1); */ ;
+ {
+ int __gen_e_acsl_initialized_58;
+ __gen_e_acsl_initialized_58 = __e_acsl_initialized((void *)(q + 2),
+ sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_58,"Assertion","main",
+ "!\\initialized(q + 2)","tests/memory/initialized.c",130);
+ }
+ /*@ assert ¬\initialized(q + 2); */ ;
+ free((void *)q);
+ __e_acsl_full_init((void *)(& q));
q = (int *)(& q - 1024 * 5);
__e_acsl_full_init((void *)(& q));
q = (int *)128;
{
- int __gen_e_acsl_initialized_32;
- __gen_e_acsl_initialized_32 = __e_acsl_initialized((void *)q,sizeof(int));
- __e_acsl_assert(! __gen_e_acsl_initialized_32,"Assertion","main",
- "!\\initialized(q)","tests/memory/initialized.c",93);
+ int __gen_e_acsl_initialized_59;
+ __gen_e_acsl_initialized_59 = __e_acsl_initialized((void *)q,sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_59,"Assertion","main",
+ "!\\initialized(q)","tests/memory/initialized.c",139);
}
/*@ assert ¬\initialized(q); */ ;
__e_acsl_full_init((void *)(& p));
p = (int *)0;
{
- int __gen_e_acsl_initialized_33;
- __gen_e_acsl_initialized_33 = __e_acsl_initialized((void *)p,sizeof(int));
- __e_acsl_assert(! __gen_e_acsl_initialized_33,"Assertion","main",
- "!\\initialized(p)","tests/memory/initialized.c",96);
+ int __gen_e_acsl_initialized_60;
+ __gen_e_acsl_initialized_60 = __e_acsl_initialized((void *)p,sizeof(int));
+ __e_acsl_assert(! __gen_e_acsl_initialized_60,"Assertion","main",
+ "!\\initialized(p)","tests/memory/initialized.c",142);
}
/*@ assert ¬\initialized(p); */ ;
int size = 100;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c
new file mode 100644
index 0000000000000000000000000000000000000000..1e1047dc8b47a51c32345364e5bcb7c37dcf6ee8
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c
@@ -0,0 +1,147 @@
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "stdlib.h"
+struct __anonstruct_int32_pair_t_1 {
+ int32_t a ;
+ int32_t b ;
+};
+typedef struct __anonstruct_int32_pair_t_1 int32_pair_t;
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ {
+ int32_pair_t static_pair;
+ __e_acsl_store_block((void *)(& static_pair),(size_t)8);
+ {
+ int __gen_e_acsl_initialized;
+ __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& static_pair.a),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized,"Assertion","main",
+ "!\\initialized(&static_pair.a)",
+ "tests/memory/struct_initialized.c",13);
+ }
+ /*@ assert ¬\initialized(&static_pair.a); */ ;
+ {
+ int __gen_e_acsl_initialized_2;
+ __gen_e_acsl_initialized_2 = __e_acsl_initialized((void *)(& static_pair.b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_2,"Assertion","main",
+ "!\\initialized(&static_pair.b)",
+ "tests/memory/struct_initialized.c",14);
+ }
+ /*@ assert ¬\initialized(&static_pair.b); */ ;
+ __e_acsl_initialize((void *)(& static_pair.a),sizeof(int32_t));
+ static_pair.a = 1;
+ {
+ int __gen_e_acsl_initialized_3;
+ __gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)(& static_pair.a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_3,"Assertion","main",
+ "\\initialized(&static_pair.a)",
+ "tests/memory/struct_initialized.c",16);
+ }
+ /*@ assert \initialized(&static_pair.a); */ ;
+ {
+ int __gen_e_acsl_initialized_4;
+ __gen_e_acsl_initialized_4 = __e_acsl_initialized((void *)(& static_pair.b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_4,"Assertion","main",
+ "!\\initialized(&static_pair.b)",
+ "tests/memory/struct_initialized.c",17);
+ }
+ /*@ assert ¬\initialized(&static_pair.b); */ ;
+ __e_acsl_initialize((void *)(& static_pair.b),sizeof(int32_t));
+ static_pair.b = 2;
+ {
+ int __gen_e_acsl_initialized_5;
+ __gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)(& static_pair.a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_5,"Assertion","main",
+ "\\initialized(&static_pair.a)",
+ "tests/memory/struct_initialized.c",19);
+ }
+ /*@ assert \initialized(&static_pair.a); */ ;
+ {
+ int __gen_e_acsl_initialized_6;
+ __gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)(& static_pair.b),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_6,"Assertion","main",
+ "\\initialized(&static_pair.b)",
+ "tests/memory/struct_initialized.c",20);
+ }
+ /*@ assert \initialized(&static_pair.b); */ ;
+ __e_acsl_delete_block((void *)(& static_pair));
+ }
+ {
+ int32_pair_t *heap_pair = malloc(sizeof(int32_pair_t));
+ __e_acsl_store_block((void *)(& heap_pair),(size_t)8);
+ __e_acsl_full_init((void *)(& heap_pair));
+ {
+ int __gen_e_acsl_initialized_7;
+ __gen_e_acsl_initialized_7 = __e_acsl_initialized((void *)(& heap_pair->a),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_7,"Assertion","main",
+ "!\\initialized(&heap_pair->a)",
+ "tests/memory/struct_initialized.c",26);
+ }
+ /*@ assert ¬\initialized(&heap_pair->a); */ ;
+ {
+ int __gen_e_acsl_initialized_8;
+ __gen_e_acsl_initialized_8 = __e_acsl_initialized((void *)(& heap_pair->b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_8,"Assertion","main",
+ "!\\initialized(&heap_pair->b)",
+ "tests/memory/struct_initialized.c",27);
+ }
+ /*@ assert ¬\initialized(&heap_pair->b); */ ;
+ __e_acsl_initialize((void *)(& heap_pair->a),sizeof(int32_t));
+ heap_pair->a = 3;
+ {
+ int __gen_e_acsl_initialized_9;
+ __gen_e_acsl_initialized_9 = __e_acsl_initialized((void *)(& heap_pair->a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_9,"Assertion","main",
+ "\\initialized(&heap_pair->a)",
+ "tests/memory/struct_initialized.c",29);
+ }
+ /*@ assert \initialized(&heap_pair->a); */ ;
+ {
+ int __gen_e_acsl_initialized_10;
+ __gen_e_acsl_initialized_10 = __e_acsl_initialized((void *)(& heap_pair->b),
+ sizeof(int32_t));
+ __e_acsl_assert(! __gen_e_acsl_initialized_10,"Assertion","main",
+ "!\\initialized(&heap_pair->b)",
+ "tests/memory/struct_initialized.c",30);
+ }
+ /*@ assert ¬\initialized(&heap_pair->b); */ ;
+ __e_acsl_initialize((void *)(& heap_pair->b),sizeof(int32_t));
+ heap_pair->b = 4;
+ {
+ int __gen_e_acsl_initialized_11;
+ __gen_e_acsl_initialized_11 = __e_acsl_initialized((void *)(& heap_pair->a),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_11,"Assertion","main",
+ "\\initialized(&heap_pair->a)",
+ "tests/memory/struct_initialized.c",32);
+ }
+ /*@ assert \initialized(&heap_pair->a); */ ;
+ {
+ int __gen_e_acsl_initialized_12;
+ __gen_e_acsl_initialized_12 = __e_acsl_initialized((void *)(& heap_pair->b),
+ sizeof(int32_t));
+ __e_acsl_assert(__gen_e_acsl_initialized_12,"Assertion","main",
+ "\\initialized(&heap_pair->b)",
+ "tests/memory/struct_initialized.c",33);
+ }
+ /*@ assert \initialized(&heap_pair->b); */ ;
+ __e_acsl_delete_block((void *)(& heap_pair));
+ }
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/struct_initialized.e-acsl.err.log b/src/plugins/e-acsl/tests/memory/oracle_dev/struct_initialized.e-acsl.err.log
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/memory/struct_initialized.c b/src/plugins/e-acsl/tests/memory/struct_initialized.c
new file mode 100644
index 0000000000000000000000000000000000000000..87ee96337d2ebfbddd575f46715f31fbd7b338d3
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/struct_initialized.c
@@ -0,0 +1,35 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+typedef struct {
+ int32_t a;
+ int32_t b;
+} int32_pair_t;
+
+int main() {
+ // Static alloc
+ {
+ int32_pair_t static_pair;
+ //@ assert !\initialized(&static_pair.a);
+ //@ assert !\initialized(&static_pair.b);
+ static_pair.a = 1;
+ //@ assert \initialized(&static_pair.a);
+ //@ assert !\initialized(&static_pair.b);
+ static_pair.b = 2;
+ //@ assert \initialized(&static_pair.a);
+ //@ assert \initialized(&static_pair.b);
+ }
+
+ // Dynamic alloc
+ {
+ int32_pair_t * heap_pair = malloc(sizeof(int32_pair_t));
+ //@ assert !\initialized(&heap_pair->a);
+ //@ assert !\initialized(&heap_pair->b);
+ heap_pair->a = 3;
+ //@ assert \initialized(&heap_pair->a);
+ //@ assert !\initialized(&heap_pair->b);
+ heap_pair->b = 4;
+ //@ assert \initialized(&heap_pair->a);
+ //@ assert \initialized(&heap_pair->b);
+ }
+}