diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle index 500161bb9b87f344c719102b69b2fca48fd92521..7ae3924febd86be97966145c4a9f4f9036d271b5 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/ya/declared_function.i (no preprocessing) [kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing) -[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:50: Warning: - Neither code nor specification for function f, generating default assigns from the prototype [wp] Warning: Missing RTE guards +[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:105: Warning: + Neither code nor specification for function f, generating default assigns from the prototype diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle index 30ba0541d811ba71dc98cdebc6793c7e0d12e87e..4528171182267c406d39f66383a6a0b3ab9f48c9 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle @@ -2,5 +2,5 @@ [aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead [kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing) [wp] Warning: Missing RTE guards -[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:69: Warning: +[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:70: Warning: Neither code nor specification for function f, generating default assigns from the prototype diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle index 2dd3de37879294166ef9a7e0f933bf3cc88c7339..504add72c15b60e3a444880a1f2512361f7b52ce 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/ya/serial.c (with preprocessing) [kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing) -[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:738: Warning: - Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype [wp] Warning: Missing RTE guards +[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:1450: Warning: + Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle index 0bf1b088bf5ade07b4cd849c3aec445cb17b41ef..6af6c903d75f55c62879d1118a94fba3347d91fa 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle @@ -1,5 +1,3 @@ [kernel] Parsing tests/ya/test_acces_params.c (with preprocessing) [kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing) -[wp] TMPDIR/aorai_test_acces_params_0.i:4: Warning: - Global invariant not handled yet ('inv' ignored) [wp] Warning: Missing RTE guards diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle index 82a83a9128b6065cf9c1cddf718442da4c93d7d1..9e85d00f9bab0ceefcf38b4712d0f3ecb4bc72a2 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle @@ -1,5 +1,3 @@ [kernel] Parsing tests/ya/test_acces_params2.c (with preprocessing) [kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing) -[wp] TMPDIR/aorai_test_acces_params2_0.i:3: Warning: - Global invariant not handled yet ('inv' ignored) [wp] Warning: Missing RTE guards