GitLab

Fastwp now adds VC explanation labels in the same way as the regular WP.
That was an oversight of existing implementation.

In a counterexample model returned by cvc4, values can be also of the form
"(mk_t__ref([0-9]*) (value))", while only the form "(mk_t__ref (value))"
was supported.

* src/driver/parse_smtv2_model_lexer.mll
MK_T__REF can be of the form "mk_t__ref([0-9]*)".

Enabling the transformation detect_polymorphism caused some variables be
of reference type and their values outputed in the form "mk_t__ref value".
This was not recognized by the counterexample model parser.

* src/driver/parse_smtv2_model_lexer.mll
Add new token corresponding to string "mk_t__ref"

* src/driver/parse_smtv2_model_parser.mly
Value can be also of the form "(mk_t__ref value)"

So that it can be used to search for other labels.

* termcode.ml
(search_labels): basically a copy of get_expls_fmla with extra argument
for the callback
(get_expls_fmla): rewritten to use search_labels

So that it can be used to search for other labels.

* termcode.ml
(search_labels): basically a copy of get_expls_fmla with extra argument
for the callback
(get_expls_fmla): rewritten to use search_labels

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.

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.

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.

The file of the form "file:line:col1:col2" was created, than split on ":"
and and int_of_string was used to get line number and colon numbers. This
failed on windows because the file name contained ':', i.e.,
"C:\...\gnatprove\p\..\p.mlw:2254:55:150".

axioms with a single "remove allprops".

use remove allprops in the driver for bitvectors.

This removes the need for exporting the theory about marks and thus the
resulting noise in the produced tasks. The patch is large due to the
dependencies between files.

This fixes (-2) mod 2 being evaluated as nonzero.

ECase(ghost e1,[branch]) and constructor application with ghost parameters
were handled incorrectly.

The following could be proved correct:

type t = A | B
function f (x:'a) : 'a = x
predicate top = A = f A
lemma bad : forall x:t. match x with A -> x = B | B -> x = B -> top end
lemma fail : false