GitLab

This prevents us from binding the same oldie variable twice,
see bench/programs/good/rec_oldies.mlw

"for i = A to B do invariant I ... done" now requires (A <= B+1)
and I(A) unconditionally, and has a single outcome under I(B+1).

To restore the old behaviour (where the loop code is handled
under (A <= B) and there is a separate outcome under (A > B)),
put the label "vc:liberal_for" over the loop expression.

We believe that the (A <= B+1) condition is likely, and asserting
it by default allows us to avoid the second outbound branch.

- builtin Why3 connectors and parens are "Operator", not "Keyword"
- square brackets are Normal (just like other used-defined ops)

Dummy C printer added

Attempt to make it generic, using registered extraction functions

Compiles but not working yet

To install the Why3-related Vim files, just create a symbolic link:
  ln -s "$(why3 --print-datadir)/vim" ~/.vim/bundle/why3

Thanks to Johanness Kanig for the suggestion.

We added the generation of identifiers for counterex values inside the
printer of altergo.
Also added a file to factorize counterex printing functions that are used
for both altergo and smtv2.

* Makefile.in
(cntexmp_printer): Factorization file added to Makefile.

* src/driver/parse_smtv2_model_lexer.mll
(MODEL): Adding model keyword.

* src/driver/parse_smtv2_model_parser.mly
(output): Added parsing when keyword model is at beginning of the
 output of the prover.

* src/printer/alt_ergo.ml
Adding info mimicking smtv2.ml inside most printing functions for counterex
generation.

* src/printer/cntexmp_printer.ml
Common functions to alt_ergo.ml and smtv2.ml

* src/printer/smtv2.ml
Removed functions that are factorized into cntexmp_printer.ml