1. 19 Sep, 2016 2 commits
  2. 26 Aug, 2016 5 commits
  3. 19 Aug, 2016 1 commit
  4. 25 Jul, 2016 1 commit
  5. 21 Jul, 2016 1 commit
  6. 15 Mar, 2016 2 commits
  7. 05 Feb, 2016 1 commit
    • Andrei Paskevich's avatar
      Mlw_expr: fix potentially unsound pattern matching in programs · 2d1a5883
      Andrei Paskevich authored
      split the ppat_ghost field in program patterns into two distinct
      conditions:
      - ppat_ghost, indicating that the pattern starts as ghost,
        meaning that all variables in it are ghost, too;
      - ppat_fail, meaning that the pattern contains a refutable
        ghost subpattern, which makes the match in the extracted code
        impossible, which makes the whole match expression ghost.
      
      Until now, the two conditions were disjunctively combined, making
      admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.
      2d1a5883
  8. 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
  9. 10 Jan, 2016 1 commit
    • Andrei Paskevich's avatar
      Mlw_expr: fix potentially unsound pattern matching in programs · eda92a0b
      Andrei Paskevich authored
      split the ppat_ghost field in program patterns into two distinct
      conditions:
      - ppat_ghost, indicating that the pattern starts as ghost,
        meaning that all variables in it are ghost, too;
      - ppat_fail, meaning that the pattern contains a refutable
        ghost subpattern, which makes the match in the extracted code
        impossible, which makes the whole match expression ghost.
      
      Until now, the two conditions were disjunctively combined, making
      admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.
      eda92a0b
  10. 04 Dec, 2015 1 commit
  11. 16 Oct, 2015 1 commit
  12. 14 Oct, 2015 1 commit
  13. 13 Oct, 2015 3 commits
  14. 08 Oct, 2015 1 commit
  15. 07 Oct, 2015 1 commit
  16. 06 Oct, 2015 2 commits
    • David Hauzar's avatar
      Not appending "." to names of record fields in counterexamples. · da802d43
      David Hauzar authored
      Previously, "." was automatically appended to names stored in
      model_trace label when creating variables corresponding to record
      fields in eval_match and when projecting record fields in the
      transformation intro_projections_counterexmp. Now, this is not done
      and "." must be given in model_trace label of the projection or
      record field.
      
      The reason is that for SPARK, character different from "." (e.g., "'"
      needs to be sometimes appended.
      da802d43
    • David Hauzar's avatar
      Propagating of model labels through expressions Eany. · 431d1caa
      David Hauzar authored
      In standard WP, propagate also location of the expression, in fast wp,
      do not propagate model labels through Eany expression.
      431d1caa
  17. 30 Sep, 2015 1 commit
  18. 20 Sep, 2015 1 commit
  19. 11 Sep, 2015 1 commit
  20. 09 Sep, 2015 2 commits
  21. 01 Sep, 2015 1 commit
  22. 30 Aug, 2015 1 commit
  23. 24 Aug, 2015 1 commit
  24. 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
  25. 22 Jul, 2015 1 commit
    • 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
  26. 21 Jul, 2015 1 commit
  27. 20 Jul, 2015 3 commits
  28. 17 Jul, 2015 1 commit