diff --git a/tests/spec/default_spec_combine.i b/tests/spec/default_spec_combine.i
index 7910730ee26c916363e7519c8d9f091afe659635..59f99b915ba87eabe2481ba2d528cffa78d3849f 100644
--- a/tests/spec/default_spec_combine.i
+++ b/tests/spec/default_spec_combine.i
@@ -10,34 +10,103 @@
@ predicate P reads \nothing;
@ predicate Q reads \nothing;
@ predicate R reads \nothing;
+ @ predicate S reads \nothing;
}*/
-// Test combine exits
+// Test combine exits with unguarded behaviors and no complete
/*@ behavior A:
@ exits P;
@ behavior B:
@ exits Q;
@ exits R;
- @ complete behaviors;
+ @ behavior C:
+ @ assumes R;
+ @ exits S;
+ @*/
+void f1_unguarded(void);
+
+// Test combine exits with only guarded behaviors and complete
+// Also test when complete behaviors have no clauses exits
+/*@ behavior A:
+ @ assumes P;
+ @ behavior B:
+ @ assumes Q;
+ @ exits Q;
+ @ exits R;
+ @ behavior C:
+ @ assumes R;
+ @ exits S;
+ @ behavior D:
+ @ assumes S;
+ @ complete behaviors A, D;
+ @ complete behaviors B, C;
+ @*/
+void f1_complete(void);
+
+// Test combine exits with only guarded behaviors and no complete
+/*@ behavior A:
+ @ assumes P;
+ @ exits P;
+ @ behavior B:
+ @ assumes Q;
+ @ exits Q;
+ @ exits R;
+ @ behavior C:
+ @ assumes R;
+ @ exits S;
+ @*/
+void f1_guarded(void);
+
+// Test combine assigns with unguarded behaviors and no complete
+/*@ behavior A:
+ @ assigns *a;
+ @ behavior B:
+ @ assigns *b;
+ @ assigns *a \from c;
+ @ assigns *a \from d;
+ @ assigns *b \from c;
+ @ behavior C:
+ @ assumes R;
+ @ assigns *a, *e;
@*/
-void f1(void);
+void f2_unguarded(int* a, int *b, int c, int d, int *e);
-// Test combine assigns
+// Test combine assigns with only guarded behaviors and complete
/*@ behavior A:
+ @ assumes P;
@ assigns *a;
@ behavior B:
+ @ assumes Q;
@ assigns *b;
@ assigns *a \from c;
@ assigns *a \from d;
@ assigns *b \from c;
@ behavior C:
- @ assigns *a, *b;
+ @ assumes R;
+ @ assigns *a, *e;
@ complete behaviors;
@*/
-void f2(int* a, int *b, int c, int d);
+void f2_complete(int* a, int *b, int c, int d, int *e);
+
+// Test combine assigns with only guarded behaviors and no complete
+/*@ behavior A:
+ @ assumes P;
+ @ assigns *a;
+ @ behavior B:
+ @ assumes Q;
+ @ assigns *b;
+ @ assigns *a \from c;
+ @ assigns *a \from d;
+ @ assigns *b \from c;
+ @ behavior C:
+ @ assumes R;
+ @ assigns *a, *e;
+ @*/
+void f2_guarded(int* a, int *b, int c, int d, int *e);
+
-// Test combine requires
+// Test combine requires with unguarded behaviors and no complete
/*@ behavior A:
@ requires P;
@ requires Q;
@@ -45,11 +114,46 @@ void f2(int* a, int *b, int c, int d);
@ requires P;
@ requires R;
@ requires R;
+ @ behavior C:
+ @ assumes R;
+ @ requires S;
+ @*/
+void f3_unguarded(void);
+
+// Test combine requires with only guarded behaviors ans complete
+/*@ behavior A:
+ @ assumes P;
+ @ requires P;
+ @ requires Q;
+ @ behavior B:
+ @ assumes Q;
+ @ requires P;
+ @ requires R;
+ @ requires R;
+ @ behavior C:
+ @ assumes R;
+ @ requires S;
@ complete behaviors;
@*/
-void f3(void);
+void f3_complete(void);
+
+// Test combine requires with only guarded behaviors and no complete
+/*@ behavior A:
+ @ assumes P;
+ @ requires P;
+ @ requires Q;
+ @ behavior B:
+ @ assumes Q;
+ @ requires P;
+ @ requires R;
+ @ requires R;
+ @ behavior C:
+ @ assumes R;
+ @ requires S;
+ @*/
+void f3_guarded(void);
-// Test combine frees/allocates
+// Test combine unguarded frees/allocates and no complete
/*@ behavior A:
@ allocates \result;
@ allocates \old(a);
@@ -60,8 +164,47 @@ void f3(void);
@ allocates \old(b);
@ frees \nothing;
@ behavior C:
+ @ assumes R;
+ @ allocates \nothing;
+ @ frees a, b;
+ @*/
+int* f4_unguarded(int* a, int* b);
+
+// Test combine only guarded frees/allocates and complete
+/*@ behavior A:
+ @ assumes P;
+ @ allocates \result;
+ @ allocates \old(a);
+ @ frees b;
+ @ behavior B:
+ @ assumes Q;
+ @ allocates \result;
+ @ allocates \old(a);
+ @ allocates \old(b);
+ @ frees \nothing;
+ @ behavior C:
+ @ assumes R;
@ allocates \nothing;
@ frees a, b;
@ complete behaviors;
@*/
-int* f4(int* a, int* b);
+int* f4_complete(int* a, int* b);
+
+// Test combine only guarded frees/allocates and no complete
+/*@ behavior A:
+ @ assumes P;
+ @ allocates \result;
+ @ allocates \old(a);
+ @ frees b;
+ @ behavior B:
+ @ assumes Q;
+ @ allocates \result;
+ @ allocates \old(a);
+ @ allocates \old(b);
+ @ frees \nothing;
+ @ behavior C:
+ @ assumes R;
+ @ allocates \nothing;
+ @ frees a, b;
+ @*/
+int* f4_guarded(int* a, int* b);
diff --git a/tests/spec/default_spec_combine.ml b/tests/spec/default_spec_combine.ml
index f4a862e81c62940812c138436206d4ccb97ec9f3..8357f1034bf3aebfbe78c33a077903a82744b797 100644
--- a/tests/spec/default_spec_combine.ml
+++ b/tests/spec/default_spec_combine.ml
@@ -11,13 +11,10 @@ let gen_requires _ _ = [ ]
let gen_allocates _ _ = FreeAllocAny
let status_allocates = Property_status.Dont_know
-let gen_terminates _ _ = None
-let status_terminates = Property_status.Dont_know
-
let run () =
let open Populate_spec in
let get_spec kf =
- populate_funspec kf [`Exits; `Assigns; `Requires; `Allocates; `Terminates]
+ populate_funspec kf [`Exits; `Assigns; `Requires; `Allocates]
in
Globals.Functions.iter get_spec
@@ -28,10 +25,8 @@ let populate () =
~gen_assigns ~status_assigns
~gen_requires
~gen_allocates ~status_allocates
- ~gen_terminates ~status_terminates
"donothing"
-
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 bf4d185694f2bc9afa45bc94231a66220a33d0d0..a28b89bfb9d64f49a87d15c41027df526357daec 100644
--- a/tests/spec/default_spec_custom.ml
+++ b/tests/spec/default_spec_custom.ml
@@ -14,7 +14,7 @@ let gen_requires _ _ = [ Logic_const.(new_predicate pfalse) ]
let gen_allocates kf _ =
if Kernel_function.has_definition kf
then FreeAlloc([],[])
- else FreeAllocAny
+ else FreeAlloc([],[])
let gen_terminates kf _ =
if Kernel_function.has_definition kf then
diff --git a/tests/spec/oracle/default_spec_combine.0.res.oracle b/tests/spec/oracle/default_spec_combine.0.res.oracle
index bc19f23f4dd18373c32e5f6e531ae8cdda42d9a4..8bb154287f019a700b7eb836afe39ab5d92e297f 100644
--- a/tests/spec/oracle/default_spec_combine.0.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.0.res.oracle
@@ -1,21 +1,41 @@
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 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 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 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 clauses (allocates) in specification of prototype f4,
- generating default specification (some combined from existing behaviors),
- 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_complete,
+ generating default specification (some combined from existing behaviors), 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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
/* Generated by Frama-C */
/*@
axiomatic a {
@@ -28,6 +48,9 @@ axiomatic a {
predicate R
reads \nothing;
+ predicate S
+ reads \nothing;
+
}
*/
/*@ exits P ∨ Q ∨ R;
@@ -39,9 +62,50 @@ axiomatic a {
exits Q;
exits R;
- complete behaviors B, A;
+ behavior C:
+ assumes R;
+ exits S;
+ */
+void f1_unguarded(void);
+
+/*@ exits Q ∨ R ∨ S;
+
+ behavior A:
+ assumes P;
+
+ behavior B:
+ assumes Q;
+ exits Q;
+ exits R;
+
+ behavior C:
+ assumes R;
+ exits S;
+
+ behavior D:
+ assumes S;
+
+ complete behaviors A, D;
+ complete behaviors B, C;
*/
-void f1(void);
+void f1_complete(void);
+
+/*@ exits P ∨ Q ∨ R ∨ S;
+
+ behavior A:
+ assumes P;
+ exits P;
+
+ behavior B:
+ assumes Q;
+ exits Q;
+ exits R;
+
+ behavior C:
+ assumes R;
+ exits S;
+ */
+void f1_guarded(void);
/*@ assigns *a, *b;
assigns *a \from c;
@@ -58,42 +122,166 @@ void f1(void);
assigns *a \from d;
behavior C:
- assigns *a, *b;
+ assumes R;
+ assigns *a, *e;
+ */
+void f2_unguarded(int *a, int *b, int c, int d, int *e);
+
+/*@ assigns *a, *b, *e;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+
+ behavior A:
+ assumes P;
+ assigns *a;
+
+ behavior B:
+ assumes Q;
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assumes R;
+ assigns *a, *e;
+
+ complete behaviors C, B, A;
+ */
+void f2_complete(int *a, int *b, int c, int d, int *e);
+
+/*@ assigns *a, *b, *e;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+
+ behavior A:
+ assumes P;
+ assigns *a;
+
+ behavior B:
+ assumes Q;
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assumes R;
+ assigns *a, *e;
+ */
+void f2_guarded(int *a, int *b, int c, int d, int *e);
+
+/*@ requires (P ∧ R) ∨ (P ∧ Q);
+
+ behavior A:
+ requires P;
+ requires Q;
+
+ behavior B:
+ requires P;
+ requires R;
+ requires R;
+
+ behavior C:
+ assumes R;
+ requires S;
+ */
+void f3_unguarded(void);
+
+/*@ requires (P ∧ Q) ∨ (P ∧ R) ∨ S;
+
+ behavior A:
+ assumes P;
+ requires P;
+ requires Q;
+
+ behavior B:
+ assumes Q;
+ requires P;
+ requires R;
+ requires R;
+
+ behavior C:
+ assumes R;
+ requires S;
complete behaviors C, B, A;
*/
-void f2(int *a, int *b, int c, int d);
+void f3_complete(void);
-/*@ requires (P ∧ Q) ∨ (P ∧ R);
+/*@ requires (P ∧ R) ∨ (P ∧ Q) ∨ S;
behavior A:
+ assumes P;
requires P;
requires Q;
behavior B:
+ assumes Q;
requires P;
requires R;
requires R;
- complete behaviors B, A;
+ behavior C:
+ assumes R;
+ requires S;
+ */
+void f3_guarded(void);
+
+/*@ frees b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ assumes R;
+ frees a, b;
*/
-void f3(void);
+int *f4_unguarded(int *a, int *b);
/*@ frees a, b;
allocates \result, \old(a), \old(b);
behavior A:
+ assumes P;
frees b;
allocates \result, \old(a);
behavior B:
+ assumes Q;
allocates \result, \old(a), \old(b);
behavior C:
+ assumes R;
frees a, b;
complete behaviors C, B, A;
*/
-int *f4(int *a, int *b);
+int *f4_complete(int *a, int *b);
+
+/*@ frees a, b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ assumes P;
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ assumes Q;
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ assumes R;
+ frees a, b;
+ */
+int *f4_guarded(int *a, int *b);
diff --git a/tests/spec/oracle/default_spec_combine.1.res.oracle b/tests/spec/oracle/default_spec_combine.1.res.oracle
index a37b50f294ce90fd7930aaae2f4b99297cf84a95..faa0575f55f2cd07495f78341814f218751455dc 100644
--- a/tests/spec/oracle/default_spec_combine.1.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.1.res.oracle
@@ -1,21 +1,41 @@
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 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 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 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 clauses (terminates, allocates, requires) in specification of prototype f4,
- generating default specification (some combined from existing behaviors),
- 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_complete,
+ generating default specification (some combined from existing behaviors), 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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
/* Generated by Frama-C */
/*@
axiomatic a {
@@ -28,10 +48,12 @@ axiomatic a {
predicate R
reads \nothing;
+ predicate S
+ reads \nothing;
+
}
*/
/*@ requires \false;
- terminates \false;
exits P ∨ Q ∨ R;
behavior A:
@@ -41,12 +63,54 @@ axiomatic a {
exits Q;
exits R;
- complete behaviors B, A;
+ behavior C:
+ assumes R;
+ exits S;
+ */
+void f1_unguarded(void);
+
+/*@ requires \false;
+ exits Q ∨ R ∨ S;
+
+ behavior A:
+ assumes P;
+
+ behavior B:
+ assumes Q;
+ exits Q;
+ exits R;
+
+ behavior C:
+ assumes R;
+ exits S;
+
+ behavior D:
+ assumes S;
+
+ complete behaviors A, D;
+ complete behaviors B, C;
+ */
+void f1_complete(void);
+
+/*@ requires \false;
+ exits P ∨ Q ∨ R ∨ S;
+
+ behavior A:
+ assumes P;
+ exits P;
+
+ behavior B:
+ assumes Q;
+ exits Q;
+ exits R;
+
+ behavior C:
+ assumes R;
+ exits S;
*/
-void f1(void);
+void f1_guarded(void);
/*@ requires \false;
- terminates \false;
assigns *a, *b;
assigns *a \from c;
assigns *a \from d;
@@ -62,45 +126,171 @@ void f1(void);
assigns *a \from d;
behavior C:
- assigns *a, *b;
+ assumes R;
+ assigns *a, *e;
+ */
+void f2_unguarded(int *a, int *b, int c, int d, int *e);
+
+/*@ requires \false;
+ assigns *a, *b, *e;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+
+ behavior A:
+ assumes P;
+ assigns *a;
+
+ behavior B:
+ assumes Q;
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assumes R;
+ assigns *a, *e;
+
+ complete behaviors C, B, A;
+ */
+void f2_complete(int *a, int *b, int c, int d, int *e);
+
+/*@ requires \false;
+ assigns *a, *b, *e;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+
+ behavior A:
+ assumes P;
+ assigns *a;
+
+ behavior B:
+ assumes Q;
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assumes R;
+ assigns *a, *e;
+ */
+void f2_guarded(int *a, int *b, int c, int d, int *e);
+
+/*@ requires (P ∧ R) ∨ (P ∧ Q);
+
+ behavior A:
+ requires P;
+ requires Q;
+
+ behavior B:
+ requires P;
+ requires R;
+ requires R;
+
+ behavior C:
+ assumes R;
+ requires S;
+ */
+void f3_unguarded(void);
+
+/*@ requires (P ∧ Q) ∨ (P ∧ R) ∨ S;
+
+ behavior A:
+ assumes P;
+ requires P;
+ requires Q;
+
+ behavior B:
+ assumes Q;
+ requires P;
+ requires R;
+ requires R;
+
+ behavior C:
+ assumes R;
+ requires S;
complete behaviors C, B, A;
*/
-void f2(int *a, int *b, int c, int d);
+void f3_complete(void);
-/*@ requires (P ∧ Q) ∨ (P ∧ R);
- terminates \false;
+/*@ requires (P ∧ R) ∨ (P ∧ Q) ∨ S;
behavior A:
+ assumes P;
requires P;
requires Q;
behavior B:
+ assumes Q;
requires P;
requires R;
requires R;
- complete behaviors B, A;
+ behavior C:
+ assumes R;
+ requires S;
+ */
+void f3_guarded(void);
+
+/*@ requires \false;
+ frees b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ assumes R;
+ frees a, b;
*/
-void f3(void);
+int *f4_unguarded(int *a, int *b);
/*@ requires \false;
- terminates \false;
frees a, b;
allocates \result, \old(a), \old(b);
behavior A:
+ assumes P;
frees b;
allocates \result, \old(a);
behavior B:
+ assumes Q;
allocates \result, \old(a), \old(b);
behavior C:
+ assumes R;
frees a, b;
complete behaviors C, B, A;
*/
-int *f4(int *a, int *b);
+int *f4_complete(int *a, int *b);
+
+/*@ requires \false;
+ frees a, b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ assumes P;
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ assumes Q;
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ assumes R;
+ frees a, b;
+ */
+int *f4_guarded(int *a, int *b);
diff --git a/tests/spec/oracle/default_spec_combine.2.res.oracle b/tests/spec/oracle/default_spec_combine.2.res.oracle
index 60a9ca8fbf7571455d4215f9f39aa3142d5fc217..892d7404ea4065e8dc3147db1f74b6b5772f93db 100644
--- a/tests/spec/oracle/default_spec_combine.2.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.2.res.oracle
@@ -1,21 +1,41 @@
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 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 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 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 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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
+[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
/* Generated by Frama-C */
/*@
axiomatic a {
@@ -28,10 +48,12 @@ axiomatic a {
predicate R
reads \nothing;
+ predicate S
+ reads \nothing;
+
}
*/
-/*@ terminates \true;
- exits P ∨ Q ∨ R;
+/*@ exits P ∨ Q ∨ R;
assigns \nothing;
allocates \nothing;
@@ -42,12 +64,56 @@ axiomatic a {
exits Q;
exits R;
- complete behaviors B, A;
+ behavior C:
+ assumes R;
+ exits S;
*/
-void f1(void);
+void f1_unguarded(void);
-/*@ terminates \true;
- exits \false;
+/*@ exits Q ∨ R ∨ S;
+ assigns \nothing;
+ allocates \nothing;
+
+ behavior A:
+ assumes P;
+
+ behavior B:
+ assumes Q;
+ exits Q;
+ exits R;
+
+ behavior C:
+ assumes R;
+ exits S;
+
+ behavior D:
+ assumes S;
+
+ complete behaviors A, D;
+ complete behaviors B, C;
+ */
+void f1_complete(void);
+
+/*@ exits P ∨ Q ∨ R ∨ S;
+ assigns \nothing;
+ allocates \nothing;
+
+ behavior A:
+ assumes P;
+ exits P;
+
+ behavior B:
+ assumes Q;
+ exits Q;
+ exits R;
+
+ behavior C:
+ assumes R;
+ exits S;
+ */
+void f1_guarded(void);
+
+/*@ exits \false;
assigns *a, *b;
assigns *a \from c;
assigns *a \from d;
@@ -64,33 +130,149 @@ void f1(void);
assigns *a \from d;
behavior C:
- assigns *a, *b;
+ assumes R;
+ assigns *a, *e;
+ */
+void f2_unguarded(int *a, int *b, int c, int d, int *e);
+
+/*@ exits \false;
+ assigns *a, *b, *e;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+ allocates \nothing;
+
+ behavior A:
+ assumes P;
+ assigns *a;
+
+ behavior B:
+ assumes Q;
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assumes R;
+ assigns *a, *e;
complete behaviors C, B, A;
*/
-void f2(int *a, int *b, int c, int d);
+void f2_complete(int *a, int *b, int c, int d, int *e);
+
+/*@ exits \false;
+ assigns *a, *b, *e;
+ assigns *a \from c;
+ assigns *a \from d;
+ assigns *b \from c;
+ allocates \nothing;
+
+ behavior A:
+ assumes P;
+ assigns *a;
+
+ behavior B:
+ assumes Q;
+ assigns *b, *a;
+ assigns *b \from c;
+ assigns *a \from c;
+ assigns *a \from d;
+
+ behavior C:
+ assumes R;
+ assigns *a, *e;
+ */
+void f2_guarded(int *a, int *b, int c, int d, int *e);
+
+/*@ requires (P ∧ R) ∨ (P ∧ Q);
+ exits \false;
+ assigns \nothing;
+ allocates \nothing;
+
+ behavior A:
+ requires P;
+ requires Q;
+
+ behavior B:
+ requires P;
+ requires R;
+ requires R;
+
+ behavior C:
+ assumes R;
+ requires S;
+ */
+void f3_unguarded(void);
-/*@ requires (P ∧ Q) ∨ (P ∧ R);
- terminates \true;
+/*@ requires (P ∧ Q) ∨ (P ∧ R) ∨ S;
exits \false;
assigns \nothing;
allocates \nothing;
behavior A:
+ assumes P;
requires P;
requires Q;
behavior B:
+ assumes Q;
requires P;
requires R;
requires R;
- complete behaviors B, A;
+ behavior C:
+ assumes R;
+ requires S;
+
+ complete behaviors C, B, A;
*/
-void f3(void);
+void f3_complete(void);
-/*@ terminates \true;
+/*@ requires (P ∧ R) ∨ (P ∧ Q) ∨ S;
exits \false;
+ assigns \nothing;
+ allocates \nothing;
+
+ behavior A:
+ assumes P;
+ requires P;
+ requires Q;
+
+ behavior B:
+ assumes Q;
+ requires P;
+ requires R;
+ requires R;
+
+ behavior C:
+ assumes R;
+ requires S;
+ */
+void f3_guarded(void);
+
+/*@ exits \false;
+ assigns \result, *a, *b;
+ assigns \result \from *a, *b;
+ assigns *a \from *a, *b;
+ assigns *b \from *a, *b;
+ frees b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ assumes R;
+ frees a, b;
+ */
+int *f4_unguarded(int *a, int *b);
+
+/*@ exits \false;
assigns \result, *a, *b;
assigns \result \from *a, *b;
assigns *a \from *a, *b;
@@ -99,17 +281,43 @@ void f3(void);
allocates \result, \old(a), \old(b);
behavior A:
+ assumes P;
frees b;
allocates \result, \old(a);
behavior B:
+ assumes Q;
allocates \result, \old(a), \old(b);
behavior C:
+ assumes R;
frees a, b;
complete behaviors C, B, A;
*/
-int *f4(int *a, int *b);
+int *f4_complete(int *a, int *b);
+
+/*@ exits \false;
+ assigns \result, *a, *b;
+ assigns \result \from *a, *b;
+ assigns *a \from *a, *b;
+ assigns *b \from *a, *b;
+ frees a, b;
+ allocates \result, \old(a), \old(b);
+
+ behavior A:
+ assumes P;
+ frees b;
+ allocates \result, \old(a);
+
+ behavior B:
+ assumes Q;
+ allocates \result, \old(a), \old(b);
+
+ behavior C:
+ assumes R;
+ frees a, b;
+ */
+int *f4_guarded(int *a, int *b);
diff --git a/tests/spec/oracle/default_spec_custom.0.res.oracle b/tests/spec/oracle/default_spec_custom.0.res.oracle
index ba3feb06de673131cf915e3e4a6a95191a9fc21f..7942991288ffc539d79bfe090bb6edac453623b3 100644
--- a/tests/spec/oracle/default_spec_custom.0.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.0.res.oracle
@@ -25,6 +25,7 @@ void f1(void);
/*@ terminates \true;
exits \false;
+ assigns \nothing;
allocates \nothing; */
void f2(void)
{
@@ -43,7 +44,11 @@ int f3(int *a);
/*@ terminates \true;
exits \false;
- allocates \nothing; */
+ assigns \result, *b;
+ assigns \result \from *b;
+ assigns *b \from *b;
+ allocates \nothing;
+ */
int f4(int *b)
{
int tmp;
diff --git a/tests/spec/oracle/default_spec_custom.1.res.oracle b/tests/spec/oracle/default_spec_custom.1.res.oracle
index d95af99e11c90acdc2ad30e4d2d3a6df0461fb8b..1e9483d762792b7824fdbe296b37ac3c9a3abb3b 100644
--- a/tests/spec/oracle/default_spec_custom.1.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.1.res.oracle
@@ -3,15 +3,17 @@ 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, requires, assigns, exits) from the prototype
+ generating default specifications (terminates, allocates, 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 (terminates, requires, assigns, exits) from the prototype
+ generating default specifications (terminates, allocates, requires, assigns, exits) from the prototype
/* Generated by Frama-C */
/*@ requires \false;
terminates \false;
exits \false;
- assigns \nothing; */
+ assigns \nothing;
+ allocates \nothing;
+ */
void f1(void);
/*@ requires \false;
@@ -29,6 +31,7 @@ void f2(void)
assigns \result, *a;
assigns \result \from *a;
assigns *a \from *a;
+ allocates \nothing;
*/
int f3(int *a);
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
index bdc222f95456a3d065795b7b96a4a37a0cd2f60b..d60c199fd8a5e1d436cf7d52ba3a084dcd81b77c 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -4,24 +4,19 @@
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
+ 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
+ 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
+ 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
+ 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
+ generating default specification, 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 cc2910b141b298311f7b9d469a3599ec43e53194..a70fdeec08b451c5494b9ca76f006d5fe19b6fc1 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -4,12 +4,10 @@
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
+ 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
+ generating default specification, 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 ca5c29a70c2d8f7b67e0a12c2517346007c04971..186bd10c71b5f2094a1b5b70c7efbad09529a567 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -4,32 +4,25 @@
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
+ 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ generating default specification, see -generated-spec-* options for more info
/* Generated by Frama-C */
/*@ terminates \true;
exits \false;
@@ -39,6 +32,7 @@ void f1(void);
/*@ terminates \true;
exits \false;
+ assigns \nothing;
allocates \nothing; */
void f2(void)
{
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index 9f1437903e8415ab29e1ea9f45c02ba67057f902..064bbc6c3cea1ec4666f0822571a30b2e34a8f6c 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -4,28 +4,22 @@
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
+ 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
+ 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
+ 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
+ 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
+ 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
+ generating default specification, see -generated-spec-* options for more info
/* Generated by Frama-C */
/*@ requires \false;
terminates \true;
@@ -35,6 +29,7 @@ void f1(void);
/*@ terminates \true;
exits \false;
+ assigns \nothing;
allocates \nothing; */
void f2(void)
{