From e696b5396782841809f6d64b7bd540e252bb2c44 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 6 Sep 2022 14:09:16 +0200
Subject: [PATCH] [aorai] add test for function pointers
---
src/plugins/aorai/tests/ya/function_ptr.i | 20 +++++++++++++++++++
src/plugins/aorai/tests/ya/function_ptr.ya | 14 +++++++++++++
.../tests/ya/oracle/function_ptr.err.oracle | 0
.../tests/ya/oracle/function_ptr.res.oracle | 0
4 files changed, 34 insertions(+)
create mode 100644 src/plugins/aorai/tests/ya/function_ptr.i
create mode 100644 src/plugins/aorai/tests/ya/function_ptr.ya
create mode 100644 src/plugins/aorai/tests/ya/oracle/function_ptr.err.oracle
create mode 100644 src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
diff --git a/src/plugins/aorai/tests/ya/function_ptr.i b/src/plugins/aorai/tests/ya/function_ptr.i
new file mode 100644
index 00000000000..d74d63528a3
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/function_ptr.i
@@ -0,0 +1,20 @@
+/* run.config*
+ STDOPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya}
+*/
+
+void (*pf)(void);
+
+int X;
+
+void f(void) { X++; }
+
+void g(void) { X--; }
+
+int main(int c) {
+ if(c) pf = f; else pf = g;
+ /*@ calls f,g; */
+ pf();
+ if (c) pf = g; else pf = f;
+ /*@ calls f,g; */
+ pf();
+}
diff --git a/src/plugins/aorai/tests/ya/function_ptr.ya b/src/plugins/aorai/tests/ya/function_ptr.ya
new file mode 100644
index 00000000000..acfb544b612
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/function_ptr.ya
@@ -0,0 +1,14 @@
+%init: i;
+%accept: ok;
+%deterministic;
+
+i: { CALL(main) } -> s1;
+
+s1: { f() } -> f_called
+ | { g() } -> g_called;
+
+f_called: { g() } -> ok;
+
+g_called: { f() } -> ok;
+
+ok: { RETURN(main) } -> ok;
diff --git a/src/plugins/aorai/tests/ya/oracle/function_ptr.err.oracle b/src/plugins/aorai/tests/ya/oracle/function_ptr.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle b/src/plugins/aorai/tests/ya/oracle/function_ptr.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab