Skip to content
Snippets Groups Projects
Commit 4c65271b authored by Thibault Martin's avatar Thibault Martin Committed by Allan Blanchard
Browse files

Update tests and oracles for Populate_spec

parent 4a8862f9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 857 additions and 143 deletions
tests/spec/default_spec_combine.i
+ 153
− 10
View file @ 4c65271b
......@@ -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);
tests/spec/default_spec_combine.ml
+ 1
− 6
View file @ 4c65271b
......@@ -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
tests/spec/default_spec_custom.ml
+ 1
− 1
View file @ 4c65271b
......@@ -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
......
tests/spec/oracle/default_spec_combine.0.res.oracle
+ 212
− 24
View file @ 4c65271b
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);
tests/spec/oracle/default_spec_combine.1.res.oracle
+ 218
− 28
View file @ 4c65271b
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);
tests/spec/oracle/default_spec_combine.2.res.oracle
+ 238
− 30
View file @ 4c65271b
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);
tests/spec/oracle/default_spec_custom.0.res.oracle
+ 6
− 1
View file @ 4c65271b
......@@ -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;
......
tests/spec/oracle/default_spec_custom.1.res.oracle
+ 6
− 3
View file @ 4c65271b
......@@ -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);
......
tests/spec/oracle/default_spec_mode.0.res.oracle
+ 5
− 10
View file @ 4c65271b
......@@ -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;
......
tests/spec/oracle/default_spec_mode.1.res.oracle
+ 2
− 4
View file @ 4c65271b
......@@ -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; */
......
tests/spec/oracle/default_spec_mode.2.res.oracle
+ 8
− 14
View file @ 4c65271b
......@@ -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)
{
......
tests/spec/oracle/default_spec_mode.3.res.oracle
+ 7
− 12
View file @ 4c65271b
......@@ -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)
{
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment