1. 18 Jun, 2017 2 commits
  2. 16 Jun, 2017 1 commit
  3. 13 Jun, 2017 1 commit
    • Johannes Kanig's avatar
      Q520-002 fix unsoundness related to exceptions · 6c65e7ee
      Johannes Kanig authored
      On N127-001, an optimisation of the fast WP was introduced, based on
      marking states that contain variables that need to be refreshed when
      merging them. However, this "marked" status was incorrectly reset to
      false when merging states, even though some of those "unfresh" variables
      could survive the merge. The consequence was that the WP was reusing
      variables too aggressively, which would result in incorrect VCs.
      
      We now compute the marked status of a merged state from the states to be
      merged: if one of them is marked, the merged state is marked too.
      
      mlw_wp.ml:
      (merge): synthetize marked status from input states
      
      Change-Id: Ifb02c54fca58137c31762469e48b59e7c907b995
      6c65e7ee
  4. 12 Jun, 2017 6 commits
  5. 08 Jun, 2017 1 commit
  6. 24 May, 2017 1 commit
    • MARCHE Claude's avatar
      allow relative pathnames for drivers stored in the Why3 config file · eb751c1b
      MARCHE Claude authored
      If drivers in why3.conf are simple names like "alt_ergo", then the driver file
      is search as <datadir>/drivers/alt_ergo.drv
      
      This behavior is now the same as when a driver is given with option -D on the
      command line for why3prove, why3replay or why3extract
      
      Reminder: the datadir is either given as
      1) the environment variable WHY3DATA
      2) the field "datadir" of the [main] section of the
         why3 config file if exists
      3) or by default the compile-time datadir
      eb751c1b
  7. 22 May, 2017 1 commit
  8. 19 May, 2017 3 commits
  9. 16 May, 2017 1 commit
  10. 15 May, 2017 1 commit
  11. 12 May, 2017 1 commit
  12. 10 May, 2017 2 commits
  13. 05 May, 2017 1 commit
  14. 27 Apr, 2017 1 commit
  15. 20 Apr, 2017 3 commits
  16. 19 Apr, 2017 1 commit
  17. 13 Apr, 2017 2 commits
  18. 12 Apr, 2017 11 commits
    • MARCHE Claude's avatar
      fixed dates and authors · 9c4fec84
      MARCHE Claude authored
      9c4fec84
    • Sylvain Dailler's avatar
      Adding new cntexmps from spark/why3. · 084a4108
      Sylvain Dailler authored
      084a4108
    • Johannes Kanig's avatar
      PB23-035 enrich information in .spark files · a4bf8bd8
      Johannes Kanig authored
      For every check, we now print the "check_tree" into the JSON output.
      This is basically a dump of the session tree, just in a different
      format.
      
      * json.ml
      new json datatype and new function "print_json" to print it
      
      Change-Id: I0b28ac181793af4d160abc58c2634b3cbcac9b94
      a4bf8bd8
    • Sylvain Dailler's avatar
      Q217-025 Allow parsing for reference in counterexamples · f9e2170a
      Sylvain Dailler authored
      Parsing reference was forgotten in commit for Q217-025. This solves the
      problem with a new token MK_ANYTHING.
      
      * src/driver/parse_smtv2_model_lexer.mll
      (parse): Added lexing for all remaining mk*___ record constructs.
      
      * src/driver/parse_smtv2_model_parser.mly
      (smt_term): An smt_term can be a reference to a smt_term. It means it can
      be (Mk_anything smt_term).
      
      Change-Id: Ib529fee83d16d09266e526ca5fb3c65526addff5
      f9e2170a
    • Sylvain Dailler's avatar
      Q327-007 Change printer specific to cvc4 ce · ac4f6321
      Sylvain Dailler authored
      Added a counter for constructors. We print a new functions to redefine
      constructors only if there is a need.
      
      * src/printer/smtv2_cvc_ce.ml
      (print_constructor_decl): Added counter.
      (print_data_decl): Added counter.
      (print_saved_constructors): Print only if number of constructors in the
      list is greater than counter.
      
      Change-Id: Iad0f29caac961644dcbf4137341abd76c01e1090
      ac4f6321
    • Sylvain Dailler's avatar
      Q316-004 Remove get-info · 9ef97dbb
      Sylvain Dailler authored
      Do not print (get-info :reason-unknown) on smt2 output. Previously,
      detection of end of model and beginning of statistics was done by using
      the reason. We now detect a single parenthesis on a line: every cvc4 model
      ends with this (we assume statistics does not contain a line beginning
      with a closing parenthesis). As a side effect, we also find
      more counterexamples.
      
      * src/driver/parse_smtv2_model.ml
      (parse): Revert changes that were detecting Abort trap.
      
      * src/driver/parse_smtv2_model_parser.mly
      (output): Revert changes to allow absence of parenthesis at the end. Also
      removed parsing on results given by the reason. Now match on ).
      
      * src/printer/smtv2_cvc_ce.ml
      (print_prop_decl): Remove (get-info :reason-unknown).
      
      * src/printer/smtv2.ml
      (print_prop_decl): Remove get-info for coherence.
      
      Change-Id: Ifbd7b2b9ce499f8aaa020f58375d784793990965
      9ef97dbb
    • Sylvain Dailler's avatar
      Q316-004 Parse cvc4 output on mac · 4e94e8dc
      Sylvain Dailler authored
      This patch allows parsing model including the error message raised by cvc4
      on mac.
      
      * src/driver/parse_smtv2_model.ml
      (parse): Allow parsing of specific error message "Abort trap".
      (output): Allow parsing when last parenthesis is missing which is the case
      when the bug is occuring.
      
      Change-Id: I80d7276d37916e09ba4bb28478ac9a7427789771
      4e94e8dc
    • Sylvain Dailler's avatar
      Q217-025 minor typo · cffa3177
      Sylvain Dailler authored
      Change-Id: Id165717756375db150031589740470cc1e08b8ac
      cffa3177
    • Sylvain Dailler's avatar
      Q217-025 Printer to smt2: convert bool term inside type to bv · a303ae72
      Sylvain Dailler authored
      This commit solves a CVC4 limitation on boolean inside datatypes for CE.
      It converts them to bv by adding a new printer. This commit is a hack and
      it will be reverted when the bug is solved in CVC4.
      
      * Makefile.in
      (Makefile): Added new printer.
      * drivers/smtv-libv2_cvc_ce.drv:
      (printer): new printer used is smtv2_cvc_ce
      * src/driver/parse_smtv2_model_lexer.mll
      (parse): Changed the way constructor of datatype are detected.
      * src/printer/smtv2_cvc_ce.ml
      (print_constructors): Projections to bool are changed to projections
      to bitvectors. Duplicate projections are generated which returns bool and
      are used in the rest of smtv2 generated.
      
      Change-Id: Ib2eba92aa788938b0bec30f8c156e9b235896881
      a303ae72
    • Sylvain Dailler's avatar
      Q217-025 Use get-model instead of get-values for CE · 1f6da25d
      Sylvain Dailler authored
      This commit allows parsing of the result of get-model from smtsolvers.
      It changes the communication between why3 and Spark for CE to communicate
      records and array as JSON values.
      
       * src/core/model_parser.ml
      (model_value): Adding boolean and record type to model values.
      (print_*): Changed printing functions to print arrays and records as JSON
      values not as strings.
      
       * src/driver/collect_data_model.ml
      (get_variables_*): collect all internal variables of a term and put them
      into a map.
      (add_all_cvc): Add all cvc4 variables in the model to a global map.
      (add_vars_to_table): Add values of variables that can be deduced from ITE
       to the table.
      (corres_else_element): Take the definitions of functions to_rep/of_rep
      and extract the values of internal CVC variables from it.
      (refine_*): Recursively replace internal variables in a term with values
      taken from the table.
      (convert_*): Convert to type model_value from model_parser.ml.
      (create_list): Combine the following to get a list of model_value from
      the parsing of the model.
      
      * src/driver/parse_smtv2_model.ml
      (parse): Changed the detected end of model.
      
      * src/driver/parse_smtv2_model_lexer.mll
      (rule): Added tokens related to model definitions and SPARK definitions of
      records, discriminants and ref.
      
      * src/driver/parse_smtv2_model_parser.mly
      (output): Changed the parser so that it can parse a model as returned by
      Cvc4 or z3.
      
      * src/driver/smt2_model_defs.ml
      (print_*): Added printing functions for terms.
      (make_local*): Changes the AST of terms to differentiate smtsolver
      internal variables, user-defined variables and local variables.
      (subst*): Removes the local let bindings introduced by z3.
      (build_record_discr): Put definitions of discriminants inside the record
      definition.
      
       * src/printer/smtv2.ml
      (print_logic_decl): Removed get-values and added get-model.
      
      * src/transform/intro_projections_counterexmp.ml
      (intro_const_equal_to_term): Only allow projections for attributes first,
      last and field projections. Necessary when the field of a record is
      itself on array on which we want to get First and Last.
      
      * src/transform/intro_vc_vars_counterexmp.ml
      (do_intro): Some definitions moved to intro_projections_counterexmp.ml.
      
      Change-Id: Ib77fb66a2f7c53a9f54cfc300c8984e1fcec8087
      1f6da25d
    • MARCHE Claude's avatar
      update header for year 2017 · 216f2ecd
      MARCHE Claude authored
      216f2ecd