1. 15 Mar, 2016 5 commits
  2. 14 Mar, 2016 5 commits
  3. 10 Mar, 2016 2 commits
  4. 09 Mar, 2016 1 commit
  5. 08 Mar, 2016 3 commits
  6. 25 Feb, 2016 2 commits
  7. 22 Feb, 2016 1 commit
  8. 19 Feb, 2016 1 commit
  9. 05 Feb, 2016 9 commits
  10. 04 Feb, 2016 1 commit
    • Johannes Kanig's avatar
      N127-001 improve performance on fastWP · 2afdad2c
      Johannes Kanig authored
      On N121-024 we fixed a bug where a state was incorrectly reused during
      merge. The fix was to never reuse state when merging. This resulted in a
      performance drop.
      
      The new fix now marks states which should not be reused - basically
      states that come from raise - and when such a state is present during
      merging, we don't reuse. Otherwise, we reuse.  This seems to get us the
      performance and passes all tests.
      
      Marking is implemented simply by a flag in states
      
      * mlw_wp.ml:
      (mark) allows to set the marked flag of a state
      (empty) empty state is not marked
      (havoc) havoc doesn't change marked state
      (merge_vars, merge_regs) new argument "marked", only create a new
        variable when marked is true, otherwise reuse
      (fast_wp) in the case of Eraise, mark the used state
      
      M415-042 pass labels down to conjunctions
      
      Why3 parser groups the loop invariants into a single formula. This patch
      allows to have the VC labels on every conjunct
      
      mlw_wp.ml
      (fastwp) call wp_expl instead of t_label
      2afdad2c
  11. 02 Feb, 2016 1 commit
  12. 01 Feb, 2016 1 commit
  13. 26 Jan, 2016 1 commit
  14. 25 Jan, 2016 1 commit
  15. 23 Jan, 2016 1 commit
  16. 18 Jan, 2016 2 commits
  17. 17 Jan, 2016 1 commit
  18. 13 Jan, 2016 1 commit
  19. 12 Jan, 2016 1 commit