locale_h.res.oracle

[kernel] Parsing locale_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 localeconv <- main.
  Called from locale_h.c:4.
[eva] using specification for function localeconv
[eva] Done for function localeconv
[eva:alarm] locale_h.c:5: Warning: 
  out of bounds read. assert \valid_read(&lc->decimal_point);
[eva:alarm] locale_h.c:5: Warning: 
  out of bounds read. assert \valid_read(lc->decimal_point + 0);
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
  lc ∈ {{ &S___fc_locale[0] }}
  __retres ∈ [-128..127]