From b9a2fcc36a6b31e4298d60c04c6e45d6368751d1 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 4 Aug 2023 11:08:58 +0200
Subject: [PATCH] Update test oracles

---
 .../oracle/default_spec_combine.0.res.oracle  | 12 +++++
 .../oracle/default_spec_combine.1.res.oracle  | 33 ++++++++++++
 .../oracle/default_spec_combine.2.res.oracle  | 51 +++++++++++++++++++
 .../oracle/default_spec_custom.0.res.oracle   |  6 ++-
 .../oracle/default_spec_custom.1.res.oracle   |  6 ++-
 .../oracle/default_spec_mode.2.res.oracle     |  6 +++
 .../oracle/default_spec_mode.3.res.oracle     |  3 ++
 .../oracle/default_spec_mode.4.res.oracle     | 12 +++++
 .../oracle/default_spec_mode.5.res.oracle     |  6 +++
 .../oracle/default_spec_mode.6.res.oracle     |  2 +-
 .../oracle/default_spec_mode.7.res.oracle     |  2 +-
 11 files changed, 133 insertions(+), 6 deletions(-)

diff --git a/tests/spec/oracle/default_spec_combine.0.res.oracle b/tests/spec/oracle/default_spec_combine.0.res.oracle
index 35690113209..2884fc32019 100644
--- a/tests/spec/oracle/default_spec_combine.0.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.0.res.oracle
@@ -1,5 +1,17 @@
 Registering an mode that does nothing
 [kernel] Parsing default_spec_combine.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing exits in default behavior of prototype f1,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing assigns in default behavior of prototype f2,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing requires in default behavior of prototype f3,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing allocates in default behavior of prototype f4,
+   generating default specification from complete behaviors
 /* Generated by Frama-C */
 /*@
 axiomatic a {
diff --git a/tests/spec/oracle/default_spec_combine.1.res.oracle b/tests/spec/oracle/default_spec_combine.1.res.oracle
index 0a1534d061e..66422324816 100644
--- a/tests/spec/oracle/default_spec_combine.1.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.1.res.oracle
@@ -1,5 +1,38 @@
 Registering an mode that does nothing
 [kernel] Parsing default_spec_combine.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing exits in default behavior of prototype f1,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing requires in specification of prototype f1,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f1,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing assigns in default behavior of prototype f2,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing requires in specification of prototype f2,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f2,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing requires in default behavior of prototype f3,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing requires in specification of prototype f4,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing allocates in default behavior of prototype f4,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f4,
+   generating default specification, see -generated-spec-* optionsfor more info
 /* Generated by Frama-C */
 /*@
 axiomatic a {
diff --git a/tests/spec/oracle/default_spec_combine.2.res.oracle b/tests/spec/oracle/default_spec_combine.2.res.oracle
index 9d91be61fde..b0fba331947 100644
--- a/tests/spec/oracle/default_spec_combine.2.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.2.res.oracle
@@ -1,5 +1,56 @@
 Registering an mode that does nothing
 [kernel] Parsing default_spec_combine.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing exits in default behavior of prototype f1,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing assigns in specification of prototype f1,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing allocates in specification of prototype f1,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f1,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing exits in specification of prototype f2,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing assigns in default behavior of prototype f2,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing allocates in specification of prototype f2,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f2,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing exits in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing assigns in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing requires in default behavior of prototype f3,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing allocates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing exits in specification of prototype f4,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing assigns in specification of prototype f4,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing allocates in default behavior of prototype f4,
+   generating default specification from complete behaviors
+[kernel:annot:missing-spec] default_spec_combine.i:53: Warning: 
+  Missing terminates in specification of prototype f4,
+   generating default specification, see -generated-spec-* optionsfor more info
 /* Generated by Frama-C */
 /*@
 axiomatic a {
diff --git a/tests/spec/oracle/default_spec_custom.0.res.oracle b/tests/spec/oracle/default_spec_custom.0.res.oracle
index fda41e6d630..0b799247cf9 100644
--- a/tests/spec/oracle/default_spec_custom.0.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.0.res.oracle
@@ -7,13 +7,15 @@ Registering a new spec generation mode
 [kernel] Warning: Custom generation from mode emptymode not defined for allocates, using frama-c mode instead
 [kernel] Warning: Custom generation from mode emptymode not defined for terminates, using frama-c mode instead
 [kernel:annot:missing-spec] default_spec_custom.i:18: Warning: 
-  Neither code nor specification for function f1, generating default specs from the prototype
+  Neither code nor specification for function f1,
+   generating default specifications from the prototype
 [kernel] Warning: Custom status from mode emptymode not defined for exits
 [kernel] Warning: Custom status from mode emptymode not defined for assigns
 [kernel] Warning: Custom status from mode emptymode not defined for allocates
 [kernel] Warning: Custom status from mode emptymode not defined for terminates
 [kernel:annot:missing-spec] default_spec_custom.i:18: Warning: 
-  Neither code nor specification for function f3, generating default specs from the prototype
+  Neither code nor specification for function f3,
+   generating default specifications from the prototype
 /* Generated by Frama-C */
 /*@ terminates \true;
     exits \false;
diff --git a/tests/spec/oracle/default_spec_custom.1.res.oracle b/tests/spec/oracle/default_spec_custom.1.res.oracle
index 3151473f64c..5a21e5f9477 100644
--- a/tests/spec/oracle/default_spec_custom.1.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.1.res.oracle
@@ -2,9 +2,11 @@ Registering an empty spec generation mode
 Registering a new spec generation mode
 [kernel] Parsing default_spec_custom.i (no preprocessing)
 [kernel:annot:missing-spec] default_spec_custom.i:18: Warning: 
-  Neither code nor specification for function f1, generating default specs from the prototype
+  Neither code nor specification for function f1,
+   generating default specifications from the prototype
 [kernel:annot:missing-spec] default_spec_custom.i:18: Warning: 
-  Neither code nor specification for function f3, generating default specs from the prototype
+  Neither code nor specification for function f3,
+   generating default specifications from the prototype
 /* Generated by Frama-C */
 /*@ requires \false;
     terminates \false;
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
index e3d1b2a70b4..d735d0d8800 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -1,4 +1,10 @@
 [kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing allocates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing terminates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
 /* Generated by Frama-C */
 void f1(void);
 
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index a9f745a0148..c1e4d4686a9 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -1,4 +1,7 @@
 [kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing terminates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
 /* Generated by Frama-C */
 void f1(void);
 
diff --git a/tests/spec/oracle/default_spec_mode.4.res.oracle b/tests/spec/oracle/default_spec_mode.4.res.oracle
index 90038462eb5..95cfe9b579c 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -1,4 +1,16 @@
 [kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing exits in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing assigns in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing allocates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing terminates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
 /* Generated by Frama-C */
 void f1(void);
 
diff --git a/tests/spec/oracle/default_spec_mode.5.res.oracle b/tests/spec/oracle/default_spec_mode.5.res.oracle
index 69c1b68dab3..708f08824cd 100644
--- a/tests/spec/oracle/default_spec_mode.5.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.5.res.oracle
@@ -1,4 +1,10 @@
 [kernel] Parsing default_spec_mode.i (no preprocessing)
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing assigns in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
+[kernel:annot:missing-spec] default_spec_mode.i:31: Warning: 
+  Missing terminates in specification of prototype f3,
+   generating default specification, see -generated-spec-* optionsfor more info
 /* Generated by Frama-C */
 void f1(void);
 
diff --git a/tests/spec/oracle/default_spec_mode.6.res.oracle b/tests/spec/oracle/default_spec_mode.6.res.oracle
index 0431517a924..d131bef3d3d 100644
--- a/tests/spec/oracle/default_spec_mode.6.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.6.res.oracle
@@ -1,4 +1,4 @@
 [kernel] Parsing default_spec_mode.i (no preprocessing)
 [kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
-  Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
+   Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
 [kernel] Frama-C aborted: invalid user input.
diff --git a/tests/spec/oracle/default_spec_mode.7.res.oracle b/tests/spec/oracle/default_spec_mode.7.res.oracle
index 0431517a924..d131bef3d3d 100644
--- a/tests/spec/oracle/default_spec_mode.7.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.7.res.oracle
@@ -1,4 +1,4 @@
 [kernel] Parsing default_spec_mode.i (no preprocessing)
 [kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
-  Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
+   Accepted keys are 'exits', 'assigns', 'requires', 'allocates' and 'terminates'.
 [kernel] Frama-C aborted: invalid user input.
-- 
GitLab