diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index b57588753f96a5d8ee7b37c8421feb5212c85ece..2a86d2124c9a8f8e95189114717f1a66785ad97d 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -794,6 +794,10 @@ let activated_config kf clauses =
in
List.fold_left collect (build_config Skip) clauses
+let clauses_fmt =
+ Pretty_utils.pp_list ~pre:"" ~sep:", " ~last:" and " ~suf:""
+ Format.pp_print_string
+
(* Emit warnings if :
- we generated some clauses (cf. {!Make.get_default}).
- [kf] is a declaration and not part of frama-c (cf. {!Make.get_default}).
@@ -803,21 +807,29 @@ let activated_config kf clauses =
let do_warning kf funspec = function
| None -> ()
| Some (combined, clauses) ->
- let clauses = String.concat ", " clauses in
- if Cil.is_empty_funspec funspec then
- Kernel.warning ~once:true ~current:true ~wkey:Kernel.wkey_missing_spec
- "Neither code nor specification for function %a,@, \
- generating default specifications (%s) from the prototype"
- Kernel_function.pretty kf clauses
- else
- let combined =
- if combined then " (some combined from existing behaviors)" else ""
- in
- Kernel.warning ~once:true ~current:true ~wkey:Kernel.wkey_missing_spec
- "Missing clauses (%s) in specification of prototype %a,@, \
- generating default specification%s, see -generated-spec-* options \
- for more info"
- clauses Kernel_function.pretty kf combined
+ let n = List.length clauses in
+ let clauses = Format.asprintf "%a" clauses_fmt (List.rev clauses) in
+ let msg =
+ if Cil.is_empty_funspec funspec then
+ Format.asprintf
+ "Neither code nor specification for function %a,@, \
+ generating default %s"
+ Kernel_function.pretty kf clauses
+ else
+ let source =
+ if combined then
+ if n = 1 then " from the specification"
+ else " (some from the specification)"
+ else ""
+ in
+ Format.asprintf
+ "Neither code nor explicit %s for function %a,@, generating default \
+ clauses%s"
+ clauses Kernel_function.pretty kf source
+ in
+ Kernel.warning
+ ~once:true ~current:true ~wkey:Kernel.wkey_missing_spec
+ "%s. See -generated-spec-* options for more info" msg
(* Perform generation of all clauses, adds them to the original specification,
and emit property status for each of them. *)
diff --git a/tests/spec/oracle/default_spec_combine.0.res.oracle b/tests/spec/oracle/default_spec_combine.0.res.oracle
index 8bb154287f019a700b7eb836afe39ab5d92e297f..720ca104b63c74ffef25d0c52b4a492790d5c412 100644
--- a/tests/spec/oracle/default_spec_combine.0.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.0.res.oracle
@@ -1,41 +1,41 @@
Registering an mode that does nothing
[kernel] Parsing default_spec_combine.i (no preprocessing)
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (exits) in specification of prototype f1_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits for function f1_complete,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (exits) in specification of prototype f1_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits for function f1_guarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (exits) in specification of prototype f1_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits for function f1_unguarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (assigns) in specification of prototype f2_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit assigns for function f2_complete,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (assigns) in specification of prototype f2_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit assigns for function f2_guarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (assigns) in specification of prototype f2_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit assigns for function f2_unguarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires) in specification of prototype f3_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires for function f3_complete,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires) in specification of prototype f3_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires for function f3_guarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires) in specification of prototype f3_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires for function f3_unguarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates) in specification of prototype f4_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit allocates for function f4_complete,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates) in specification of prototype f4_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit allocates for function f4_guarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates) in specification of prototype f4_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit allocates for function f4_unguarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
/* 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 faa0575f55f2cd07495f78341814f218751455dc..0841097ed270800ecff3e6d4c1897adf0e059a15 100644
--- a/tests/spec/oracle/default_spec_combine.1.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.1.res.oracle
@@ -1,41 +1,41 @@
Registering an mode that does nothing
[kernel] Parsing default_spec_combine.i (no preprocessing)
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires, exits) in specification of prototype f1_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits and requires for function f1_complete,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires, exits) in specification of prototype f1_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits and requires for function f1_guarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires, exits) in specification of prototype f1_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits and requires for function f1_unguarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires, assigns) in specification of prototype f2_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit assigns and requires for function f2_complete,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires, assigns) in specification of prototype f2_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit assigns and requires for function f2_guarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires, assigns) in specification of prototype f2_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit assigns and requires for function f2_unguarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires) in specification of prototype f3_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires for function f3_complete,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires) in specification of prototype f3_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires for function f3_guarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (requires) in specification of prototype f3_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires for function f3_unguarded,
+ generating default clauses from the specification. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, requires) in specification of prototype f4_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires and allocates for function f4_complete,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, requires) in specification of prototype f4_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires and allocates for function f4_guarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, requires) in specification of prototype f4_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit requires and allocates for function f4_unguarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for 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 892d7404ea4065e8dc3147db1f74b6b5772f93db..8b3889333f7004b422daeebb545e1a8f7aefc2a7 100644
--- a/tests/spec/oracle/default_spec_combine.2.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.2.res.oracle
@@ -1,41 +1,41 @@
Registering an mode that does nothing
[kernel] Parsing default_spec_combine.i (no preprocessing)
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f1_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f1_complete,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f1_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f1_guarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f1_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f1_unguarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f2_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f2_complete,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f2_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f2_guarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f2_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f2_unguarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, requires, assigns, exits) in specification of prototype f3_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns, requires and allocates for function f3_complete,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, requires, assigns, exits) in specification of prototype f3_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns, requires and allocates for function f3_guarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, requires, assigns, exits) in specification of prototype f3_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns, requires and allocates for function f3_unguarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f4_complete,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f4_complete,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f4_guarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f4_guarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
- Missing clauses (allocates, assigns, exits) in specification of prototype f4_unguarded,
- generating default specification (some combined from existing behaviors), see -generated-spec-* options for more info
+ Neither code nor explicit exits, assigns and allocates for function f4_unguarded,
+ generating default clauses (some from the specification). See -generated-spec-* options for 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 7942991288ffc539d79bfe090bb6edac453623b3..286ed55307b6f1575fa74f51b4b6cbbd891b150d 100644
--- a/tests/spec/oracle/default_spec_custom.0.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.0.res.oracle
@@ -8,14 +8,14 @@ Registering a new spec generation mode
[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 specifications (terminates, allocates, assigns, exits) from the prototype
+ generating default exits, assigns, allocates and terminates. See -generated-spec-* options for more info
[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 specifications (terminates, allocates, assigns, exits) from the prototype
+ generating default exits, assigns, allocates and terminates. See -generated-spec-* options for more info
/* 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 1e9483d762792b7824fdbe296b37ac3c9a3abb3b..b88fb59fe31c1f4c1ea8a8e5f298cff5d9533ab9 100644
--- a/tests/spec/oracle/default_spec_custom.1.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.1.res.oracle
@@ -3,10 +3,10 @@ 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 specifications (terminates, allocates, requires, assigns, exits) from the prototype
+ generating default exits, assigns, requires, allocates and terminates. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
Neither code nor specification for function f3,
- generating default specifications (terminates, allocates, requires, assigns, exits) from the prototype
+ generating default exits, assigns, requires, allocates and terminates. See -generated-spec-* options for more info
/* Generated by Frama-C */
/*@ requires \false;
terminates \false;
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
index d60c199fd8a5e1d436cf7d52ba3a084dcd81b77c..26d552ea577ab80091bde8d2bdd06be1d4eb15ea 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -1,22 +1,22 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor specification for function f1,
- generating default specifications (exits) from the prototype
+ generating default exits. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (allocates) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit allocates for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (exits) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit exits for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (allocates) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit allocates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
/*@ terminates \true;
exits \false;
diff --git a/tests/spec/oracle/default_spec_mode.1.res.oracle b/tests/spec/oracle/default_spec_mode.1.res.oracle
index a70fdeec08b451c5494b9ca76f006d5fe19b6fc1..a330ade6cc97a3b5880801493ef4e0bb9d53d98b 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -1,13 +1,13 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor specification for function f1,
- generating default specifications (requires) from the prototype
+ generating default requires. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
/* 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 186bd10c71b5f2094a1b5b70c7efbad09529a567..00c309f12714144030ab6c61729cca8f29b8841c 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -1,28 +1,28 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor specification for function f1,
- generating default specifications (exits) from the prototype
+ generating default exits. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (assigns) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit assigns for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (allocates) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit allocates for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (exits) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit exits for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (assigns) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit assigns for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (allocates) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit allocates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
/*@ terminates \true;
exits \false;
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index 064bbc6c3cea1ec4666f0822571a30b2e34a8f6c..45eacc7b262eab6b733552eeab654601b76a2e57 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -1,25 +1,25 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
Neither code nor specification for function f1,
- generating default specifications (exits) from the prototype
+ generating default exits. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (assigns) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit assigns for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (requires) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit requires for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f1,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (exits) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit exits for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (assigns) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit assigns for function f3,
+ generating default clauses. See -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
- Missing clauses (terminates) in specification of prototype f3,
- generating default specification, see -generated-spec-* options for more info
+ Neither code nor explicit terminates for function f3,
+ generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
/*@ requires \false;
terminates \true;