stdlib_h.res.oracle

[kernel] Parsing stdlib_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
  nondet ∈ [--..--]
[eva] computing for function strtol <- main.
  Called from stdlib_h.c:20.
[eva] using specification for function strtol
[eva] stdlib_h.c:20: 
  function strtol: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:20: 
  function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:20: 
  function strtol: precondition 'base_range' got status valid.
[eva] stdlib_h.c:20: 
  function strtol, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtol
[eva] computing for function strtol <- main.
  Called from stdlib_h.c:21.
[eva:alarm] stdlib_h.c:21: Warning: 
  function strtol: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:21: 
  function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:21: 
  function strtol: precondition 'base_range' got status valid.
[eva] stdlib_h.c:21: 
  function strtol, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtol
[eva] computing for function strtol <- main.
  Called from stdlib_h.c:22.
[eva:alarm] stdlib_h.c:22: Warning: 
  function strtol: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:22: 
  function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:22: 
  function strtol: precondition 'base_range' got status valid.
[eva] Done for function strtol
[eva] computing for function strtol <- main.
  Called from stdlib_h.c:23.
[eva] stdlib_h.c:23: 
  function strtol: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:23: 
  function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:23: 
  function strtol: precondition 'base_range' got status valid.
[eva] Done for function strtol
[eva] computing for function strtoll <- main.
  Called from stdlib_h.c:27.
[eva] using specification for function strtoll
[eva] stdlib_h.c:27: 
  function strtoll: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:27: 
  function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:27: 
  function strtoll: precondition 'base_range' got status valid.
[eva] stdlib_h.c:27: 
  function strtoll, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
  Called from stdlib_h.c:28.
[eva:alarm] stdlib_h.c:28: Warning: 
  function strtoll: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:28: 
  function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:28: 
  function strtoll: precondition 'base_range' got status valid.
[eva] stdlib_h.c:28: 
  function strtoll, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoll
[eva] computing for function strtoll <- main.
  Called from stdlib_h.c:29.
[eva:alarm] stdlib_h.c:29: Warning: 
  function strtoll: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:29: 
  function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:29: 
  function strtoll: precondition 'base_range' got status valid.
[eva] Done for function strtoll
[eva] computing for function strtoul <- main.
  Called from stdlib_h.c:33.
[eva] using specification for function strtoul
[eva] stdlib_h.c:33: 
  function strtoul: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:33: 
  function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:33: 
  function strtoul: precondition 'base_range' got status valid.
[eva] stdlib_h.c:33: 
  function strtoul, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
  Called from stdlib_h.c:34.
[eva:alarm] stdlib_h.c:34: Warning: 
  function strtoul: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:34: 
  function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:34: 
  function strtoul: precondition 'base_range' got status valid.
[eva] stdlib_h.c:34: 
  function strtoul, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoul
[eva] computing for function strtoul <- main.
  Called from stdlib_h.c:35.
[eva:alarm] stdlib_h.c:35: Warning: 
  function strtoul: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:35: 
  function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:35: 
  function strtoul: precondition 'base_range' got status valid.
[eva] Done for function strtoul
[eva] computing for function strtoull <- main.
  Called from stdlib_h.c:39.
[eva] using specification for function strtoull
[eva] stdlib_h.c:39: 
  function strtoull: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:39: 
  function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:39: 
  function strtoull: precondition 'base_range' got status valid.
[eva] stdlib_h.c:39: 
  function strtoull, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
  Called from stdlib_h.c:40.
[eva:alarm] stdlib_h.c:40: Warning: 
  function strtoull: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:40: 
  function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:40: 
  function strtoull: precondition 'base_range' got status valid.
[eva] stdlib_h.c:40: 
  function strtoull, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtoull
[eva] computing for function strtoull <- main.
  Called from stdlib_h.c:41.
[eva:alarm] stdlib_h.c:41: Warning: 
  function strtoull: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:41: 
  function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:41: 
  function strtoull: precondition 'base_range' got status valid.
[eva] Done for function strtoull
[eva] computing for function strtod <- main.
  Called from stdlib_h.c:46.
[eva] using specification for function strtod
[eva] stdlib_h.c:46: 
  function strtod: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:46: 
  function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:46: 
  function strtod, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtod
[eva] computing for function strtod <- main.
  Called from stdlib_h.c:47.
