From 17548910184a91f24a5dd9e365af3dc2d50ccacf Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Fri, 12 Feb 2021 20:04:52 +0100 Subject: [PATCH] [aorai] update oracles for prove config --- src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle | 2 +- .../aorai/tests/ya/oracle_prove/logical_operators.res.oracle | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) 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 e3d5ec00773..db979fdb7c8 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 4f152c30c54..6168c618fe7 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 -- GitLab