Skip to content
Snippets Groups Projects
  1. Jun 07, 2022
  2. Jun 06, 2022
  3. Jun 03, 2022
    • Valentin Perrelle's avatar
      Merge branch 'fix/eva/evaluation-oracle' into 'master' · b1fd1d45
      Valentin Perrelle authored
      [Eva] Fixes the evaluation engine when a domain oracle returns Bottom.
      
      See merge request frama-c/frama-c!3766
      b1fd1d45
    • David Bühler's avatar
      [Eva] Fixes the evaluation engine when a domain oracle returns Bottom. · d6245ae1
      David Bühler authored
      When the evaluation of any subexpression leads to Bottom, the evaluation of the
      complete expression returns only Bottom with no valuation: thus the valuation
      cache is no longer updated.
      
      However, when the evaluation of another expression requested by a domain through
      the oracle leads to Bottom, the evaluation of the primary expression may
      continue without leading to Bottom (domains are allowed to request the evaluation
      of 1/0 at any time, after all).
      
      In this case, we should properly update the cached valuation by binding Bottom
      to the expression requested by the domain, in case it should be used again in
      the evaluation (for instance if the requested evaluation was a subexpression of
      the primary target of the evaluation).
      
      And especially, if subdivided evaluations are enabled, the reference to the
      cached valuation must _always_ be reset after the oracle (even when it returns
      Bottom), as the cache has been used for successive evaluations with various
      hypotheses, and the last one is probably not sound in the general case.
      d6245ae1
  4. Jun 01, 2022
  5. May 31, 2022
  6. May 30, 2022
Loading