aboutsummaryrefslogtreecommitdiffstats
path: root/arm
ModeNameSize
-rw-r--r--Archi.v2556logstatsplain
-rw-r--r--Asm.v38495logstatsplain
-rw-r--r--AsmToJSON.ml919logstatsplain
-rw-r--r--Asmexpand.ml13842logstatsplain
-rw-r--r--Asmgen.v28878logstatsplain
-rw-r--r--Asmgenproof.v36713logstatsplain
-rw-r--r--Asmgenproof1.v57666logstatsplain
-rw-r--r--CBuiltins.ml2456logstatsplain
-rw-r--r--CombineOp.v4225logstatsplain
-rw-r--r--CombineOpproof.v6419logstatsplain
-rw-r--r--ConstpropOp.vp10882logstatsplain
-rw-r--r--ConstpropOpproof.v22078logstatsplain
-rw-r--r--Conventions1.v25823logstatsplain
-rw-r--r--Machregs.v6346logstatsplain
-rw-r--r--Machregsaux.ml1446logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v7316logstatsplain
-rw-r--r--Op.v45524logstatsplain
-rw-r--r--PrintOp.ml7083logstatsplain
-rw-r--r--SelectOp.vp18485logstatsplain
-rw-r--r--SelectOpproof.v31787logstatsplain
-rw-r--r--Stacklayout.v5401logstatsplain
-rw-r--r--TargetPrinter.ml34340logstatsplain
-rw-r--r--ValueAOp.v7837logstatsplain
-rw-r--r--extractionMachdep.v1333logstatsplain