From 0dc96aa6686dd75974a5a4a90413b87c85be082b Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 16 Mar 2016 14:29:48 +0100
Subject: [PATCH] [tests] Improved test case initialized to cover a bug in
partial initialization [ see 61afda4f1ba39f2b9ec5dff3c5cb118402457031 ]
---
src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c | 7 +++++++
.../e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c | 3 +++
2 files changed, 10 insertions(+)
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 88d367ba270..c4c5edec1f4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/initialized.c
@@ -116,4 +116,11 @@ int main(void) {
/* @assert ! \initialized(partsc + i); */
}
}
+
+ /* Check duplicate initialization does not affect correct count of
+ * initialized bits (relevant for ADT models only). */
+ int dup [2];
+ dup[0] = 1;
+ dup[0] = 1;
+ /* @assert ! \initialized(&dup); */
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
index bfcf7fe7b53..e0be4e27e9c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_initialized.c
@@ -23,6 +23,7 @@ int main(void)
int size;
char *partsc;
char *partsi;
+ int dup[2];
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
__e_acsl_globals_init();
__store_block((void *)(d),16UL);
@@ -333,6 +334,8 @@ int main(void)
i_0 ++;
}
}
+ dup[0] = 1;
+ dup[0] = 1;
__retres = 0;
__delete_block((void *)(& B));
__delete_block((void *)(& A));
--
GitLab