From f14e917cd2ea23ecca419a1abe115eefd50fbd62 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 13 Nov 2020 10:38:24 +0100
Subject: [PATCH] [eacsl] Update tests
---
src/plugins/e-acsl/tests/memory/initialized.c | 46 +++
.../tests/memory/oracle_ci/gen_initialized.c | 322 +++++++++++++++++-
.../memory/oracle_ci/gen_struct_initialized.c | 147 ++++++++
.../oracle_ci/struct_initialized.res.oracle | 2 +
.../struct_initialized.e-acsl.err.log | 0
.../e-acsl/tests/memory/struct_initialized.c | 35 ++
6 files changed, 544 insertions(+), 8 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle
create mode 100644 src/plugins/e-acsl/tests/memory/oracle_dev/struct_initialized.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/memory/struct_initialized.c
diff --git a/src/plugins/e-acsl/tests/memory/initialized.c b/src/plugins/e-acsl/tests/memory/initialized.c
index 4af4918caa2..34f53edb19e 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 2fc7f4ff024..dec94db6533 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 00000000000..1e1047dc8b4
--- /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 00000000000..efd02631129
--- /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 00000000000..e69de29bb2d
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 00000000000..87ee96337d2
--- /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);
+ }
+}
--
GitLab