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 0000000000000000000000000000000000000000..74cf4d32f8f1dee4dac82aebaec6527cb6e6b452
--- /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;
+}