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);