asm_initialized.res.oracle

[kernel] Parsing asm_initialized.i (no preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  
[eva:alarm] asm_initialized.i:10: Warning: 
  accessing uninitialized left-value. assert \initialized(&sp);
[eva:alarm] asm_initialized.i:10: Warning: 
  out of bounds write. assert \valid(sp - 2);
[kernel] asm_initialized.i:10: Warning: 
  all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  NON TERMINATING FUNCTION
[from] Computing for function main
[from] Non-terminating function main (no dependencies)
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function main:
  NON TERMINATING - NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main:
    \nothing
[inout] Inputs for function main:
    \nothing
/* Generated by Frama-C */
int main(void)
{
  int *sp;
  int x;
  /*@ ensures \initialized(&sp);
      assigns sp;
      assigns sp \from \nothing; */
  __asm__ volatile ("mov %%rsp, %0;" : "=r" (sp));
  /*@ assert Eva: initialization: \initialized(&sp); */
  /*@ assert Eva: mem_access: \valid(sp - 2); */
  *(sp - 2) = 3;
  return x;
}