[eva:alarm] stdlib_h.c:47: Warning: 
  function strtod: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:47: 
  function strtod: precondition 'separation' got status valid.
[eva] stdlib_h.c:47: 
  function strtod, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtod
[eva] computing for function strtod <- main.
  Called from stdlib_h.c:48.
[eva:alarm] stdlib_h.c:48: Warning: 
  function strtod: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:48: 
  function strtod: precondition 'separation' got status valid.
[eva] Done for function strtod
[eva] computing for function strtold <- main.
  Called from stdlib_h.c:52.
[eva] using specification for function strtold
[eva] stdlib_h.c:52: 
  function strtold: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:52: 
  function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:52: 
  function strtold, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtold
[eva] computing for function strtold <- main.
  Called from stdlib_h.c:53.
[eva:alarm] stdlib_h.c:53: Warning: 
  function strtold: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:53: 
  function strtold: precondition 'separation' got status valid.
[eva] stdlib_h.c:53: 
  function strtold, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtold
[eva] computing for function strtold <- main.
  Called from stdlib_h.c:54.
[eva:alarm] stdlib_h.c:54: Warning: 
  function strtold: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:54: 
  function strtold: precondition 'separation' got status valid.
[eva] Done for function strtold
[eva] computing for function strtof <- main.
  Called from stdlib_h.c:58.
[eva] using specification for function strtof
[eva] stdlib_h.c:58: 
  function strtof: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:58: 
  function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:58: 
  function strtof, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtof
[eva] computing for function strtof <- main.
  Called from stdlib_h.c:59.
[eva:alarm] stdlib_h.c:59: Warning: 
  function strtof: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:59: 
  function strtof: precondition 'separation' got status valid.
[eva] stdlib_h.c:59: 
  function strtof, behavior store_position: precondition 'valid_endptr' got status valid.
[eva] Done for function strtof
[eva] computing for function strtof <- main.
  Called from stdlib_h.c:60.
[eva:alarm] stdlib_h.c:60: Warning: 
  function strtof: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:60: 
  function strtof: precondition 'separation' got status valid.
[eva] Done for function strtof
[eva] computing for function bsearch <- main.
  Called from stdlib_h.c:64.
[eva] using specification for function bsearch
[eva] stdlib_h.c:64: 
  function bsearch: precondition 'valid_function_compar' got status valid.
[eva] Done for function bsearch
[eva:alarm] stdlib_h.c:65: Warning: assertion got status unknown.
[eva] computing for function bsearch <- main.
  Called from stdlib_h.c:67.
[eva] stdlib_h.c:67: 
  function bsearch: precondition 'valid_function_compar' got status valid.
[eva] Done for function bsearch
[eva:alarm] stdlib_h.c:68: Warning: assertion got status unknown.
[eva] computing for function mkstemp <- main.
  Called from stdlib_h.c:82.
[eva] using specification for function mkstemp
[eva] stdlib_h.c:82: 
  function mkstemp: precondition 'valid_template' got status valid.
[eva] stdlib_h.c:82: 
  function mkstemp: precondition 'template_len' got status valid.
[eva] Done for function mkstemp
[eva] computing for function drand48 <- main.
  Called from stdlib_h.c:86.
[eva] using specification for function drand48
[eva:alarm] stdlib_h.c:86: Warning: 
  function drand48: precondition 'random48_initialized' got status invalid.
[eva] Done for function drand48
[eva] computing for function lrand48 <- main.
  Called from stdlib_h.c:90.
[eva] using specification for function lrand48
[eva:alarm] stdlib_h.c:90: Warning: 
  function lrand48: precondition 'random48_initialized' got status invalid.
[eva] Done for function lrand48
[eva] computing for function mrand48 <- main.
  Called from stdlib_h.c:94.
[eva] using specification for function mrand48
[eva:alarm] stdlib_h.c:94: Warning: 
  function mrand48: precondition 'random48_initialized' got status invalid.
[eva] Done for function mrand48
[eva] computing for function erand48 <- main.
  Called from stdlib_h.c:99.
[eva] using specification for function erand48
[eva:alarm] stdlib_h.c:99: Warning: 
  function erand48: precondition 'initialization,initialized_xsubi' got status invalid.
[eva] Done for function erand48
[eva] computing for function erand48 <- main.
  Called from stdlib_h.c:104.
