1. 28 Aug, 2015 1 commit
  2. 27 Aug, 2015 2 commits
  3. 11 Aug, 2015 3 commits
  4. 06 Aug, 2015 1 commit
    • David Hauzar's avatar
      More projection functions for a single type. · 4748a76d
      David Hauzar authored
      Transformation intro_projections_counterexmp support more
      projections for a single type Ty.ty. The projections can have a name
      and this name is appended to the name of the function symbol or
      predicate being projected.
      
      This is useful for records - for record type, there can be a projection
      for each element of the type and the name of the projection can be
      the name of the element.
      4748a76d
  5. 05 Aug, 2015 1 commit
    • David Hauzar's avatar
      Introducting constants with model labels for variables in the term · 0b53e050
      David Hauzar authored
      triggering VC.
      
      - Transformation intro_vc_vars_counterexamp introduces new constant with
      model labels for every variable in the term that trigger VC and axiom
      that this constant is equal to the variable, finds the position of the
      term that trigger VC, and saves this position in meta (for smtv2
      printer).
      
      - Transformation prepare_for_counterexmp additionally performs the
      transformation intro_vc_vars_counterexamp
      
      - smtv2 printer no longer collects the location of the term that
      triggers VC and does not collect variables in this term in a special
      way. Note that this functionality was not yet completely removed from
      the printer. It will be done so after the transformation
      intro_vc_vars_counterexmp will be tested.
      
      The rationale:
      Variables that should be displayed in counterexample are marked
      by model labels ("model", "model_projected", "model_trace:*").
      
      Variables inside the term that triggers VC should be displayed in
      counterexample for that VC. However, many VCs (tasks) can be generated
      for  a signle *.mlw file and only variables in the term that trigger
      the VC (task) that is currently proven should be displayed. That means
      that the process of selecting variables inside the term that triggers
      VC for counterexample must be done while processing the task. It is
      done by transformation intro_vc_vars_counterexmp. This means that smtv2
      printer no longer has to find the position of the term that triggers
      VC and no longer has to collect variables in this term in a special
      way.
      0b53e050
  6. 04 Aug, 2015 1 commit
    • David Hauzar's avatar
      Introducing new constant for all terms labeled by "model_projected". · 4b9104a7
      David Hauzar authored
      Transformation intro_projections_counterexmp introduce new constant c
      and axiom for all abstract functions and predicates p labeled with
      label "model_projected", not only for these for that there exists
      projection function. If the projection function does not exist,
      the axiom states c = p, if there exists projection function f,
      the axiom states c = f p.
      4b9104a7
  7. 31 Jul, 2015 1 commit
  8. 30 Jul, 2015 2 commits
  9. 29 Jul, 2015 1 commit
  10. 27 Jul, 2015 3 commits
  11. 26 Jul, 2015 2 commits
  12. 24 Jul, 2015 1 commit
  13. 22 Jul, 2015 3 commits
    • Jean-Christophe Filliâtre's avatar
      try to add some ensures to abstract when none is given · c960adbd
      Jean-Christophe Filliâtre authored
      when a abstract construct has no user postcondition
      we try to add one by purifying the program expression,
      that is, ensures { result = t }, where t is a term
      obtained from the program expression e
      
      program expression e may involve function calls with
      preconditions (e.g. array access, division)
      
      the purpose of this change is to limit the number
      of VCs by surrounding some program expressions with
      abstract (e.g. if abstract i >= 0 && a[i] = 0 end then ...)
      
      this is not a conservative change: one may have to
      add ensures { true } to recover the previous behavior
      (yet there is no example in the gallery of abstract e
      with e pure and no post)
      
      note: we might want to do that automatically for if-then-else
      expressions (including lazy operators)
      c960adbd
    • David Hauzar's avatar
      Storing counter-example model elements related to the term that · e4ef16a0
      David Hauzar authored
      triggers VC in Model_parser.model and printing them.
      e4ef16a0
    • David Hauzar's avatar
      Refactoring of getting information about the term triggering VC · be6edaf0
      David Hauzar authored
      in counter-example.
      be6edaf0
  14. 21 Jul, 2015 3 commits
  15. 20 Jul, 2015 4 commits
  16. 18 Jul, 2015 1 commit
  17. 17 Jul, 2015 3 commits
  18. 16 Jul, 2015 6 commits
  19. 15 Jul, 2015 1 commit