stdlib_h.1.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:21.
[eva] using specification for function strtol
[eva] stdlib_h.c:21: 
  function strtol: precondition 'valid_nptr' got status valid.
[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] stdlib_h.c:22: 
  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:23.
[eva:alarm] stdlib_h.c:23: Warning: 
  function strtol: precondition 'valid_nptr' got status unknown.
[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 strtol <- main.
  Called from stdlib_h.c:24.
[eva] stdlib_h.c:24: 
  function strtol: precondition 'valid_nptr' got status valid.
[eva] stdlib_h.c:24: 
  function strtol: precondition 'separation' got status valid.
[eva] stdlib_h.c:24: 
  function strtol: precondition 'base_range' got status valid.
[eva] Done for function strtol
[eva] computing for function strtoll <- main.
  Called from stdlib_h.c:28.
[eva] using specification for function strtoll
[eva] stdlib_h.c:28: 
  function strtoll: precondition 'valid_nptr' got status valid.
[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] stdlib_h.c:29: 
  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:30.
[eva:alarm] stdlib_h.c:30: Warning: 
  function strtoll: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:30: 
  function strtoll: precondition 'separation' got status valid.
[eva] stdlib_h.c:30: 
  function strtoll: precondition 'base_range' got status valid.
[eva] Done for function strtoll
[eva] computing for function strtoul <- main.
  Called from stdlib_h.c:34.
[eva] using specification for function strtoul
[eva] stdlib_h.c:34: 
  function strtoul: precondition 'valid_nptr' got status valid.
[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] stdlib_h.c:35: 
  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:36.
[eva:alarm] stdlib_h.c:36: Warning: 
  function strtoul: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:36: 
  function strtoul: precondition 'separation' got status valid.
[eva] stdlib_h.c:36: 
  function strtoul: precondition 'base_range' got status valid.
[eva] Done for function strtoul
[eva] computing for function strtoull <- main.
  Called from stdlib_h.c:40.
[eva] using specification for function strtoull
[eva] stdlib_h.c:40: 
  function strtoull: precondition 'valid_nptr' got status valid.
[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] stdlib_h.c:41: 
  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:42.
[eva:alarm] stdlib_h.c:42: Warning: 
  function strtoull: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:42: 
  function strtoull: precondition 'separation' got status valid.
[eva] stdlib_h.c:42: 
  function strtoull: precondition 'base_range' got status valid.
[eva] Done for function strtoull
[eva] computing for function strtod <- main.
  Called from stdlib_h.c:47.
[eva] using specification for function strtod
[eva] stdlib_h.c:47: 
  function strtod: precondition 'valid_nptr' got status valid.
[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] stdlib_h.c:48: 
  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:49.
[eva:alarm] stdlib_h.c:49: Warning: 
  function strtod: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:49: 
  function strtod: precondition 'separation' got status valid.
[eva] Done for function strtod
[eva] computing for function strtold <- main.
  Called from stdlib_h.c:53.
[eva] using specification for function strtold
[eva] stdlib_h.c:53: 
  function strtold: precondition 'valid_nptr' got status valid.
[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] stdlib_h.c:54: 
  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:55.
[eva:alarm] stdlib_h.c:55: Warning: 
  function strtold: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:55: 
  function strtold: precondition 'separation' got status valid.
[eva] Done for function strtold
[eva] computing for function strtof <- main.
  Called from stdlib_h.c:59.
[eva] using specification for function strtof
[eva] stdlib_h.c:59: 
  function strtof: precondition 'valid_nptr' got status valid.
[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] stdlib_h.c:60: 
  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:61.
[eva:alarm] stdlib_h.c:61: Warning: 
  function strtof: precondition 'valid_nptr' got status unknown.
[eva] stdlib_h.c:61: 
  function strtof: precondition 'separation' got status valid.
[eva] Done for function strtof
[eva] computing for function bsearch <- main.
  Called from stdlib_h.c:65.
[eva] using specification for function bsearch
[eva] stdlib_h.c:65: 
  function bsearch: precondition 'valid_function_compar' got status valid.
[eva] Done for function bsearch
[eva:alarm] stdlib_h.c:66: Warning: assertion got status unknown.
[eva] computing for function bsearch <- main.
  Called from stdlib_h.c:68.
[eva] stdlib_h.c:68: 
  function bsearch: precondition 'valid_function_compar' got status valid.
[eva] Done for function bsearch
[eva:alarm] stdlib_h.c:69: Warning: assertion got status unknown.
[eva] computing for function mkstemp <- main.
  Called from stdlib_h.c:83.
[eva] using specification for function mkstemp
[eva] stdlib_h.c:83: 
  function mkstemp: precondition 'valid_template' got status valid.
[eva] stdlib_h.c:83: 
  function mkstemp: precondition 'template_len' got status valid.
[eva] Done for function mkstemp
[eva] computing for function drand48 <- main.
  Called from stdlib_h.c:87.
[eva] using specification for function drand48
[eva:alarm] stdlib_h.c:87: 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:91.
[eva] using specification for function lrand48
[eva:alarm] stdlib_h.c:91: 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:95.
[eva] using specification for function mrand48
[eva:alarm] stdlib_h.c:95: 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:100.
[eva] using specification for function erand48
[eva:alarm] stdlib_h.c:100: 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:105.
[eva] stdlib_h.c:105: 
  function erand48: precondition 'initialization,initialized_xsubi' got status valid.
[eva] Done for function erand48
[eva] stdlib_h.c:106: assertion got status valid.
[eva] computing for function jrand48 <- main.
  Called from stdlib_h.c:107.
[eva] using specification for function jrand48
[eva] stdlib_h.c:107: 
  function jrand48: precondition 'initialization,initialized_xsubi' got status valid.
[eva] Done for function jrand48
[eva] stdlib_h.c:108: assertion got status valid.
[eva] computing for function nrand48 <- main.
  Called from stdlib_h.c:109.
[eva] using specification for function nrand48
[eva] stdlib_h.c:109: 
  function nrand48: precondition 'initialization,initialized_xsubi' got status valid.
[eva] Done for function nrand48
[eva] stdlib_h.c:110: assertion got status valid.
[eva] computing for function srand48 <- main.
  Called from stdlib_h.c:112.
[eva] using specification for function srand48
[eva] Done for function srand48
[eva] computing for function seed48 <- main.
  Called from stdlib_h.c:114.
[eva] using specification for function seed48
[eva] stdlib_h.c:114: 
  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:116.
[eva] using specification for function lcong48
[eva] Done for function lcong48
[eva] computing for function drand48 <- main.
  Called from stdlib_h.c:118.
[eva] stdlib_h.c:118: 
  function drand48: precondition 'random48_initialized' got status valid.
[eva] Done for function drand48
[eva] stdlib_h.c:119: assertion got status valid.
[eva] computing for function mrand48 <- main.
  Called from stdlib_h.c:120.
[eva] stdlib_h.c:120: 
  function mrand48: precondition 'random48_initialized' got status valid.
[eva] Done for function mrand48
[eva] stdlib_h.c:121: assertion got status valid.
[eva] computing for function lrand48 <- main.
  Called from stdlib_h.c:122.
[eva] stdlib_h.c:122: 
  function lrand48: precondition 'random48_initialized' got status valid.
[eva] Done for function lrand48
[eva] stdlib_h.c:123: 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..15]
  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}