diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle index e3d5ec00773c630fcd03a506eaec86aa0b0777ee..db979fdb7c87c7b1d15c858c8fe51e570b729a72 100644 --- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle +++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle @@ -3,5 +3,5 @@ Calling undeclared function call_to_an_undefined_function. Old style K&R code? [kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing) [wp] Warning: Missing RTE guards -[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:86: Warning: +[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:87: Warning: Neither code nor specification for function call_to_an_undefined_function, generating default assigns from the prototype diff --git a/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle index 4f152c30c54f4965a93599b99d6a8f6cb9ad0c56..6168c618fe79e2e0da7ebe5b8b2167825f84ce8d 100644 --- a/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle +++ b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle @@ -1,4 +1,3 @@ [kernel] Parsing tests/ya/logical_operators.i (no preprocessing) -[aorai] Welcome to the Aorai plugin [kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing) [wp] Warning: Missing RTE guards