issue #11]

issue #11]

spelling

fix comments

propagate change according to kernel changes about vlogic/vgenerated; but Misc.is_generated_varinfo is much less efficient than before

[E-ACSL] add missing test

[E-ACSL] compute a more precise type for quantified variable with a strict upper bound
[E-ACSL] do not modify the type of a quantified variable anymore

[E-ACSL] convert postcondition even in presence of untranslated assigns clause
[E-ACSL] fix bug when the translation of a predicate containing \at is abruptely stopped because of a not-yet-implemented construct (the generated code contained undeclared __e_acsl_at variables)

[e-acsl] generate nice variable names whenever possible

* fixes bug:
  - fixed bug in quantifications when the bound variable got C type
  - fixed bug with DEV_FLAGS in Makefile.in
* implements new E-ACSL features:
  - invariant as assertion
  - existential quantification \exists over integers
  - equivalence <==>
  - \at as a predicate
  - conditional _ ? _ : _ (for terms and predicates)
  - binary boolean operations over terms
  - mixed assumes and ensures in function contracts
* other new features:
  - better error messages when runtime checks fail 
    (replace e_acsl_fail by e_acsl_assert)
  - remove option -e-acsl-assert
  - add E-ACSL manuals in doc/manuals
  - add files doc/Changelog, INSTALL, README and VERSION
  - new option -e-acsl-version
  - check Frama-C version at configure
  - make src-distrib
  - header 2012

[e-acsl] universal quantifications done (including testing)

[e-acsl] do not stop anymore when detecting an invalid/unsupported annotation
[e-acsl] tests for invalid quantifications