From 203c39ebdffd6ca76e6494e7b854d75b8b1a53cb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 26 Feb 2019 11:04:44 +0100
Subject: [PATCH] [doc] add missing example
---
.../e-acsl/doc/userman/examples/instrument.i | 19 +++++++++++++++++++
1 file changed, 19 insertions(+)
create mode 100644 src/plugins/e-acsl/doc/userman/examples/instrument.i
diff --git a/src/plugins/e-acsl/doc/userman/examples/instrument.i b/src/plugins/e-acsl/doc/userman/examples/instrument.i
new file mode 100644
index 00000000000..74cf4d32f8f
--- /dev/null
+++ b/src/plugins/e-acsl/doc/userman/examples/instrument.i
@@ -0,0 +1,19 @@
+void f(int *p) {
+ *p = 0;
+}
+
+void g(int *p) {
+ *p = 1;
+}
+
+int main(void) {
+ int t[3];
+ f(&t[0]);
+ /*@ assert \initialized(&t[0]); */
+ t[1] = 1;
+ g(&t[1]);
+ g(&t[2]);
+ /*@ assert \initialized(&t[1]); */
+ /*@ assert \initialized(&t[2]); */
+ return 0;
+}
--
GitLab