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.v37899logstatsplain
-rw-r--r--ConstpropOpproof.v17697logstatsplain
-rw-r--r--Machregs.v2961logstatsplain
-rw-r--r--Machregsaux.ml1538logstatsplain
-rw-r--r--Machregsaux.mli1018logstatsplain
-rw-r--r--Op.v36626logstatsplain
-rw-r--r--PrintAsm.ml23334logstatsplain
-rw-r--r--PrintAsm.mli869logstatsplain
-rw-r--r--PrintOp.ml5284logstatsplain
-rw-r--r--SelectOp.v28296logstatsplain
-rw-r--r--SelectOpproof.v32120logstatsplain
-rw-r--r--extractionMachdep.v881logstatsplain
d---------standard122logstatsplain