From d1f9faf7c5fd0748ff7ee134f2ee6651ee420fd0 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 8 Sep 2023 15:39:13 +0200
Subject: [PATCH] Fix & update default_spec & vis_spec tests
---
tests/misc/oracle/vis_spec.res.oracle | 22 ++-----
tests/misc/vis_spec.ml | 2 -
tests/spec/default_spec_combine.i | 4 +-
tests/spec/default_spec_combine.ml | 5 +-
tests/spec/default_spec_custom.ml | 4 +-
tests/spec/default_spec_mode.i | 9 ++-
tests/spec/default_spec_mode.ml | 19 ++++++
.../oracle/default_spec_combine.0.res.oracle | 20 ++++---
.../oracle/default_spec_combine.1.res.oracle | 41 ++++---------
.../oracle/default_spec_combine.2.res.oracle | 59 ++++---------------
.../oracle/default_spec_custom.0.res.oracle | 4 +-
.../oracle/default_spec_custom.1.res.oracle | 4 +-
.../oracle/default_spec_mode.0.res.oracle | 40 ++++++++++++-
.../oracle/default_spec_mode.1.res.oracle | 26 +++++++-
.../oracle/default_spec_mode.2.res.oracle | 50 ++++++++++++----
.../oracle/default_spec_mode.3.res.oracle | 42 +++++++++++--
.../oracle/default_spec_mode.4.res.oracle | 51 +---------------
.../oracle/default_spec_mode.5.res.oracle | 47 +--------------
.../oracle/default_spec_mode.6.res.oracle | 4 --
.../oracle/default_spec_mode.7.res.oracle | 4 --
20 files changed, 221 insertions(+), 236 deletions(-)
create mode 100644 tests/spec/default_spec_mode.ml
delete mode 100644 tests/spec/oracle/default_spec_mode.6.res.oracle
delete mode 100644 tests/spec/oracle/default_spec_mode.7.res.oracle
diff --git a/tests/misc/oracle/vis_spec.res.oracle b/tests/misc/oracle/vis_spec.res.oracle
index 8151d594e44..70cd75db512 100644
--- a/tests/misc/oracle/vis_spec.res.oracle
+++ b/tests/misc/oracle/vis_spec.res.oracle
@@ -1,25 +1,11 @@
[kernel] Parsing vis_spec.i (no preprocessing)
Starting visit
Considering vspec of function g
-Function prototype; Funspec is
-'terminates \true;
- exits \false;
- allocates \nothing;'
+Function prototype; Funspec is 'assigns \nothing;'
Considering sspec of function f
Funspec of f is '' through visitor
-It is 'terminates \true;
- exits \false;
- assigns \nothing;
- allocates \nothing;'
-through get_spec
+It is 'assigns \nothing;' through get_spec
Considering vspec of function f
-Funspec of f is 'terminates \true;
- exits \false;
- allocates \nothing;'
-through visitor
-It is 'terminates \true;
- exits \false;
- assigns \nothing;
- allocates \nothing;'
-through get_spec
+Funspec of f is 'assigns \nothing;' through visitor
+It is 'assigns \nothing;' through get_spec
End visit
diff --git a/tests/misc/vis_spec.ml b/tests/misc/vis_spec.ml
index fa9afd7df9d..aac82704de2 100644
--- a/tests/misc/vis_spec.ml
+++ b/tests/misc/vis_spec.ml
@@ -11,7 +11,6 @@ class pathcrawlerVisitor prj =
fundec.svar.vname
Printer.pp_funspec fundec.sspec;
let kf = Globals.Functions.get fundec.svar in
- Populate_spec.(populate_funspec kf [`Assigns]);
Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
Printer.pp_funspec
(Annotations.funspec kf);
@@ -26,7 +25,6 @@ class pathcrawlerVisitor prj =
fundec.svar.vname
Printer.pp_funspec sp;
let kf = Globals.Functions.get fundec.svar in
- Populate_spec.(populate_funspec kf [`Assigns]);
Format.printf "@[It is@ @['%a'@]@ through get_spec@]@."
Printer.pp_funspec
(Annotations.funspec kf);
diff --git a/tests/spec/default_spec_combine.i b/tests/spec/default_spec_combine.i
index 29c80655c6c..7910730ee26 100644
--- a/tests/spec/default_spec_combine.i
+++ b/tests/spec/default_spec_combine.i
@@ -2,8 +2,8 @@
MODULE: @PTEST_NAME@
STDOPT: +"-generated-spec-mode donothing"
- STDOPT: +"-generated-spec-mode safe -generated-spec-custom allocates:safe"
- STDOPT: +"-generated-spec-mode frama-c -generated-spec-custom allocates:frama-c"
+ STDOPT: +"-generated-spec-mode safe"
+ STDOPT: +"-generated-spec-mode frama-c"
*/
/*@ axiomatic a {
diff --git a/tests/spec/default_spec_combine.ml b/tests/spec/default_spec_combine.ml
index 6261077f996..f4a862e81c6 100644
--- a/tests/spec/default_spec_combine.ml
+++ b/tests/spec/default_spec_combine.ml
@@ -15,8 +15,9 @@ let gen_terminates _ _ = None
let status_terminates = Property_status.Dont_know
let run () =
+ let open Populate_spec in
let get_spec kf =
- ignore(Annotations.funspec kf)
+ populate_funspec kf [`Exits; `Assigns; `Requires; `Allocates; `Terminates]
in
Globals.Functions.iter get_spec
@@ -32,3 +33,5 @@ let populate () =
let () = Cmdline.run_after_configuring_stage populate
+
+let () = Db.Main.extend run
diff --git a/tests/spec/default_spec_custom.ml b/tests/spec/default_spec_custom.ml
index 826cd252d44..bf4d185694f 100644
--- a/tests/spec/default_spec_custom.ml
+++ b/tests/spec/default_spec_custom.ml
@@ -27,8 +27,10 @@ let status_allocates = Property_status.Dont_know
let status_terminates = Property_status.Dont_know
let run () =
+ let open Populate_spec in
let get_spec kf =
- ignore(Annotations.funspec kf)
+ populate_funspec ~do_body:true kf
+ [`Exits; `Assigns; `Requires; `Allocates; `Terminates]
in
Globals.Functions.iter get_spec
diff --git a/tests/spec/default_spec_mode.i b/tests/spec/default_spec_mode.i
index de2d911f8ef..e9023087582 100644
--- a/tests/spec/default_spec_mode.i
+++ b/tests/spec/default_spec_mode.i
@@ -1,9 +1,8 @@
/* run.config
- STDOPT: +"-no-generate-default-spec"
- STDOPT: +"-generated-spec-mode skip"
- STDOPT: +"-generated-spec-mode acsl -generated-spec-custom allocates:acsl"
- STDOPT: +"-generated-spec-mode safe -generated-spec-custom allocates:safe"
- STDOPT: +"-generated-spec-mode frama-c -generated-spec-custom allocates:frama-c"
+ MODULE: @PTEST_NAME@
+ STDOPT: +"-generated-spec-mode acsl"
+ STDOPT: +"-generated-spec-mode safe"
+ STDOPT: +"-generated-spec-mode frama-c"
STDOPT: +"-generated-spec-custom exits:acsl,assigns:frama-c,requires:safe,allocates:safe,terminates:acsl"
EXIT: 1
diff --git a/tests/spec/default_spec_mode.ml b/tests/spec/default_spec_mode.ml
new file mode 100644
index 00000000000..14210495d5f
--- /dev/null
+++ b/tests/spec/default_spec_mode.ml
@@ -0,0 +1,19 @@
+let run () =
+ let open Populate_spec in
+ let get_spec kf =
+ let funspec = Annotations.funspec kf in
+ populate_funspec ~do_body:true ~funspec kf [`Exits];
+ populate_funspec ~do_body:true kf [`Assigns];
+ populate_funspec ~do_body:true kf [`Requires];
+ populate_funspec ~do_body:true kf [`Allocates];
+ populate_funspec ~do_body:true kf [`Terminates];
+
+ (* Should no nothing *)
+ ignore(!Annotations.populate_spec_ref kf funspec);
+ populate_funspec ~do_body:true kf
+ [`Exits; `Assigns; `Requires; `Allocates; `Terminates]
+ in
+ Globals.Functions.iter get_spec
+ [@@ warning "-3"]
+
+let () = Db.Main.extend run
diff --git a/tests/spec/oracle/default_spec_combine.0.res.oracle b/tests/spec/oracle/default_spec_combine.0.res.oracle
index 2884fc32019..bc19f23f4dd 100644
--- a/tests/spec/oracle/default_spec_combine.0.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.0.res.oracle
@@ -1,17 +1,21 @@
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
+ Missing clauses (exits) in specification of prototype f1,
+ generating default specification (some combined from existing behaviors),
+ 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
+ Missing clauses (assigns) in specification of prototype f2,
+ generating default specification (some combined from existing behaviors),
+ 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
+ Missing clauses (requires) in specification of prototype f3,
+ generating default specification (some combined from existing behaviors),
+ 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
+ Missing clauses (allocates) in specification of prototype f4,
+ generating default specification (some combined from existing behaviors),
+ 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 2d5b9acc3fb..a37b50f294c 100644
--- a/tests/spec/oracle/default_spec_combine.1.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.1.res.oracle
@@ -1,38 +1,21 @@
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
+ Missing clauses (terminates, requires, exits) in specification of prototype f1,
+ generating default specification (some combined from existing behaviors),
+ see -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:53: Warning:
- Missing requires in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Missing clauses (terminates, requires, assigns) in specification of prototype f2,
+ generating default specification (some combined from existing behaviors),
+ 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-* options for more info
+ Missing clauses (terminates, requires) in specification of prototype f3,
+ generating default specification (some combined from existing behaviors),
+ 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-* 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-* 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-* 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-* 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-* options for more info
+ Missing clauses (terminates, allocates, requires) in specification of prototype f4,
+ generating default specification (some combined from existing behaviors),
+ 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 d3b8b07f176..60a9ca8fbf7 100644
--- a/tests/spec/oracle/default_spec_combine.2.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.2.res.oracle
@@ -1,56 +1,21 @@
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
+ Missing clauses (terminates, allocates, assigns, exits) in specification of prototype f1,
+ generating default specification (some combined from existing behaviors),
+ see -generated-spec-* options for more info
[kernel:annot:missing-spec] default_spec_combine.i:53: Warning:
- Missing assigns in specification of prototype f1,
- generating default specification, see -generated-spec-* options for more info
+ Missing clauses (terminates, allocates, assigns, exits) in specification of prototype f2,
+ generating default specification (some combined from existing behaviors),
+ 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-* options for more info
+ Missing clauses (terminates, allocates, requires, assigns, exits) in specification of prototype f3,
+ generating default specification (some combined from existing behaviors),
+ 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-* 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-* 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-* 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-* 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-* 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-* 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-* 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-* 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-* 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-* 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-* options for more info
+ Missing clauses (terminates, allocates, assigns, exits) in specification of prototype f4,
+ generating default specification (some combined from existing behaviors),
+ 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 0b799247cf9..ba3feb06de6 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 from the prototype
+ generating default specifications (terminates, allocates, assigns, exits) 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 specifications from the prototype
+ generating default specifications (terminates, allocates, assigns, exits) 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 5a21e5f9477..d95af99e11c 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 from the prototype
+ generating default specifications (terminates, requires, assigns, exits) from the prototype
[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
Neither code nor specification for function f3,
- generating default specifications from the prototype
+ generating default specifications (terminates, requires, assigns, exits) from the prototype
/* 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 e36e7137656..bdc222f9545 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -1,18 +1,54 @@
[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
+[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
+[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
+[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
+[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
+[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
/* Generated by Frama-C */
+/*@ terminates \true;
+ exits \false;
+ allocates \nothing; */
void f1(void);
+/*@ terminates \true;
+ exits \false;
+ allocates \nothing; */
void f2(void)
{
f1();
return;
}
-/*@ requires \true; */
+/*@ requires \true;
+ terminates \true;
+ exits \false;
+ allocates \nothing; */
int f3(int *a);
/*@ requires \true;
- assigns *b; */
+ terminates \true;
+ exits \false;
+ assigns *b;
+ allocates \nothing;
+ */
int f4(int *b)
{
int tmp;
diff --git a/tests/spec/oracle/default_spec_mode.1.res.oracle b/tests/spec/oracle/default_spec_mode.1.res.oracle
index e36e7137656..cc2910b141b 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -1,18 +1,40 @@
[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
+[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
+[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
/* Generated by Frama-C */
+/*@ requires \false;
+ terminates \false; */
void f1(void);
+/*@ terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing; */
void f2(void)
{
f1();
return;
}
-/*@ requires \true; */
+/*@ requires \true;
+ terminates \false; */
int f3(int *a);
/*@ requires \true;
- assigns *b; */
+ terminates \true;
+ exits \false;
+ assigns *b;
+ allocates \nothing;
+ */
int f4(int *b)
{
int tmp;
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
index 281c87b8e9f..ca5c29a70c2 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -1,14 +1,40 @@
[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-* 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-* 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-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor specification for function f1,
+ generating default specifications (exits) from the prototype
+[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
+[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
+[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
+[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
+[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
+[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
+[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
/* Generated by Frama-C */
+/*@ terminates \true;
+ exits \false;
+ assigns \nothing;
+ allocates \nothing; */
void f1(void);
/*@ terminates \true;
@@ -23,7 +49,11 @@ void f2(void)
/*@ requires \true;
terminates \true;
exits \false;
- allocates \nothing; */
+ assigns \result, *a;
+ assigns \result \from *a;
+ assigns *a \from *a;
+ allocates \nothing;
+ */
int f3(int *a);
/*@ requires \true;
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index 4793b616e3f..9f1437903e8 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -1,13 +1,40 @@
[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-* options for more info
+[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+ Neither code nor specification for function f1,
+ generating default specifications (exits) from the prototype
+[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
+[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
+[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
+[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
+[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
+[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
/* Generated by Frama-C */
+/*@ requires \false;
+ terminates \true;
+ exits \false;
+ assigns \nothing; */
void f1(void);
/*@ terminates \true;
exits \false;
- assigns \nothing;
allocates \nothing; */
void f2(void)
{
@@ -16,7 +43,12 @@ void f2(void)
}
/*@ requires \true;
- terminates \false; */
+ terminates \true;
+ exits \false;
+ assigns \result, *a;
+ assigns \result \from *a;
+ assigns *a \from *a;
+ */
int f3(int *a);
/*@ requires \true;
diff --git a/tests/spec/oracle/default_spec_mode.4.res.oracle b/tests/spec/oracle/default_spec_mode.4.res.oracle
index 86d3a6b91f8..d131bef3d3d 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -1,49 +1,4 @@
[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-* 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-* 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-* 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-* options for more info
-/* Generated by Frama-C */
-void f1(void);
-
-/*@ terminates \true;
- exits \false;
- allocates \nothing; */
-void f2(void)
-{
- f1();
- return;
-}
-
-/*@ requires \true;
- terminates \true;
- exits \false;
- assigns \result, *a;
- assigns \result \from *a;
- assigns *a \from *a;
- allocates \nothing;
- */
-int f3(int *a);
-
-/*@ requires \true;
- terminates \true;
- exits \false;
- assigns *b;
- allocates \nothing;
- */
-int f4(int *b)
-{
- int tmp;
- tmp = f3(b);
- return tmp;
-}
-
-
+[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
+ 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.5.res.oracle b/tests/spec/oracle/default_spec_mode.5.res.oracle
index 319e013e53f..d131bef3d3d 100644
--- a/tests/spec/oracle/default_spec_mode.5.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.5.res.oracle
@@ -1,45 +1,4 @@
[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-* 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-* 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-* options for more info
-/* Generated by Frama-C */
-void f1(void);
-
-/*@ terminates \true;
- exits \false;
- allocates \nothing; */
-void f2(void)
-{
- f1();
- return;
-}
-
-/*@ requires \true;
- terminates \true;
- exits \false;
- assigns \result, *a;
- assigns \result \from *a;
- assigns *a \from *a;
- */
-int f3(int *a);
-
-/*@ requires \true;
- terminates \true;
- exits \false;
- assigns *b;
- allocates \nothing;
- */
-int f4(int *b)
-{
- int tmp;
- tmp = f3(b);
- return tmp;
-}
-
-
+[kernel] User Error: 'wrong_clause' is not a valid key for -generated-spec-custom.
+ 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.6.res.oracle b/tests/spec/oracle/default_spec_mode.6.res.oracle
deleted file mode 100644
index d131bef3d3d..00000000000
--- a/tests/spec/oracle/default_spec_mode.6.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[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'.
-[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
deleted file mode 100644
index d131bef3d3d..00000000000
--- a/tests/spec/oracle/default_spec_mode.7.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[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'.
-[kernel] Frama-C aborted: invalid user input.
--
GitLab