GitLab

Merge branch 'counter-examples' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into counter-examples

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)"

Merge branch 'counter-examples' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into counter-examples

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".

The value of bitvector can not fit into integer range (it can be, e.g,
9223372036854775881). Values of bitvectors are stored as strings and not
converted to integers.

This is to ensure the assumption of the transformation
intro_projections_counterexmp that every variable with model label has
location. For variables without location, it makes no sense to include
them in counterexample.

Record fields labeled with label model_trace:@hide_field will be not
shown in counterexample.

Previously, "." was automatically appended to names stored in
model_trace label when creating variables corresponding to record
fields in eval_match and when projecting record fields in the
transformation intro_projections_counterexmp. Now, this is not done
and "." must be given in model_trace label of the projection or
record field.

The reason is that for SPARK, character different from "." (e.g., "'"
needs to be sometimes appended.

In standard WP, propagate also location of the expression, in fast wp,
do not propagate model labels through Eany expression.

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.

the name of the projection to projected element.

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".

Prevent loosing labels of formulas with f.t_node equal to Tquant in
transformations eliminate_algebraic and introduce_premises.

Need to compile Alt-Ergo with Nums instead of Zarith,
which is not supported by js_of_ocaml

The concatenation of strings in the list of strings returned by
bounded_split must be equal to the string being split.