1. 18 Nov, 2015 2 commits
  2. 13 Nov, 2015 1 commit
  3. 11 Nov, 2015 1 commit
  4. 03 Nov, 2015 1 commit
  5. 23 Oct, 2015 2 commits
  6. 22 Oct, 2015 3 commits
  7. 21 Oct, 2015 2 commits
  8. 19 Oct, 2015 5 commits
  9. 16 Oct, 2015 1 commit
  10. 14 Oct, 2015 1 commit
  11. 10 Oct, 2015 1 commit
  12. 07 Oct, 2015 1 commit
    • Clément Fumex's avatar
      - some modifications to bv.why/mlw : · 8761602f
      Clément Fumex authored
        + size -> size_bv
        + size_int -> size
        + change two_power_size and max_int definitions
        + add axioms to BVConverter
        + new axiom relating nth and nth_bv
        + some reorganisation
      - update coq realisation
      - modify in consequence the relevant examples and pull the completed ones out of in_progress
      8761602f
  13. 06 Oct, 2015 3 commits
  14. 02 Oct, 2015 3 commits
  15. 01 Oct, 2015 1 commit
  16. 27 Sep, 2015 1 commit
  17. 24 Sep, 2015 1 commit
  18. 23 Sep, 2015 1 commit
  19. 22 Sep, 2015 1 commit
  20. 21 Sep, 2015 1 commit
  21. 17 Sep, 2015 1 commit
  22. 09 Sep, 2015 1 commit
  23. 07 Sep, 2015 1 commit
    • David Hauzar's avatar
      Different handling of postconditions in counterexamples. · 7ef0629a
      David Hauzar authored
      Postconditions for that variables mentioned in these postconditions
      should be in counterexample are now marked with label "model_vc_post".
      
      Variables corresponding to return values are no longer handled by
      transformation intro_vc_vars_counterexmp. They must have location
      of the corresponding postcondition, label "model" or "model_trace", and
      label of the form "model_trace:name@result". Generartion of these labels
      to variables corresponding to return values created in WP is for future
      work.
      7ef0629a
  24. 04 Sep, 2015 2 commits
  25. 03 Sep, 2015 2 commits
    • David Hauzar's avatar
      Traceability for record field names in counterexamples. · b25b6a72
      David Hauzar authored
      In wp, eval_match is used to replace record fields with simple variables
      of the same type. Originally, all labels from the variable that field
      was accessed were copied to new variables representing fields of this
      variable. Therefore also "model_trace:var_name" label was copied and thus
      the field had name "var_name" in the counterexample.
      
      This commit solves this problem by appending names of the fields to
      "model_trace:*" label of new variables representing record fields.
      b25b6a72
    • Martin Clochard's avatar
      (wip) formalization of Why3 API. · 314ec01e
      Martin Clochard authored
      314ec01e