aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend
ModeNameSize
-rw-r--r--C2C.ml37773logstatsplain
-rw-r--r--CPragmas.ml4672logstatsplain
-rw-r--r--Cexec.v82775logstatsplain
-rw-r--r--Clight.v27909logstatsplain
-rw-r--r--ClightBigstep.v21751logstatsplain
-rw-r--r--Cminorgen.v10417logstatsplain
-rw-r--r--Cminorgenproof.v82328logstatsplain
-rw-r--r--Cop.v41215logstatsplain
-rw-r--r--Csem.v32708logstatsplain
-rw-r--r--Csharpminor.v17121logstatsplain
-rw-r--r--Cshmgen.v21834logstatsplain
-rw-r--r--Cshmgenproof.v50638logstatsplain
-rw-r--r--Cstrategy.v121784logstatsplain
-rw-r--r--Csyntax.v9426logstatsplain
-rw-r--r--Ctypes.v23620logstatsplain
-rw-r--r--Initializers.v7986logstatsplain
-rw-r--r--Initializersproof.v26897logstatsplain
-rw-r--r--PrintClight.ml11064logstatsplain
-rw-r--r--PrintCsyntax.ml19242logstatsplain
-rw-r--r--SimplExpr.v18927logstatsplain
-rw-r--r--SimplExprproof.v79753logstatsplain
-rw-r--r--SimplExprspec.v44511logstatsplain
-rw-r--r--SimplLocals.v8849logstatsplain
-rw-r--r--SimplLocalsproof.v82996logstatsplain