[eva] stdlib_h.c:104: 
  function erand48: precondition 'initialization,initialized_xsubi' got status valid.
[eva] Done for function erand48
[eva] stdlib_h.c:105: assertion got status valid.
[eva] computing for function jrand48 <- main.
  Called from stdlib_h.c:106.
[eva] using specification for function jrand48
[eva] stdlib_h.c:106: 
  function jrand48: precondition 'initialization,initialized_xsubi' got status valid.
[eva] Done for function jrand48
[eva] stdlib_h.c:107: assertion got status valid.
[eva] computing for function nrand48 <- main.
  Called from stdlib_h.c:108.
[eva] using specification for function nrand48
[eva] stdlib_h.c:108: 
  function nrand48: precondition 'initialization,initialized_xsubi' got status valid.
[eva] Done for function nrand48
[eva] stdlib_h.c:109: assertion got status valid.
[eva] computing for function srand48 <- main.
  Called from stdlib_h.c:111.
[eva] using specification for function srand48
[eva] Done for function srand48
[eva] computing for function seed48 <- main.
  Called from stdlib_h.c:113.
[eva] using specification for function seed48
[eva] stdlib_h.c:113: 
  function seed48: precondition 'initialization,initialized_seed16v' got status valid.
[eva] Done for function seed48
[eva] computing for function lcong48 <- main.
  Called from stdlib_h.c:115.
[eva] using specification for function lcong48
[eva] Done for function lcong48
[eva] computing for function drand48 <- main.
  Called from stdlib_h.c:117.
[eva] stdlib_h.c:117: 
  function drand48: precondition 'random48_initialized' got status valid.
[eva] Done for function drand48
[eva] stdlib_h.c:118: assertion got status valid.
[eva] computing for function mrand48 <- main.
  Called from stdlib_h.c:119.
[eva] stdlib_h.c:119: 
  function mrand48: precondition 'random48_initialized' got status valid.
[eva] Done for function mrand48
[eva] stdlib_h.c:120: assertion got status valid.
[eva] computing for function lrand48 <- main.
  Called from stdlib_h.c:121.
[eva] stdlib_h.c:121: 
  function lrand48: precondition 'random48_initialized' got status valid.
[eva] Done for function lrand48
[eva] stdlib_h.c:122: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  __fc_random48_init ∈ {1}
  __fc_random48_counter[0..2] ∈ [--..--]
  base ∈ {0; 2; 36}
  sl ∈ {{ "12 34 -56" }}
  s ∈ {{ " 3.14 0x1.2p2" }}
  pl ∈ {{ "12 34 -56" + [0..9] }}
  q ∈ {{ " 3.14 0x1.2p2" + [0..13] }}
  l ∈ [0..2147483647]
  pll ∈ {{ "12 34 -56" + [0..9] }}
  ll ∈ [--..--]
  pul ∈ {{ "12 34 -56" + [0..9] }}
  ul ∈ [--..--]
  pull ∈ {{ "12 34 -56" + [0..9] }}
  ull ∈ [--..--]
  sd ∈ {{ " 3.14 0x1.2p2" }}
  pd ∈ {{ " 3.14 0x1.2p2" + [0..13] }}
  d ∈ [-0. .. 1.]
  pld ∈ {{ " 3.14 0x1.2p2" + [0..13] }}
  ld ∈ [-inf .. inf] ∪ {NaN}
  pf ∈ {{ " 3.14 0x1.2p2" + [0..13] }}
  f ∈ [-inf .. inf] ∪ {NaN}
  ai[0] ∈ {1}
    [1] ∈ {-1}
    [2] ∈ {50000}
    [3] ∈ {20}
  key ∈ {-1}
  p ∈ {{ &ai[1] }}
  tempFilename[0..9] ∈ [--..--]
  r ∈ [-1..19]
  xsubi[0..2] ∈ {42}
  seed48v[0] ∈ {0}
         [1] ∈ {4}
         [2] ∈ {2}
  res ∈ {{ &__fc_random48_counter[0] }}
  param[0] ∈ {0}
       [1] ∈ {4}
       [2] ∈ {2}
       [3] ∈ {0}
       [4] ∈ {4}
       [5] ∈ {2}
       [6] ∈ {0}
  __retres ∈ {0}