1. 11 Feb, 2019 1 commit
  2. 01 Feb, 2019 1 commit
  3. 28 Nov, 2018 1 commit
    • Sylvain Dailler's avatar
      Removes model_trace added at parsing · 786526f4
      Sylvain Dailler authored
      Removes debug flag: debug_auto_model.
      Some changes in counterexamples triggered by:
      - (non counterexamples) transformations which have a specific case for
         model_trace but not for the new detection: this is intended as
         simplifications that would be done are often simplifications we want
         for counterexamples,
      - Some locations are missing in variables introduced by SP/WP which should
        explain the rest.
      
      This also disables projections for record in intro_projection_counterexmp.
      
      Correct subst_filter to be consistent with new counterexample modification
      786526f4
  4. 24 Oct, 2018 1 commit
  5. 23 Oct, 2018 2 commits
  6. 22 Oct, 2018 1 commit
  7. 21 Oct, 2018 1 commit
    • Andrei Paskevich's avatar
      WhyML: reference variables · 79f564bd
      Andrei Paskevich authored
      caveat: pass-as-reference does not work in chain relations.
              That is, 0 < r += 12 will not typecheck even
              if x is autodereferencing and (+=) has the
              first parameter with the reference marker.
      
      todo: forbid reference markers in logic, in type definitions,
            over logical symbols, etc.
      
      todo: update extraction drivers.
            why3.Ref.Ref defines
              - type "ref",
              - constructor "mk ref" (never used in Typing)
              - projection "contents" (both val and function)
              - program function "ref" (alias for "mk ref")
            ref.Ref defines
              - let-function (!)
              - program function (:=)
      
            It is important to attribute the symbols to their
            respective modules, since a program with reference
            variables may never use ref.Ref and why3.Ref.Ref
            is imported automatically.
      79f564bd
  8. 16 Oct, 2018 1 commit
  9. 15 Oct, 2018 1 commit
  10. 14 Oct, 2018 1 commit
  11. 08 Oct, 2018 1 commit
  12. 04 Oct, 2018 1 commit
  13. 28 Sep, 2018 1 commit
    • Raphael Rieu-Helft's avatar
      Add support for partial functions · 17ed1270
      Raphael Rieu-Helft authored
      Program functions can be declared as partial with "let/val partial".
      Similarly to "diverges", partial code cannot be ghost, however it does not need to be
      explicitly specified as partial.
      
      Fixes #184.
      17ed1270
  14. 11 Sep, 2018 1 commit
    • Guillaume Melquiond's avatar
      Remove handcrafted error messages (fix issues #150 and #172). · ce21b6c1
      Guillaume Melquiond authored
      Short story: it was a source of bugs, there was only one handcrafted
      message over 650, and, to quote François Pottier, "you seem to have
      misunderstood what the various commands do".
      
      Long story: the proper steps to update the error messages after modifying
      the parser are
      
      1. update the old states with --update-errors
      2. generate the new states with --list-errors
      3. compare the old and new states with --compare-errors
      4. manually reconcile the differences between the old and new states
      5. write error messages for the new states
      6. add %on_error_reduce and go back to step 1, if step 5 is too hard
      7. check that the error messages for the old states are still meaningful
      8. check that the set of states is both correct (--compile-errors) and
         complete (--compare-errors)
      
      We were doing only step 1 and half of step 8. Doing the other half of
      step 8 would have prevented issue #172 from occurring. But that would have
      meant doing step 4 after each parser modification, which was never done.
      Note that step 2 is so expensive that it is impossible to perform step 8
      during continuous integration.
      
      Given the work needed to update the error messages after a syntax change,
      I don't think we can reliably use them until WhyML no longer evolves.
      ce21b6c1
  15. 29 Aug, 2018 1 commit
  16. 21 Aug, 2018 1 commit
  17. 06 Aug, 2018 1 commit
  18. 25 Jul, 2018 1 commit
  19. 17 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      Ident: disambiguated symbolic notation · 295cacf4
      Andrei Paskevich authored
      It is possible to append an arbitary number of quote symbols
      at the end of an prefix/infix/mixfix operator:
      
                  applied form      standalone form
      
                    -' 42               (-'_)
                    x +' y              (+')
                    a[0]' <- 1          ([]'<-)
      
      Pretty-printing will use the quote symbols for disambiguation.
      
      The derived symbols can be produced by Why3 by appending
      a suffix of the form "_toto" or "'toto". These symbols can
      be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
      295cacf4
  20. 11 Jul, 2018 3 commits
  21. 07 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      confine all notation handling inside Ident · 0fea401c
      Andrei Paskevich authored
      This commit removes all hard-coded "infix ..", "prefix ..",
      and "mixfix .." from the rest of the code, and handles the
      symbolic notation entirely inside Ident. It does not change
      the notation itself.
      0fea401c
  22. 27 Jun, 2018 1 commit
  23. 21 Jun, 2018 2 commits
  24. 18 Jun, 2018 1 commit
  25. 15 Jun, 2018 2 commits
  26. 14 Jun, 2018 1 commit
  27. 07 Jun, 2018 2 commits
  28. 05 Jun, 2018 1 commit
  29. 04 Jun, 2018 1 commit
  30. 01 Jun, 2018 1 commit
  31. 31 May, 2018 2 commits
  32. 01 May, 2018 1 commit
    • Sylvain Dailler's avatar
      Tentatively add new error handling mode of menhir · 68532c3b
      Sylvain Dailler authored
      This commit tries to add the new parsing errors from menhir. It changes
      the lexer so that precise error made from the provided handcrafted.messages
      can be displayed on failure.
      Also fix #111
      
      * Makefile.in
      This adds a rule for src/parser/parser_messages.ml which either compile
      the messages or regenerates them. It needs regeneration when changes are
      added in .mly or .messages file. This also adds option .DELETE_ON_ERROR.
      
      * src/parser/lexer.mll
      The parser now uses loop_handle function from menhir (see menhir ref.
      manual).
      
      * src/parser/report.ml
      Added file from Compcert's preparser to report error from "checkpoint". It
      allows to use $0 notation in handcrafted.messages
      
      * src/parser/handcrafted.messages
      To be edited file for error messages.
      
      * bench/*
      Adding a parsing-bench for parsing errors following the model of ce-bench:
      an oracle is provided so that error messages are not lost.
      68532c3b
  33. 16 Apr, 2018 1 commit