1. 01 Jun, 2018 8 commits
    • 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
  2. 30 May, 2018 2 commits
  3. 29 May, 2018 5 commits
  4. 28 May, 2018 1 commit
  5. 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.
  6. 22 May, 2018 5 commits
  7. 18 May, 2018 1 commit
    • Raphael Rieu-Helft's avatar
      Fix #119 · 8598369d
      Raphael Rieu-Helft authored
      Nodes that are detached now keep their former obsolete status
      (cherry picked from commit 7cb941ba)
  8. 17 May, 2018 6 commits
  9. 16 May, 2018 9 commits
  10. 15 May, 2018 2 commits
    • Sylvain Dailler's avatar
      R511-024 Change model parsing for ce · 22742df5
      Sylvain Dailler authored
      Now considers the end of the model as being the last set of parenthesis
      ))) on beginning of line, not just a single one.
      * src/driver/parse_smtv2_model.ml
      (parse): Changed slightly the regexp used for end of model.
      Change-Id: I020d975e73e2430403b36bbd6beaeb9060a31668
      (cherry picked from commit 73abf2f41f1973c69814a2f6a3c0c6d77c83745a)
    • MARCHE Claude's avatar
      fix obsolete session · ed25db86
      MARCHE Claude authored