cfrontend - compcert - CompCert fork with minor modifications for Vericert.

Mode	Name	Size
-rw-r--r--	C2C.ml	44971	log stats plain
-rw-r--r--	CPragmas.ml	3556	log stats plain
-rw-r--r--	Cexec.v	83819	log stats plain
-rw-r--r--	Clight.v	28928	log stats plain
-rw-r--r--	ClightBigstep.v	21821	log stats plain
-rw-r--r--	Cminorgen.v	10229	log stats plain
-rw-r--r--	Cminorgenproof.v	82972	log stats plain
-rw-r--r--	Cop.v	60726	log stats plain
-rw-r--r--	Csem.v	32967	log stats plain
-rw-r--r--	Csharpminor.v	17323	log stats plain
-rw-r--r--	Cshmgen.v	24735	log stats plain
-rw-r--r--	Cshmgenproof.v	58905	log stats plain
-rw-r--r--	Cstrategy.v	121399	log stats plain
-rw-r--r--	Csyntax.v	9600	log stats plain
-rw-r--r--	Ctypes.v	53805	log stats plain
-rw-r--r--	Ctyping.v	70758	log stats plain
-rw-r--r--	Initializers.v	9008	log stats plain
-rw-r--r--	Initializersproof.v	32751	log stats plain
-rw-r--r--	PrintClight.ml	9377	log stats plain
-rw-r--r--	PrintCsyntax.ml	17317	log stats plain
-rw-r--r--	SimplExpr.v	18564	log stats plain
-rw-r--r--	SimplExprproof.v	81488	log stats plain
-rw-r--r--	SimplExprspec.v	43103	log stats plain
-rw-r--r--	SimplLocals.v	10596	log stats plain
-rw-r--r--	SimplLocalsproof.v	84413	log stats plain