absent.1.res.oracle

[kernel] Parsing tests/meta/absent.c (with preprocessing)
[meta] Translation is enabled
[meta] Will process 2 properties
[meta:unknown-func] Warning: 
  g is not a valid C function, ignoring it during target computation
[meta:unknown-func] Warning: 
  g is not a valid C function, ignoring it during target computation
[meta] Successful translation
/* Generated by Frama-C */
int x;
/*@ requires xpos1: meta: x ≥ 0;
    ensures xpos1: meta: x ≥ 0; */
void f(void)
{
  if (x > 100) x --; else x ++;
  return;
}

/*@ meta "xpos1"; */
/*@ meta "xpos2";
*/