diff --git a/tests/misc/oracle/vis_spec.res.oracle b/tests/misc/oracle/vis_spec.res.oracle
index 8151d594e44b27c6cff757e4a8b94291f9d2aa54..70cd75db5128c85f29e576c5c3cf89351dd05a86 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 fa9afd7df9d662272abca93b3bf823aaeeda6bb2..aac82704de22ad22e1541fd65c20e2d2112f2939 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 29c80655c6cc90912e6967dfd83a900104237911..7910730ee26c916363e7519c8d9f091afe659635 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 6261077f996b4fcc155bba54723938dfea1bbf3d..f4a862e81c62940812c138436206d4ccb97ec9f3 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 826cd252d4412701ec30b57f22b403ff2e334582..bf4d185694f2bc9afa45bc94231a66220a33d0d0 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 de2d911f8eff7565ffae7f058c8865dfc174dfa8..e902308758270d68e57a2a0cda366ced22a0256c 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 0000000000000000000000000000000000000000..14210495d5fd113b5b14be8ce7f95a80ec030042
--- /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 2884fc3201922d5e68feac39dd115e64e7459974..bc19f23f4dd18373c32e5f6e531ae8cdda42d9a4 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 2d5b9acc3fbb8171dd013c06da9e4b2251ba2627..a37b50f294ce90fd7930aaae2f4b99297cf84a95 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 d3b8b07f176f95c16f9d25b6e35b8d749f43c3c6..60a9ca8fbf7571455d4215f9f39aa3142d5fc217 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 0b799247cf98e154a9689a6ef8fd268838ddd14f..ba3feb06de673131cf915e3e4a6a95191a9fc21f 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 5a21e5f94773c0f3cce2b4a87537e456ec621d47..d95af99e11c90acdc2ad30e4d2d3a6df0461fb8b 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 e36e713765661974785859139e5a07493fce89a5..bdc222f95456a3d065795b7b96a4a37a0cd2f60b 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 e36e713765661974785859139e5a07493fce89a5..cc2910b141b298311f7b9d469a3599ec43e53194 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 281c87b8e9f19209107e14fbbebbee96f1a6a3af..ca5c29a70c2d8f7b67e0a12c2517346007c04971 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 4793b616e3f74d3bb94df64927efb5c3bac299c1..9f1437903e8415ab29e1ea9f45c02ba67057f902 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 86d3a6b91f8ea103b72ddada30792e648361057b..d131bef3d3d34d4a170f09b286deada4b266c4f6 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 319e013e53fab12b1416810d7531dcc92c5b294a..d131bef3d3d34d4a170f09b286deada4b266c4f6 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 d131bef3d3d34d4a170f09b286deada4b266c4f6..0000000000000000000000000000000000000000
--- 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 d131bef3d3d34d4a170f09b286deada4b266c4f6..0000000000000000000000000000000000000000
--- 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.