imprecise_invalid_write.res.oracle

[kernel] Parsing tests/value/imprecise_invalid_write.i (no preprocessing)
[kernel] tests/value/imprecise_invalid_write.i:5: Warning: 
  Body of function main1 falls-through. Adding a return statement
[kernel] tests/value/imprecise_invalid_write.i:10: Warning: 
  Body of function main2 falls-through. Adding a return statement
[kernel] tests/value/imprecise_invalid_write.i:17: Warning: 
  Body of function main3 falls-through. Adding a return statement
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  x ∈ {0}
  s ∈ {{ "abc" }}
[eva] computing for function main1 <- main.
  Called from tests/value/imprecise_invalid_write.i:22.
[eva:alarm] tests/value/imprecise_invalid_write.i:5: Warning: 
  out of bounds write. assert \valid((int *)c);
[kernel] tests/value/imprecise_invalid_write.i:5: Warning: 
  all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2 <- main.
  Called from tests/value/imprecise_invalid_write.i:25.
[eva] tests/value/imprecise_invalid_write.i:9: 
  Assigning imprecise value to p.
  The imprecision originates from Arithmetic
  {tests/value/imprecise_invalid_write.i:9}
[eva:alarm] tests/value/imprecise_invalid_write.i:10: Warning: 
  out of bounds write. assert \valid((int *)p);
[kernel] tests/value/imprecise_invalid_write.i:10: Warning: 
  all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
  Called from tests/value/imprecise_invalid_write.i:28.
[eva] tests/value/imprecise_invalid_write.i:16: 
  Assigning imprecise value to p.
  The imprecision originates from Arithmetic
  {tests/value/imprecise_invalid_write.i:16}
[eva:alarm] tests/value/imprecise_invalid_write.i:17: Warning: 
  out of bounds write. assert \valid(p);
[kernel] tests/value/imprecise_invalid_write.i:17: Warning: 
  all target addresses were invalid. This path is assumed to be dead.
[eva] Recording results for main3
[eva] Done for function main3
[eva] Recording results for main
[eva] done for function main
[eva] tests/value/imprecise_invalid_write.i:5: 
  assertion 'Eva,mem_access' got final status invalid.
[eva] tests/value/imprecise_invalid_write.i:10: 
  assertion 'Eva,mem_access' got final status invalid.
[eva] tests/value/imprecise_invalid_write.i:17: 
  assertion 'Eva,mem_access' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
  NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main2:
  NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main3:
  NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main:
  
[from] Computing for function main1
[from] Non-terminating function main1 (no dependencies)
[from] Done for function main1
[from] Computing for function main2
[from] Non-terminating function main2 (no dependencies)
[from] Done for function main2
[from] Computing for function main3
[from] Non-terminating function main3 (no dependencies)
[from] Done for function main3
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function main1:
  NON TERMINATING - NO EFFECTS
[from] Function main2:
  NON TERMINATING - NO EFFECTS
[from] Function main3:
  NON TERMINATING - NO EFFECTS
[from] Function main:
  NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main1:
    \nothing
[inout] Inputs for function main1:
    x
[inout] Out (internal) for function main2:
    p
[inout] Inputs for function main2:
    \nothing
[inout] Out (internal) for function main3:
    p
[inout] Inputs for function main3:
    s
[inout] Out (internal) for function main:
    \nothing
[inout] Inputs for function main:
    x; s