aboutsummaryrefslogtreecommitdiffstats
path: root/arm
ModeNameSize
-rw-r--r--Archi.v2560logstatsplain
-rw-r--r--Asm.v38859logstatsplain
-rw-r--r--AsmToJSON.ml919logstatsplain
-rw-r--r--AsmToJSON.mli899logstatsplain
-rw-r--r--Asmexpand.ml14842logstatsplain
-rw-r--r--Asmgen.v28863logstatsplain
-rw-r--r--Asmgenproof.v36042logstatsplain
-rw-r--r--Asmgenproof1.v57505logstatsplain
-rw-r--r--CBuiltins.ml2606logstatsplain
-rw-r--r--CombineOp.v4223logstatsplain
-rw-r--r--CombineOpproof.v6406logstatsplain
-rw-r--r--ConstpropOp.vp10882logstatsplain
-rw-r--r--ConstpropOpproof.v22013logstatsplain
-rw-r--r--Conventions1.v21964logstatsplain
-rw-r--r--Machregs.v6997logstatsplain
-rw-r--r--Machregsaux.ml1457logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v7298logstatsplain
-rw-r--r--Op.v45496logstatsplain
-rw-r--r--PrintOp.ml7089logstatsplain
-rw-r--r--SelectOp.vp18485logstatsplain
-rw-r--r--SelectOpproof.v31691logstatsplain
-rw-r--r--Stacklayout.v5669logstatsplain
-rw-r--r--TargetPrinter.ml32926logstatsplain
-rw-r--r--ValueAOp.v7835logstatsplain
-rw-r--r--extractionMachdep.v1333logstatsplain