CristalCaveGem » LustreC

Correct some problem related to new bool encoding

Correct a bug in ensures stack generation related to existential

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

Added an option for let vs exists axiomatization

ALT2 proved by framaC without human interaction

ALT_2 working with modification made by hand

Correct bug option exists

Update on c backend proof

Bugfixes and coq proof generation for lemma inv_inv

solved the bug of multiple definition of assert exists ...

add coq support

Expliciting asserts in C code

correct bug in proof printing

Push current status of proof backend

Version quasi fonctionnelle de la generation de spec.
Encore des problemes de typage

Merge latest trunk commits

Merged horn_traces branch

Prepared first stage of code reorg:
1. moved type def in lustrespec.ml
2. moved constructor and basic functions in corelang
3. Modified eexpr with prenext quantifiers

On going work: it does not compile!

Merged trunk updates

Specialized the prefix/postfix modifiers through functors arguments

Split all functions of C backends in separate files

Moved c_backend in separate folder