GitLab

triggering VC was not collected.

premises.

VC only in the goal.

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

source-code location.

that triggers VC.

when a abstract construct has no user postcondition
we try to add one by purifying the program expression,
that is, ensures { result = t }, where t is a term
obtained from the program expression e

program expression e may involve function calls with
preconditions (e.g. array access, division)

the purpose of this change is to limit the number
of VCs by surrounding some program expressions with
abstract (e.g. if abstract i >= 0 && a[i] = 0 end then ...)

this is not a conservative change: one may have to
add ensures { true } to recover the previous behavior
(yet there is no example in the gallery of abstract e
with e pure and no post)

note: we might want to do that automatically for if-then-else
expressions (including lazy operators)

triggers VC in Model_parser.model and printing them.

in counter-example.

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

SMTv2 printer: do not print declarations of algebraic datatypes when they are given in the syntax map

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