aboutsummaryrefslogtreecommitdiffstats
path: root/x86
ModeNameSize
-rw-r--r--Asm.v42770logstatsplain
-rw-r--r--AsmToJSON.ml1026logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml22186logstatsplain
-rw-r--r--Asmgen.v30111logstatsplain
-rw-r--r--Asmgenproof.v35087logstatsplain
-rw-r--r--Asmgenproof1.v63808logstatsplain
-rw-r--r--Builtins1.v2205logstatsplain
-rw-r--r--CBuiltins.ml3388logstatsplain
-rw-r--r--CombineOp.v5047logstatsplain
-rw-r--r--CombineOpproof.v7102logstatsplain
-rw-r--r--ConstpropOp.vp18869logstatsplain
-rw-r--r--ConstpropOpproof.v40628logstatsplain
-rw-r--r--Conventions1.v18005logstatsplain
-rw-r--r--Machregs.v12009logstatsplain
-rw-r--r--Machregsaux.ml1602logstatsplain
-rw-r--r--Machregsaux.mli1093logstatsplain
-rw-r--r--NeedOp.v9351logstatsplain
-rw-r--r--Op.v63731logstatsplain
-rw-r--r--PrintOp.ml9349logstatsplain
-rw-r--r--SelectLong.vp13074logstatsplain
-rw-r--r--SelectLongproof.v24444logstatsplain
-rw-r--r--SelectOp.vp20996logstatsplain
-rw-r--r--SelectOpproof.v39078logstatsplain
-rw-r--r--Stacklayout.v6332logstatsplain
-rw-r--r--TargetPrinter.ml36156logstatsplain
-rw-r--r--ValueAOp.v10622logstatsplain
-rw-r--r--extractionMachdep.v1420logstatsplain