aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
ModeNameSize
-rw-r--r--Asm.v25771logstatsplain
-rw-r--r--Asmgen.v19228logstatsplain
-rw-r--r--Asmgenproof.v46740logstatsplain
-rw-r--r--Asmgenproof1.v53532logstatsplain
-rw-r--r--Asmgenretaddr.v8522logstatsplain
-rw-r--r--CBuiltins.ml1492logstatsplain
-rw-r--r--ConstpropOp.v37987logstatsplain
-rw-r--r--ConstpropOpproof.v17758logstatsplain
-rw-r--r--Machregs.v2961logstatsplain
-rw-r--r--Machregsaux.ml1538logstatsplain
-rw-r--r--Machregsaux.mli1018logstatsplain
-rw-r--r--Op.v36778logstatsplain
-rw-r--r--PrintAsm.ml23335logstatsplain
-rw-r--r--PrintAsm.mli869logstatsplain
-rw-r--r--PrintOp.ml5284logstatsplain
-rw-r--r--SelectOp.v28296logstatsplain
-rw-r--r--SelectOpproof.v32376logstatsplain
-rw-r--r--extractionMachdep.v881logstatsplain
d---------standard122logstatsplain