sys_file_h.res.oracle

[kernel] Parsing tests/libc/sys_file_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
  
[eva] computing for function __va_open_void <- main.
  Called from tests/libc/sys_file_h.c:5.
[eva] using specification for function __va_open_void
[eva] tests/libc/sys_file_h.c:5: 
  function __va_open_void: precondition 'valid_filename' got status valid.
[eva] tests/libc/sys_file_h.c:5: 
  function __va_open_void: precondition 'flag_not_CREAT' got status valid.
[eva] Done for function __va_open_void
[eva] computing for function flock <- main.
  Called from tests/libc/sys_file_h.c:6.
[eva] using specification for function flock
[eva] Done for function flock
[eva] computing for function flock <- main.
  Called from tests/libc/sys_file_h.c:7.
[eva] Done for function flock
[eva] computing for function flock <- main.
  Called from tests/libc/sys_file_h.c:8.
[eva] Done for function flock
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  fd ∈ [--..--]
  r ∈ {-1; 0}
  __retres ∈ {0}