diff --git a/tests/spec/oracle/default_spec_combine.0.res.oracle b/tests/spec/oracle/default_spec_combine.0.res.oracle
index 35690113209a826ba67421166dec172dd2a0db6e..2884fc3201922d5e68feac39dd115e64e7459974 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 0a1534d061eceaae505972a6bdcc69d5549cc24b..6642232481614e00ebe9ac2e1799d3546385d371 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 9d91be61fdee9287cd76f78355634b4b2cf49e60..b0fba331947e80c310d01431737b1394842bf6b4 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 fda41e6d63057da79517b773ecfedf608db05d4b..0b799247cf98e154a9689a6ef8fd268838ddd14f 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 3151473f64cd26f33ade3c2431e795f2627acd78..5a21e5f94773c0f3cce2b4a87537e456ec621d47 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 e3d1b2a70b4ab679c2049d735103be40dc5b7c66..d735d0d8800937c6f3c3c1a6a711b0b9d217b113 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 a9f745a014834522381957113332b8a16232fdb6..c1e4d4686a93cbb76abfbe8478c774c40715e370 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 90038462eb51543ab393e7acacb7d4349423df21..95cfe9b579c66443b66d5d688add17ab26c1ff26 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 69c1b68dab380444d5914c928ff3a3f6a6f7417c..708f08824cd749109c72e7d7b272b4927b3770b0 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 0431517a924001a2e1d95c2b33bc69f87a76b1a8..d131bef3d3d34d4a170f09b286deada4b266c4f6 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 0431517a924001a2e1d95c2b33bc69f87a76b1a8..d131bef3d3d34d4a170f09b286deada4b266c4f6 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.