/src/backends/C - Repository - LustreC

Name	Size	Revision	Age	Author	Comment
c_backend.ml	5.7 KB	bd09b789	almost 10 years	Guillaume Davy	add coq support
c_backend_common.ml	10.2 KB	e3945827	about 10 years	Guillaume Davy	Push current status of proof backend
c_backend_coq.ml	476 Bytes	23c510d0	almost 10 years	Guillaume Davy	Update on c backend proof
c_backend_header.ml	9.75 KB	e3945827	about 10 years	Guillaume Davy	Push current status of proof backend
c_backend_main.ml	4.36 KB	e3945827	about 10 years	Guillaume Davy	Push current status of proof backend
c_backend_makefile.ml	2.58 KB	e3945827	about 10 years	Guillaume Davy	Push current status of proof backend
c_backend_proof.ml	33.3 KB	4174a469	almost 10 years	Guillaume Davy	Correct some problem related to new bool encoding
c_backend_spec.ml	32.6 KB	4174a469	almost 10 years	Guillaume Davy	Correct some problem related to new bool encoding
c_backend_src.ml	17.7 KB	65de0e13	almost 10 years	Guillaume Davy	ALT2 proved by framaC without human interaction

#	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 ...

CristalCaveGem » LustreC