default_spec_combine.2.res.oracle 8.13 KiB
Registering an mode that does nothing
[kernel] Parsing default_spec_combine.i (no preprocessing)
[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 {
predicate P
reads \nothing;
predicate Q
reads \nothing;
predicate R
reads \nothing;
predicate S
reads \nothing;
}
*/
/*@ exits P ∨ Q ∨ R;
assigns \nothing;
allocates \nothing;
behavior A:
exits P;
behavior B:
exits Q;
exits R;
behavior C:
assumes R;
exits S;
*/void f1_unguarded(void);
/*@ 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;
assigns *b \from c;
allocates \nothing;
behavior A:
assigns *a;
behavior B:
assigns *b, *a;
assigns *b \from c;
assigns *a \from c;
assigns *a \from d;
behavior C:
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_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) ∨ 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;
complete behaviors C, B, A;
*/
void f3_complete(void);
/*@ 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;
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;
complete behaviors C, B, A;
*/
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);