GitLab

that triggers VC.

triggers VC in Model_parser.model and printing them.

in counter-example.

incidentally, removed also the "dirty hack"

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.

displayed in any case (even if the debug flag whyml_wp is not given).

Conflicts:
	src/core/model_parser.ml

on the command line (for the "replay" command)

This is to avoid recurrent replay error from Alt-Ergo, that does
not reliably replay a proof with the same number of steps

maps Why3 type int to OCaml type int
this is of course unsafe, unless one has proved absence of overflows

This commits enable the possibility to use variants
with different types/well-founded relations for
mutually recursive functions. This is useful if the
termination of sub-groups of those functions requires
a finer termination argument.

Example use case:
Suppose for example the following mutually recursive
function structure:

type t = A (list t)
let rec f (x:t) (...other args...)
  variant { x , other variants }
= ... f x (...different args...)...
with g (l:list t) (...other args...)
  variant { l }
= ...

The global termination argument is structural descent
trough the type t. However, as it is not enough for f
which perform a non-structural recursive calls, we add
other variants. Such variants were forbidden under the
previous behavior because f and g variants were
considered incompatible: As x and l have different
types, it was impossible to write the lexicographic
comparison of both n-uplets (even when completing g's
list).

The new behavior for mutual recursive calls is the
following: We first scan both variants to find the
longest compatible common prefix, e.g prefixes for
which types and relations are the same. Additionally,
we allow the last elements of such prefix to have
different types if their well-founded relation is
structural descent. Then, we generate a lexicographic
descent obligation on those prefixes only.

We still enforce that in a mutually recursive group,
the first component of each variant must corresponds
to the same well-founded relation. This event is much
more likely to be symptomatic of an error, as functions
with such fully mismatched variants cannot call each
other anyway. Moreover, one can always break them in
different recursive groups.

by wp displayed in counter-example only if the debug flag whyml_wp is
given.