1. 17 Dec, 2018 1 commit
  2. 14 Sep, 2018 1 commit
  3. 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
  4. 29 Aug, 2018 1 commit
  5. 24 Aug, 2018 1 commit
    • Andrei Paskevich's avatar
      Subst: avoid selecting polymorphic symbols and constructors · f542a3e4
      Andrei Paskevich authored
      Also, add an .mli file and export the relevant functions.
      
      Also, provide a variant of "split_vc" in introduction.ml
      which uses subst over introduced non-model constants instead
      of "simplify_trivial_quantification". This is more efficient
      and produces better results. Commented at the moment because
      of session breakage.
      f542a3e4
  6. 20 Aug, 2018 2 commits
  7. 14 Aug, 2018 1 commit
  8. 25 Jul, 2018 1 commit
  9. 11 Jul, 2018 1 commit
    • Mário Pereira's avatar
      Why3 "bootstrap": · 0da5f41e
      Mário Pereira authored
      The code in file /src/util/pqueue.ml has been extracted from a Why3 proof,
      and is now a correct-by-construction OCaml code. This file depends on the Vector
      module, which is also an OCaml implementation extracted from another Why3 proof.
      The proofs can be found in /examples/util/
      
      This is the result of Aymeric Walch bachelor internship.
      0da5f41e
  10. 06 Jul, 2018 1 commit
  11. 04 Jul, 2018 1 commit
  12. 02 Jul, 2018 1 commit
  13. 28 Jun, 2018 1 commit
  14. 25 Jun, 2018 1 commit
  15. 24 Jun, 2018 1 commit
  16. 23 Jun, 2018 1 commit
  17. 22 Jun, 2018 2 commits
  18. 21 Jun, 2018 1 commit
    • Johannes Kanig's avatar
      R531-011 implement killing of tasks · 07b60cd3
      Johannes Kanig authored
      The why3server supports the "interrupt" command which removes a task.
      But until now, the server didn't actually kill any already running
      processes. This is now implemented.
      
      Background is that I plan some refactorings which may make use of the
      "interrupt" command, so I want it to work properly.
      
      This new code is untested on windows, because no client code actually
      uses the interrupt command in SPARK. But I tested that it doesn't cause
      regressions. It will be later tested by the new code I intend to write.
      
      *server-unix.c
      *server-win.c
      (overall): outsource some little code to new proc unit
      (handle_msg): actually kill processes
      
      * proc.c - new file
      (os_kill): new platform-dependent function to kill a process by pid
      (init_process_list): new function to init the process list
      (kill_processes): new function to kill processes from process list with
        a certain key
      (free_process): release memory held by a process record
      
      Change-Id: I7238578061c65883423f8ec538d79d9de3fb717b
      (cherry picked from commit b17873a181ff56abda9d09bc8d10c29ba036c019)
      07b60cd3
  19. 15 Jun, 2018 1 commit
  20. 08 Jun, 2018 3 commits
  21. 05 Jun, 2018 3 commits
  22. 04 Jun, 2018 1 commit
  23. 01 Jun, 2018 1 commit
    • Sylvain Dailler's avatar
      Q817-011 proof - use cvc4 for floats · 517652cd
      Sylvain Dailler authored
      Driver updates and refactoring. Add new floats drivers file.
      
      Also add Clément's old transformation (intended for colibri) for
      elimination of ident/types/etc.
      
      Change-Id: I161612592904ed3700b414c01ccab7944654d4d9
      (cherry picked from commit a82204236d1e73207dbd71b95236757d0eeacfa2)
      
      Conflicts:
      	drivers/cvc4_14.drv
      	drivers/cvc4_15.drv
      	drivers/cvc4_gnatprove.drv
      	drivers/z3_gnatprove.drv
      	drivers/z3_gnatprove_ce.drv
      517652cd
  24. 30 May, 2018 1 commit
  25. 29 May, 2018 1 commit
  26. 27 May, 2018 1 commit
    • Guillaume Melquiond's avatar
      Check whether ocamlfind might have returned the actual location of nums.cma. · 31ad65d5
      Guillaume Melquiond authored
      The standard install location of the num library is $OCAMLLIB. Thus, the
      answer of ocamlfind cannot generally be trusted since it returns the
      location of the META file. Yet, on Arch Linux, nums.cma is actually stored
      next to its META file, for some reason. So, this commit makes configure
      try this location before falling back to the standard one.
      31ad65d5
  27. 24 May, 2018 4 commits
  28. 22 May, 2018 1 commit
  29. 17 May, 2018 1 commit
  30. 09 May, 2018 2 commits