fptr.res.oracle

[kernel] Parsing tests/spec/fptr.i (no preprocessing)
[kernel:annot-error] tests/spec/fptr.i:39: Warning: 
  invalid implicit conversion from 'void (*)(int )' to 'void (*)(void)'. Ignoring logic specification of function f3
/* Generated by Frama-C */
/*@
axiomatic A {
  predicate P{L}(void (*galois_fp)()) ;
  
  predicate Q{L, L2}(void (*galois_fp_old)()) ;
  
  }
 */
/*@ requires P{Pre}((void (*)())\at(fp,Pre));
    ensures Q{Pre, Post}((void (*)())\at(fp,Pre));
 */
long f0(void (*fp)(void))
{
  long __retres;
  __retres = (long)0;
  return __retres;
}

/*@ requires P{Pre}((void (*)())\at(fp,Pre));
    ensures Q{Pre, Post}((void (*)())\at(fp,Pre));
 */
long f1(void (*fp)(int ))
{
  long __retres;
  __retres = (long)0;
  return __retres;
}

/*@
axiomatic A1 {
  predicate P1{L}(void (*galois_fp)(void)) ;
  
  predicate Q1{L, L2}(void (*galois_fp_old)(void)) ;
  
  }

*/
/*@ requires P1{Pre}(\at(fp,Pre));
    ensures Q1{Pre, Post}(\at(fp,Pre)); */
long f2(void (*fp)(void))
{
  long __retres;
  __retres = (long)0;
  return __retres;
}

long f3(void (*fp)(int ))
{
  long __retres;
  __retres = (long)0;
  return __retres;
}

void my_f(void)
{
  return;
}

/*@ lemma OK{L}: P((void (*)())(&my_f)) ∧ P1(&my_f);

*/