| Branch: | Tag: | Revision:

# Date Author Comment
4174a469 12/19/2014 10:50 PM Guillaume Davy

Correct some problem related to new bool encoding

93d16170 11/15/2014 01:30 PM Guillaume Davy

Correct a bug in ensures stack generation related to existential

97602f7c 11/13/2014 11:48 AM Guillaume Davy

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

690cde69 11/13/2014 10:59 AM Pierre-Loïc Garoche

Added an option for let vs exists axiomatization

65de0e13 11/06/2014 02:54 PM Guillaume Davy

ALT2 proved by framaC without human interaction

bff13707 11/05/2014 05:15 PM Guillaume Davy

ALT_2 working with modification made by hand

a93ebdab 11/05/2014 10:46 AM Guillaume Davy

Correct bug option exists

23c510d0 11/05/2014 09:29 AM Guillaume Davy

Update on c backend proof

0ba542d7 10/29/2014 11:55 PM Guillaume Davy

Bugfixes and coq proof generation for lemma inv_inv

faa5c6db 10/23/2014 01:00 PM Pierre-Loïc Garoche

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

bd09b789 10/23/2014 12:59 PM Guillaume Davy

add coq support

d1c06a39 10/23/2014 10:47 AM Pierre-Loïc Garoche

Expliciting asserts in C code

dc6c92b2 10/22/2014 08:58 AM Guillaume Davy

correct bug in proof printing

e3945827 10/13/2014 09:20 AM Guillaume Davy

Push current status of proof backend

dae9db56 07/08/2014 02:20 AM Pierre-Loïc Garoche

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

d2ca2319 07/04/2014 02:49 PM Pierre-Loïc Garoche

Merge latest trunk commits

36454535 07/03/2014 10:46 PM Pierre-Loïc Garoche

Merged horn_traces branch

0038002e 07/02/2014 05:29 PM Pierre-Loïc Garoche

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

74dd308c 06/27/2014 05:19 PM Pierre-Loïc Garoche

On going work: it does not compile!

e95470b3 06/25/2014 05:37 PM Pierre-Loïc Garoche

Merged trunk updates

713176a4 06/25/2014 12:47 PM Pierre-Loïc Garoche

Specialized the prefix/postfix modifiers through functors arguments

522938b5 06/25/2014 11:13 AM Pierre-Loïc Garoche

Split all functions of C backends in separate files

d2be420e 06/25/2014 10:15 AM Pierre-Loïc Garoche

Moved c_backend in separate folder