assert_h.res.oracle

[kernel] Parsing assert_h.c (with 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
  fp ∈ {0}
  naan ∈ [--..--]
  s1 ∈ {0}
  nondet ∈ [--..--]
[eva] computing for function __FC_assert <- main.
  Called from assert_h.c:13.
[eva] using specification for function __FC_assert
[eva:alarm] assert_h.c:13: Warning: 
  function __FC_assert: precondition 'nonnull_c' got status unknown.
[eva] Done for function __FC_assert
[eva] computing for function __FC_assert <- main.
  Called from assert_h.c:14.
[eva:alarm] assert_h.c:14: Warning: 
  function __FC_assert: precondition 'nonnull_c' got status invalid.
[eva] Done for function __FC_assert
[eva] computing for function __FC_assert <- main.
  Called from assert_h.c:15.
[eva] assert_h.c:15: 
  function __FC_assert: precondition 'nonnull_c' got status valid.
[eva] Done for function __FC_assert
[eva] computing for function __FC_assert <- main.
  Called from assert_h.c:16.
[eva:alarm] assert_h.c:16: Warning: 
  function __FC_assert: precondition 'nonnull_c' got status invalid.
[eva] Done for function __FC_assert
[eva] computing for function __FC_assert <- main.
  Called from assert_h.c:17.
[eva:alarm] assert_h.c:17: Warning: 
  function __FC_assert: precondition 'nonnull_c' got status unknown.
[eva] Done for function __FC_assert
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main: