asm_with_contracts.res.oracle

[kernel] Parsing 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));
  /*@ for b: assigns x, y; */
  /*@ assigns x;
      assigns x \from 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;
}

__inline static void insw(unsigned short __port, void *__addr,
                          unsigned long __count)
{
  /*@ assigns __addr, __count, *((char *)__addr + (..));
      assigns __addr
        \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
      assigns __count
        \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
      assigns *((char *)__addr + (..))
        \from __port, (indirect: __addr), __count, *((char *)__addr + (..));
  */
  __asm__ volatile (
    "cld ; rep ; insw"
    : "=D" (__addr), "=c" (__count)
    : "d" (__port), "0" (__addr), "1" (__count)
    );
  return;
}