From b6c7f6d9df2e4f48ebc52d537a61596fef57cfc3 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Tue, 8 Aug 2023 11:28:38 +0200
Subject: [PATCH] Fix typo in warning
---
src/kernel_internals/typing/populate_spec.ml | 2 +-
.../oracle/default_spec_combine.1.res.oracle | 14 +++++-----
.../oracle/default_spec_combine.2.res.oracle | 26 +++++++++----------
.../oracle/default_spec_mode.2.res.oracle | 6 ++---
.../oracle/default_spec_mode.3.res.oracle | 2 +-
.../oracle/default_spec_mode.4.res.oracle | 8 +++---
.../oracle/default_spec_mode.5.res.oracle | 6 ++---
7 files changed, 32 insertions(+), 32 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index 8b762b1b8b4..e9773fec250 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -155,7 +155,7 @@ struct
else if not warned && not empty then
Kernel.warning ~once:true ~current:true ~wkey:Kernel.wkey_missing_spec
"Missing %s in specification of prototype %a,@, \
- generating default specification, see -generated-spec-* options\
+ generating default specification, see -generated-spec-* options \
for more info"
name Kernel_function.pretty kf
diff --git a/tests/spec/oracle/default_spec_combine.1.res.oracle b/tests/spec/oracle/default_spec_combine.1.res.oracle
index 66422324816..2d5b9acc3fb 100644
--- a/tests/spec/oracle/default_spec_combine.1.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.1.res.oracle
@@ -5,34 +5,34 @@ Registering an mode that does nothing
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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default 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 b0fba331947..d3b8b07f176 100644
--- a/tests/spec/oracle/default_spec_combine.2.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.2.res.oracle
@@ -5,52 +5,52 @@ Registering an mode that does nothing
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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for more info
/* Generated by Frama-C */
/*@
axiomatic a {
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
index 5fd4480bc34..281c87b8e9f 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -1,13 +1,13 @@
[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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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 c1e4d4686a9..4793b616e3f 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -1,7 +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
+ generating default specification, see -generated-spec-* options for 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 95cfe9b579c..86d3a6b91f8 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -1,16 +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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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 df3257a8871..319e013e53f 100644
--- a/tests/spec/oracle/default_spec_mode.5.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.5.res.oracle
@@ -1,13 +1,13 @@
[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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for 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
+ generating default specification, see -generated-spec-* options for more info
/* Generated by Frama-C */
void f1(void);
--
GitLab