From d8322f28b3f03e3c1f9d33fb6e6d2a2be02583b0 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 4 Jan 2019 15:29:25 +0100
Subject: [PATCH] [Aorai] add two tests for metavariables initialization
---
.../aorai/tests/ya/metavariables-right.i | 28 ++++++++++++++++++
.../aorai/tests/ya/metavariables-right.ya | 29 +++++++++++++++++++
.../aorai/tests/ya/metavariables-wrong.i | 22 ++++++++++++++
.../aorai/tests/ya/metavariables-wrong.ya | 23 +++++++++++++++
.../ya/oracle/metavariables-right.res.oracle | 14 +++++++++
.../ya/oracle/metavariables-wrong.res.oracle | 4 +++
6 files changed, 120 insertions(+)
create mode 100644 src/plugins/aorai/tests/ya/metavariables-right.i
create mode 100644 src/plugins/aorai/tests/ya/metavariables-right.ya
create mode 100644 src/plugins/aorai/tests/ya/metavariables-wrong.i
create mode 100644 src/plugins/aorai/tests/ya/metavariables-wrong.ya
create mode 100644 src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
create mode 100644 src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
diff --git a/src/plugins/aorai/tests/ya/metavariables-right.i b/src/plugins/aorai/tests/ya/metavariables-right.i
new file mode 100644
index 00000000000..b79672a08cd
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/metavariables-right.i
@@ -0,0 +1,28 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+void f(int x) {}
+void g(void) {}
+void h(int x) {}
+void i(void) {}
+
+void main(int t)
+{
+ if (t) {
+ f(42);
+ }
+ else {
+ g();
+ goto L;
+ }
+
+ int x = 0;
+ while (x < 100)
+ {
+ h(x);
+ L: i();
+ x++;
+ }
+}
+
diff --git a/src/plugins/aorai/tests/ya/metavariables-right.ya b/src/plugins/aorai/tests/ya/metavariables-right.ya
new file mode 100644
index 00000000000..2e5be920ec1
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/metavariables-right.ya
@@ -0,0 +1,29 @@
+%init: a;
+%accept: i;
+%deterministic;
+
+$x : int;
+
+a : { CALL(main) } -> b;
+
+b :
+ { CALL(f) && $x := f().x } -> c
+| { CALL(g) } -> d
+;
+
+c : { RETURN(f) } -> e;
+
+d : { RETURN(g) } -> g;
+
+e :
+ { CALL(h) && $x > 0 } -> f
+| { RETURN(main) } -> i
+;
+
+f : { RETURN(h) } -> g;
+
+g : { CALL(i) } -> h;
+
+h : { RETURN(i) && $x := 1 } -> e;
+
+i : -> i;
diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.i b/src/plugins/aorai/tests/ya/metavariables-wrong.i
new file mode 100644
index 00000000000..9f52b790bec
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/metavariables-wrong.i
@@ -0,0 +1,22 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+void f(int x) {}
+void g(void) {}
+void h(void) {}
+
+void main(void)
+{
+ int x = 0;
+ while (x < 100)
+ {
+ if (x % 2)
+ f(x);
+ else
+ g();
+ h();
+ x++;
+ }
+}
+
diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.ya b/src/plugins/aorai/tests/ya/metavariables-wrong.ya
new file mode 100644
index 00000000000..6ab66a2fa64
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/metavariables-wrong.ya
@@ -0,0 +1,23 @@
+%init: a;
+%accept: g;
+%deterministic;
+
+$x : int;
+
+a : { CALL(main) } -> b;
+
+b :
+ { CALL(f) && $x := f().x } -> c
+| { CALL(g) } -> d
+| { RETURN(main) } -> g
+;
+
+c : { RETURN(f) } -> e;
+
+d : { RETURN(g) } -> e;
+
+e : { CALL(h) && $x > 0 } -> f;
+
+f : { RETURN(h) } -> b;
+
+g : -> g;
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
new file mode 100644
index 00000000000..d816c5975a4
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/aorai/metavariables-right.i (no preprocessing)
+[kernel] tests/aorai/metavariables-right.i:10:
+ syntax error:
+ Location: between lines 10 and 12, before or at token: void
+ 8 void i() {}
+ 9
+
+ 10 volatile int v,
+ 11
+ 12 void main(void)
+
+ 13 {
+ 14 if (v) {
+[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
new file mode 100644
index 00000000000..42947ae08f4
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-wrong.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/aorai/metavariables-wrong.i (no preprocessing)
+[aorai] Welcome to the Aorai plugin
+[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0.
+[kernel] Plug-in aorai aborted: invalid user input.
--
GitLab