1. 17 Nov, 2015 4 commits
    • Johannes Kanig's avatar
    • David Hauzar's avatar
      Query cvc4 for reason of answer unknown and use it for counterexamples. · 5c3038bf
      David Hauzar authored
      When resource limit is hit, cvc4 outputs useless counterexample. Query
      cvc4 for the reason of answer unknown and use the answer to decide
      whether resource limit was hit. If it was hit, do not display the
      counterexample.
      
      * src/driver/call_provers.{ml|mli}
      (parse_prover_run): If the prover answers unknown, get the information
      about the reason of this answer.
      
      * src/printer/smtv2.ml
      (print_prop_decl): Query solver for the reason of answer unknown.
      
      * src/driver/driver.ml
      (load_driver): Initialize Unknown with no information about the reason
      of answer unknown.
      
      * src/session/session.ml
      (load_result): Initialize Unknown with no information about the reason
      of answer unknown.
      
      * src/session/session_scheduler.ml
      (schedule_proof_attempt)
      (edit_proof): Initialize Unknown with no information about the reason
      of answer unknown.
      
      * src/why3session/why3session_lib.ml
      (filter_spec): Initialize Unknown with no information about the reason
      of answer unknown.
      5c3038bf
    • David Hauzar's avatar
      Reformatting of counterexample example. · 4dfa48b8
      David Hauzar authored
      4dfa48b8
    • David Hauzar's avatar
  2. 13 Nov, 2015 1 commit
  3. 09 Nov, 2015 1 commit
    • David Hauzar's avatar
      Collect the last model element with given name and location. · ed64571a
      David Hauzar authored
      Counterexample model elements with the same name and location should
      not be displayed together. Only the one that corresponds to the term
      that is later in the task should be displayed. There can be two
      counterexample elements with the same name and location if why  code
      is generated from some source language and location are locations
      in the source language. This happens e.g., if why code is generated
      from SPARK. There, the first iteration of while cycle is unrolled in
      some cases. If the task contains both a term representing a variable
      in the first iteration of unrolled loop and a term representing the
      variable in the subsequent loop iterations, only the latter is
      relevant for the counterexample and it is the one that comes after
      the former one.
      ed64571a
  4. 23 Oct, 2015 1 commit
    • David Hauzar's avatar
      Displaying of counterexamples enhanced. · d92706f7
      David Hauzar authored
      When counterexample is displayed interleaved with source code, only the
      part of the source code from the beginning to the line of the last
      counterexample element is displayed and the focus in the editor is on the
      end of that source code.
      Textual counterexample (without interleaving with source code) is not
      displayed by default. There is a debug flag debug_show_text_cntexmp that
      enables such display.
      d92706f7
  5. 22 Oct, 2015 2 commits
  6. 08 Oct, 2015 2 commits
  7. 07 Oct, 2015 2 commits
  8. 06 Oct, 2015 4 commits
  9. 30 Sep, 2015 1 commit
    • David Hauzar's avatar
      Store counterexample information related to VC in a special index. · 924c3f18
      David Hauzar authored
      Since the exact line of the construct that triggers VC may not be
      known, the possibility to map the counterexample information related
      to this construct to dedicated index instead of mapping it to line
      number was added.
      
      Note that the line of the construct that triggers VC is guaranteed to
      be known only if  this construct does not span to multiple lines or if
      the VC is not split.
      924c3f18
  10. 23 Sep, 2015 1 commit
  11. 22 Sep, 2015 1 commit
  12. 21 Sep, 2015 1 commit
    • David Hauzar's avatar
      The format of counterexample JSON output changed. · f3aa06e2
      David Hauzar authored
      Model elements in source code line are represented as list of JSON objects
      with attributes "name", "value", and "kind". The attribute "name" is a
      name of a counterexample element, the attribute "value" is the value of
      the counterexample element, and the attribute "kind" is the kind of
      counterexample element, currently one of "old", "result", "error_message",
      and "other".
      f3aa06e2
  13. 10 Sep, 2015 3 commits
  14. 09 Sep, 2015 7 commits
  15. 08 Sep, 2015 3 commits
  16. 07 Sep, 2015 6 commits