title: Eva method to compute intervals [frama-c]
body: <p>My goal is to understand how Eva shrinks the intervals for a variable. for example:</p>
  <pre><code>unsigned int nondet_uint(void);
  int main()
  {
    unsigned int x=nondet_uint();
    unsigned int y=nondet_uint();
    //@ assert x &gt;= 20 &amp;&amp; x &lt;= 30;
    //@ assert y &lt;= 60;
    //@ assert(x&gt;=y);
    return 0;
  }
  </code></pre>
  <p>So, we have x=[20,30] and y=[0,60]. However, the results from Eva shrinks y to [0,30] which is where the domain may be valid.</p>
  <pre><code>[eva] ====== VALUES COMPUTED ======
  [eva:final-states] Values at end of function main:
    x ∈ [20..30]
    y ∈ [0..30]
    __retres ∈ {0}
  </code></pre>
  <p>I tried some options for the Eva plugin, but none showed the steps for it. May I ask you to provide the method or publication on how to compute these values?</p>