1. 24 Jun, 2018 1 commit
  2. 23 Jun, 2018 1 commit
  3. 22 Jun, 2018 2 commits
  4. 15 Jun, 2018 1 commit
  5. 08 Jun, 2018 3 commits
  6. 05 Jun, 2018 3 commits
  7. 04 Jun, 2018 1 commit
  8. 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
  9. 30 May, 2018 1 commit
  10. 29 May, 2018 1 commit
  11. 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
  12. 24 May, 2018 4 commits
  13. 22 May, 2018 1 commit
  14. 17 May, 2018 1 commit
  15. 09 May, 2018 2 commits
  16. 07 May, 2018 3 commits
  17. 04 May, 2018 1 commit
  18. 01 May, 2018 3 commits
    • 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
    • Mário Pereira's avatar
      Makefile: sml_printer -> cakeml_printer · cc1f3f37
      Mário Pereira authored
      cc1f3f37
    • Mário Pereira's avatar
      Extraction: CakeML printer (wip) · 1c4660cf
      Mário Pereira authored
      1c4660cf
  19. 12 Apr, 2018 1 commit
  20. 11 Apr, 2018 2 commits
  21. 09 Apr, 2018 3 commits
  22. 04 Apr, 2018 2 commits
  23. 23 Mar, 2018 1 commit