Commit 10445eae authored by Julien Signoles's avatar Julien Signoles

Merge branch 'bugfix/basile/eacsl-heap-init' into 'stable/titanium'

[eacsl] Fix heap initialization

See merge request frama-c/frama-c!2946
parents 5f45028b af732f72
......@@ -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.
......
......@@ -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)
......
......@@ -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); */
......
......@@ -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;
......
/* 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); */ ;