GitLab

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.

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

were added to original labels.

When eval_match creates new terms from original terms, all labels of
the original terms are copied to the new terms. The exception are
labels of the form "model_trace:*". These labels are not copied if both
original terms and new terms contain this label.

In wp, eval_match is used to replace record fields with simple variables
of the same type. Originally, all labels from the variable that field
was accessed were copied to new variables representing fields of this
variable. Therefore also "model_trace:var_name" label was copied and thus
the field had name "var_name" in the counterexample.

This commit solves this problem by appending names of the fields to
"model_trace:*" label of new variables representing record fields.

Incidentally, Try Why3 is now able to produce Alt-Ergo goals

Parsing bitvectors in the counterexample returned by the prover.

Transformation intro_projections_counterexmp support more
projections for a single type Ty.ty. The projections can have a name
and this name is appended to the name of the function symbol or
predicate being projected.

This is useful for records - for record type, there can be a projection
for each element of the type and the name of the projection can be
the name of the element.

counterexample was got.

the counter-example is empty while printing part of the counter-example
related to the term that triggers VC.

triggering VC was not collected.

construct that triggers VC in Smtv2.info instead of global variable.

that triggers VC.

triggers VC in Model_parser.model and printing them.

in counter-example.

to the counter-example model.

This line must be marked with the label "model_vc".
If VC line is postcondition, it can be marked with the label
"model_func" or "model_func:func_name". Terms corresponding to
old values of arguments will be marked with @old, term corresponding
to the function result will be marked with @result or
func_name@result if func_name was given.

Pretty printing of model element names in counter-example.
Possibility to print differently model elements corresponding to
function result, old values of function arguments and other model
elements.

This commit enable the possibility to change discriminate
behavior from Why3 source files. The 4 metas that configure
the transformation:

select_inst
select_lsinst
select_lskept
select_kept

can now be configured from source files (actually they could
before, but their value was overriden by the drivers).

The behavior in absence of annotation can be specified from
drivers using the 4 new configuration metas:

select_inst_default
select_lsinst_default
select_lskept_default
select_kept_default

They behave as their non-default counterparts, except they
have lower precedence. This avoid the forementioned
overriding problem.

Conflicts:
	src/core/model_parser.ml