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 0000000000000000000000000000000000000000..d74d63528a3e1607b01d0b3725e4bdc26a39c0b6 --- /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 0000000000000000000000000000000000000000..acfb544b612fe9e6eb7b6804a3b97d11f8db061e --- /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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391