default_spec_mode.2.res.oracle 2.23 KiB
[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 (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;
exits \false;
assigns \nothing;
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;
}