[E-ACSL] loop invariants

src/plugins/e-acsl/Makefile.in

src/plugins/e-acsl/TODO

src/plugins/e-acsl/doc/Changelog

src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf

src/plugins/e-acsl/doc/refman/e-acsl.pdf

src/plugins/e-acsl/doc/refman/loops.tex

src/plugins/e-acsl/doc/refman/speclang_modern.tex

src/plugins/e-acsl/env.ml

src/plugins/e-acsl/env.mli

src/plugins/e-acsl/loops.ml

src/plugins/e-acsl/loops.mli

src/plugins/e-acsl/main.ml

src/plugins/e-acsl/misc.ml

src/plugins/e-acsl/misc.mli

...ns/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c

...s/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c

...sl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle

...acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle