aboutsummaryrefslogtreecommitdiffstats
path: root/x86
ModeNameSize
-rw-r--r--Asm.v42485logstatsplain
-rw-r--r--AsmToJSON.ml919logstatsplain
-rw-r--r--AsmToJSON.mli899logstatsplain
-rw-r--r--Asmexpand.ml21730logstatsplain
-rw-r--r--Asmgen.v28826logstatsplain
-rw-r--r--Asmgenproof.v34667logstatsplain
-rw-r--r--Asmgenproof1.v60217logstatsplain
-rw-r--r--CBuiltins.ml3788logstatsplain
-rw-r--r--CombineOp.v5047logstatsplain
-rw-r--r--CombineOpproof.v7081logstatsplain
-rw-r--r--ConstpropOp.vp17692logstatsplain
-rw-r--r--ConstpropOpproof.v37845logstatsplain
-rw-r--r--Conventions1.v17989logstatsplain
-rw-r--r--Machregs.v11975logstatsplain
-rw-r--r--Machregsaux.ml1369logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v9152logstatsplain
-rw-r--r--Op.v59953logstatsplain
-rw-r--r--PrintOp.ml9190logstatsplain
-rw-r--r--SelectLong.vp13064logstatsplain
-rw-r--r--SelectLongproof.v24407logstatsplain
-rw-r--r--SelectOp.vp19181logstatsplain
-rw-r--r--SelectOpproof.v35524logstatsplain
-rw-r--r--Stacklayout.v6334logstatsplain
-rw-r--r--TargetPrinter.ml33474logstatsplain
-rw-r--r--ValueAOp.v10480logstatsplain
-rw-r--r--extractionMachdep.v1198logstatsplain