Open requested to merge kwaxer/frama-c:master into master
This is a follow-up to the discussion from the Frama-C mailing list to bring standard inductive lists to Frama-C WP plugin.
Replaced an axiomatic definition of lists with the standard Why3 one:
- used standard Why3 list modules;
- replaced a declared list type with the standard one;
- provided definitions of all previously specified list functions except for
- replaced all axioms with lemmas except for those related to
- proved all new lemmas with Alt-Ergo and Isabelle/HOL;
- added Why3 session with Why3 realization files and associated Isabelle/HOL theories.
nth_concat received a new premise for the index
0 <= k. All other facts have been kept intact.