1. 15 Jun, 2018 1 commit
    • MARCHE Claude's avatar
      simplified contextual menu · 0c0513a5
      MARCHE Claude authored
      The contextual menu inkoved by mouse-3 is now simplified: it contains only
      the strategies and the provers that are marked visible in the preferences
  2. 13 Jun, 2018 5 commits
  3. 12 Jun, 2018 5 commits
  4. 05 Jun, 2018 3 commits
  5. 04 Jun, 2018 2 commits
  6. 01 Jun, 2018 12 commits
    • Sylvain Dailler's avatar
      Add customization of foreground colors for error messages. · 8c7aaafc
      Sylvain Dailler authored
      Black on red was not readable. Colors to be decided.
    • Sylvain Dailler's avatar
      tactic apply: add appropriate exception. simplify code and allow inductive · 7769cda4
      Sylvain Dailler authored
      As a side effect, this also modifies reflection.ml accordingly.
    • Sylvain Dailler's avatar
    • Johannes Kanig's avatar
      (no-tn-check) use parallel constant to initialize lists · 7513458b
      Johannes Kanig authored
      Change-Id: I5c9202411fe46955c80a991eca2b7d5c2272f6d4
      (cherry picked from commit 1871023be2e4ec01bc413d4f2b670c2ed208a61a)
    • Johannes Kanig's avatar
      R531-011 declare global queue in request module · 9a4e0d40
      Johannes Kanig authored
      This allows sharing of some code between unix and windows server
      * request.c
      (queue): move global variable here
      (init_request_queue): initialize global queue
      (remove_from_queue): moved here
      * server-unix.c
      (queue): remove global variable
      (server_init_listening): call init_request_queue
      (remove_from_queue): moved from here
      (handle_msg): change call to remove_from_queue, now without queue arg
      * server-win.c
      (queue): remove global variable
      (handle_msg): now call remove_from_queue
      (init): call init_request_queue
      Change-Id: I741b8f958a0678a7acdc0c40a3b6fa72f7fb7a2c
      (cherry picked from commit 77ff3c64d289cb8d3c845f52708fed9155ca49e1)
    • Johannes Kanig's avatar
      (no-tn-check) more precise comment for list_remove · 810a2588
      Johannes Kanig authored
      Change-Id: I4645da26a36023a7c0c76afaa250783384b94ccd
      (cherry picked from commit fbeff2266782c47362cbe92513d23458c5c69788)
    • Sylvain Dailler's avatar
      R515-014 Adapt new cvc4 to ce · 5b98a355
      Sylvain Dailler authored
      This commit adapts the changes made by Florian to the drivers of cvc4 for
      counterexamples (for float with cvc4 version 1.6). It reuses without
      changes the drivers he intended to use.
      I modified the model parser so that it can recognize float models of cvc4.
      * drivers/cvc4_16_counterexample.drv
      Added import smt-libv2-floats.gen.
      * src/driver/parse_smtv2_model_lexer.mll
      Added a token for float_type.
      * src/driver/parse_smtv2_model_parser.mly
      Float_type can be encountered as names in the model but produce nothing.
      Change-Id: I64b49dd1824138a5d3f98ab046da0fdbc9420e66
      (cherry picked from commit 226d70801ad449fb86d73d35ac07fcfd56b8ba65)
    • Johannes Kanig's avatar
      R518-009 fix unsoundness related to multiple handlers · 49a561d1
      Johannes Kanig authored
      There were two bugs in the Etry case for fastwp:
      - soundness issue: the case for the normal exit was wrong.  It tried to
        merge the states iteratively by pairs, which is wrong. Instead, states
        need to be merged at once. Given the traversal that was done, it wasn't
        easily fixable, so a rewrite of the entire Etry case was necessary.
      - completeness issue: some information was dropped for the exceptional
        exits. Some code is required to recover this information.
      * mlw_wp.ml
      (fast_wp_desc): fix Etry case
      Change-Id: Ic39045baa145b3933312f4d2499582a9251b2f6c
      (cherry picked from commit c50300b6f4aa193e008492a5af719ee03cd72211)
    • Sylvain Dailler's avatar
      Remove compilation warnings · 680954f5
      Sylvain Dailler authored
    • 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)
    • Sylvain Dailler's avatar
      Update ce parser to accept empty model. · 4eabbd67
      Sylvain Dailler authored
    • Sylvain Dailler's avatar
      When printing models, add labels associated to a model element name id · 3d58982b
      Sylvain Dailler authored
      This way, (labels|tags|attributes) can be retrieved on counterexamples
  7. 30 May, 2018 2 commits
  8. 29 May, 2018 5 commits
  9. 28 May, 2018 1 commit
  10. 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.
  11. 22 May, 2018 3 commits