1. 20 Oct, 2016 2 commits
  2. 19 Oct, 2016 1 commit
  3. 18 Oct, 2016 1 commit
    • Andrei Paskevich's avatar
      vim-pathogen compliance · 7908605b
      Andrei Paskevich authored
      To install the Why3-related Vim files, just create a symbolic link:
        ln -s "$(why3 --print-datadir)/vim" ~/.vim/bundle/why3
      Thanks to Johanness Kanig for the suggestion.
  4. 11 Oct, 2016 2 commits
    • Johannes Kanig's avatar
      minor replace magic constant by named constant · 636e2c1f
      Johannes Kanig authored
      Change-Id: I296e85a9aa76594b51bf045f61df65f2e20e3a35
    • Johannes Kanig's avatar
      P909-002 allow for large exit codes · 883af7f6
      Johannes Kanig authored
      Sometimes the windows syscall GetExitCodeProcess returns a large result,
      larger than the ocaml [int] type. This is expected and not an error. For
      example the constant STATUS_QUOTA_EXCEEDED, which is 0xC0000044, may be
      a valid exit code. Such large values trip up the [int_of_string] parsing
      in the client.
      This patch implements the following solution to this problem:
      * the server doesn't care and sends the large value;
      * (the server now recognizes this value, though, to set the timeout flag
        more often)
      * the client uses an Int64 value to parse that big constant;
      * when converting to the internal Unix.process_status type, we simply
        convert to [int], because such large values don't have any special
        meaning for Why3 anyway.
      * call_provers.ml
      (parse_prover_run): now directly take the exit status as argument, and
      convert it to int;
      (handle_answer): don't wrap argument to parse_prover_run into unix type
      * prove_client.ml
      (read_answer): read Int64 type now
      * server-win.c
      (handle_child_event): set timeout boolean also when exitcode is equal to
         constant STATUS_QUOTA_EXCEEDED
      Change-Id: I1163a6f1adf1bdbfe1f53269ce0ae57dc8bd0287
  5. 29 Sep, 2016 1 commit
  6. 26 Sep, 2016 6 commits
  7. 22 Sep, 2016 2 commits
  8. 21 Sep, 2016 1 commit
  9. 19 Sep, 2016 1 commit
    • Sylvain Dailler's avatar
      Keeping keep_on_simp labels during wp generation. · 64b1fda4
      Sylvain Dailler authored
      We changed t_map_simp, track_values and the eval_match transformation
      in order to prevent them from removing terms whose head has label
       keep_on_simp. Note that simplification inside those terms is
      still possible.
      * src/core/term.ml
      (t_map_simp): Adding the case when f has label keep_on_simp.
      * src/transform/eval_match.ml
      (eval_match): Adding keep_on_simp as a stop label.
      * src/whyml/mlw_wp.ml
      (track_values): Stopping on keep_on_simp label.
  10. 16 Sep, 2016 1 commit
  11. 15 Sep, 2016 2 commits
  12. 14 Sep, 2016 6 commits
  13. 09 Sep, 2016 4 commits
  14. 06 Sep, 2016 3 commits
    • Sylvain Dailler's avatar
      Why3 altergo counterex - Allowing values to be printed for Altergo · a5d0aa0b
      Sylvain Dailler authored
      We added the generation of identifiers for counterex values inside the
      printer of altergo.
      Also added a file to factorize counterex printing functions that are used
      for both altergo and smtv2.
      * Makefile.in
      (cntexmp_printer): Factorization file added to Makefile.
      * src/driver/parse_smtv2_model_lexer.mll
      (MODEL): Adding model keyword.
      * src/driver/parse_smtv2_model_parser.mly
      (output): Added parsing when keyword model is at beginning of the
       output of the prover.
      * src/printer/alt_ergo.ml
      Adding info mimicking smtv2.ml inside most printing functions for counterex
      * src/printer/cntexmp_printer.ml
      Common functions to alt_ergo.ml and smtv2.ml
      * src/printer/smtv2.ml
      Removed functions that are factorized into cntexmp_printer.ml
    • Guillaume Melquiond's avatar
      Merge branch 'bugfix/v0.87' · 219c8bb3
      Guillaume Melquiond authored
    • Martin Clochard's avatar
  15. 02 Sep, 2016 2 commits
    • Sylvain Dailler's avatar
      Why3 counterex: Changing the way counterex value are get from prover. · 86ebcd21
      Sylvain Dailler authored
      This commit solve a problem raised by Mohamed Iguernlala. If provers give
      more values than asked, the results of counterex becomes inconsistent.
      We changed the way corresponding terms are associated to counterex value.
      Now we have a map containing the term corresponding to a counterex asked to
      a prover.
      * src/core/model_parser.ml
      (construct_name): Takes a string and create a model_name.
      (build_model_rec): Changed to use term_map which allow a name of asked
      counterex to correspond to the term asked.
      * src/core/printer.ml
      (printer_mapping): Changed type of queried_terms to store correspondance
      between names and terms.
      (printer_args): Changed initial value of queried_terms accordingly.
      * src/core/smtv2.ml
      (print_info_model): This function now returns the map of names to terms.
      (print_prop_decl): Changed variable model_list accordingly.
    • Guillaume Melquiond's avatar
  16. 01 Sep, 2016 3 commits
  17. 31 Aug, 2016 2 commits