aboutsummaryrefslogtreecommitdiffstats
path: root/arm
ModeNameSize
-rw-r--r--Archi.v2715logstatsplain
-rw-r--r--Asm.v38948logstatsplain
-rw-r--r--AsmToJSON.ml942logstatsplain
-rw-r--r--AsmToJSON.mli905logstatsplain
-rw-r--r--Asmexpand.ml17023logstatsplain
-rw-r--r--Asmgen.v29007logstatsplain
-rw-r--r--Asmgenproof.v36504logstatsplain
-rw-r--r--Asmgenproof1.v59081logstatsplain
-rw-r--r--CBuiltins.ml2828logstatsplain
-rw-r--r--CombineOp.v4223logstatsplain
-rw-r--r--CombineOpproof.v6406logstatsplain
-rw-r--r--ConstpropOp.vp11390logstatsplain
-rw-r--r--ConstpropOpproof.v22968logstatsplain
-rw-r--r--Conventions1.v23733logstatsplain
-rw-r--r--Machregs.v7116logstatsplain
-rw-r--r--Machregsaux.ml1457logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v7307logstatsplain
-rw-r--r--Op.v45639logstatsplain
-rw-r--r--PrintOp.ml7155logstatsplain
-rw-r--r--SelectLong.vp1117logstatsplain
-rw-r--r--SelectLongproof.v1221logstatsplain
-rw-r--r--SelectOp.vp18760logstatsplain
-rw-r--r--SelectOpproof.v32063logstatsplain
-rw-r--r--Stacklayout.v5666logstatsplain
-rw-r--r--TargetPrinter.ml32030logstatsplain
-rw-r--r--ValueAOp.v7847logstatsplain
-rw-r--r--extractionMachdep.v1431logstatsplain