diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml index 8b762b1b8b4bd5251fadd139b4b67e768523a3dd..e9773fec250244714e8c02dfeaca029a662e3cef 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 6642232481614e00ebe9ac2e1799d3546385d371..2d5b9acc3fbb8171dd013c06da9e4b2251ba2627 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 b0fba331947e80c310d01431737b1394842bf6b4..d3b8b07f176f95c16f9d25b6e35b8d749f43c3c6 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 5fd4480bc341b773b4dfa2f5188a1f4c7386387d..281c87b8e9f19209107e14fbbebbee96f1a6a3af 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 c1e4d4686a93cbb76abfbe8478c774c40715e370..4793b616e3f74d3bb94df64927efb5c3bac299c1 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 95cfe9b579c66443b66d5d688add17ab26c1ff26..86d3a6b91f8ea103b72ddada30792e648361057b 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 df3257a887108e95c937dbb703de33985b63c046..319e013e53fab12b1416810d7531dcc92c5b294a 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);