asm_with_contracts.res.oracle

[kernel] Parsing tests/syntax/asm_with_contracts.i (no preprocessing)
/* Generated by Frama-C */
/*@ behavior b:
      assumes z ≥ 0;
      ensures \true; */
int f(int z)
{
  int x = z;
  int y = 2;
  /*@ assigns y; */
  __asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
  /*@ assigns x;
      assigns x \from y; */
  /*@ for b: assigns x, y; */
  __asm__ ("mov %1, %0\n\t" : "=r" (x) : "r" (y));
  /*@ assigns x, y;
      
      behavior c:
        assumes x ≥ 0;
        ensures y ≥ 0;
        assigns y;
        assigns y \from x;
  */
  __asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
  return x;
}