aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
ModeNameSize
-rw-r--r--Archi.v2071logstatsplain
-rw-r--r--Asm.v34969logstatsplain
-rw-r--r--AsmToJSON.ml919logstatsplain
-rw-r--r--AsmToJSON.mli899logstatsplain
-rw-r--r--Asmexpand.ml15846logstatsplain
-rw-r--r--Asmgen.v22550logstatsplain
-rw-r--r--Asmgenproof.v33563logstatsplain
-rw-r--r--Asmgenproof1.v46213logstatsplain
-rw-r--r--CBuiltins.ml3481logstatsplain
-rw-r--r--CombineOp.v3898logstatsplain
-rw-r--r--CombineOpproof.v5874logstatsplain
-rw-r--r--ConstpropOp.vp9772logstatsplain
-rw-r--r--ConstpropOpproof.v22286logstatsplain
-rw-r--r--Conventions1.v8466logstatsplain
-rw-r--r--Machregs.v9355logstatsplain
-rw-r--r--Machregsaux.ml1369logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v6372logstatsplain
-rw-r--r--Op.v42234logstatsplain
-rw-r--r--PrintOp.ml6659logstatsplain
-rw-r--r--SelectOp.vp18429logstatsplain
-rw-r--r--SelectOpproof.v33387logstatsplain
-rw-r--r--Stacklayout.v5670logstatsplain
-rw-r--r--TargetPrinter.ml27876logstatsplain
-rw-r--r--ValueAOp.v7124logstatsplain
-rw-r--r--extractionMachdep.v1038logstatsplain