From 35c677459f36587fa0ed6abddd2f5c7cde0ff36d Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 11 Sep 2023 15:56:18 +0200
Subject: [PATCH] Rewrite warning messages
---
src/kernel_internals/typing/populate_spec.ml | 42 ++++++++++------
.../oracle/default_spec_combine.0.res.oracle | 48 +++++++++----------
.../oracle/default_spec_combine.1.res.oracle | 48 +++++++++----------
.../oracle/default_spec_combine.2.res.oracle | 48 +++++++++----------
.../oracle/default_spec_custom.0.res.oracle | 4 +-
.../oracle/default_spec_custom.1.res.oracle | 4 +-
.../oracle/default_spec_mode.0.res.oracle | 22 ++++-----
.../oracle/default_spec_mode.1.res.oracle | 10 ++--
.../oracle/default_spec_mode.2.res.oracle | 30 ++++++------
.../oracle/default_spec_mode.3.res.oracle | 26 +++++-----
10 files changed, 147 insertions(+), 135 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index b57588753f9..2a86d2124c9 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 8bb154287f0..720ca104b63 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 faa0575f55f..0841097ed27 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 892d7404ea4..8b3889333f7 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 7942991288f..286ed55307b 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 1e9483d7627..b88fb59fe31 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 d60c199fd8a..26d552ea577 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 a70fdeec08b..a330ade6cc9 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 186bd10c71b..00c309f1271 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 064bbc6c3ce..45eacc7b262 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;
--
GitLab