aboutsummaryrefslogtreecommitdiffstats
path: root/x86
ModeNameSize
-rw-r--r--Asm.v42825logstatsplain
-rw-r--r--AsmToJSON.ml1026logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml22186logstatsplain
-rw-r--r--Asmgen.v28954logstatsplain
-rw-r--r--Asmgenproof.v34708logstatsplain
-rw-r--r--Asmgenproof1.v60488logstatsplain
-rw-r--r--CBuiltins.ml3476logstatsplain
-rw-r--r--CombineOp.v5047logstatsplain
-rw-r--r--CombineOpproof.v7102logstatsplain
-rw-r--r--ConstpropOp.vp18428logstatsplain
-rw-r--r--ConstpropOpproof.v39565logstatsplain
-rw-r--r--Conventions1.v17980logstatsplain
-rw-r--r--Machregs.v11987logstatsplain
-rw-r--r--Machregsaux.ml1369logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v9151logstatsplain
-rw-r--r--Op.v61736logstatsplain
-rw-r--r--PrintOp.ml9190logstatsplain
-rw-r--r--SelectLong.vp13064logstatsplain
-rw-r--r--SelectLongproof.v24403logstatsplain
-rw-r--r--SelectOp.vp19508logstatsplain
-rw-r--r--SelectOpproof.v36854logstatsplain
-rw-r--r--Stacklayout.v6332logstatsplain
-rw-r--r--TargetPrinter.ml35624logstatsplain
-rw-r--r--ValueAOp.v10480logstatsplain
-rw-r--r--extractionMachdep.v1420logstatsplain