From eb70f3508ccfc5965f0d73c4cea4724ddba183a8 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 23 Mar 2017 16:00:37 +0100
Subject: [PATCH] [tests] add test for local_init (without oracle for the time
being)
---
src/plugins/e-acsl/tests/runtime/local_init.c | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/runtime/local_init.c
diff --git a/src/plugins/e-acsl/tests/runtime/local_init.c b/src/plugins/e-acsl/tests/runtime/local_init.c
new file mode 100644
index 00000000000..f1affb77b1d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/runtime/local_init.c
@@ -0,0 +1,17 @@
+/* run.config
+ COMMENT: test of a local initializer which contains an annotation
+ STDOPT: #"-val -value-verbose 0 -lib-entry -e-acsl-prepare -machdep gcc_x86_64 -then"
+*/
+
+int X = 0;
+int *p = &X;
+
+int f(void) {
+ int x = *p; // Eva add an alarms on this statement
+ return x;
+}
+
+int main(void) {
+ f();
+ return 0;
+}
--
GitLab