aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
ModeNameSize
-rw-r--r--Archi.v3568logstatsplain
-rw-r--r--Asm.v56121logstatsplain
-rw-r--r--AsmToJSON.ml1024logstatsplain
-rw-r--r--Asmexpand.ml17706logstatsplain
-rw-r--r--Asmgen.v45305logstatsplain
-rw-r--r--Asmgenproof.v39396logstatsplain
-rw-r--r--Asmgenproof1.v76095logstatsplain
-rw-r--r--Builtins1.v1625logstatsplain
-rw-r--r--CBuiltins.ml3194logstatsplain
-rw-r--r--CombineOp.v4511logstatsplain
-rw-r--r--CombineOpproof.v6424logstatsplain
-rw-r--r--ConstpropOp.vp18321logstatsplain
-rw-r--r--ConstpropOpproof.v34908logstatsplain
-rw-r--r--Conventions1.v14702logstatsplain
-rw-r--r--Machregs.v7762logstatsplain
-rw-r--r--Machregsaux.ml944logstatsplain
-rw-r--r--NeedOp.v9857logstatsplain
-rw-r--r--Op.v75801logstatsplain
-rw-r--r--PrintOp.ml13911logstatsplain
-rw-r--r--SelectLong.vp18098logstatsplain
-rw-r--r--SelectLongproof.v29902logstatsplain
-rw-r--r--SelectOp.vp21125logstatsplain
-rw-r--r--SelectOpproof.v38766logstatsplain
-rw-r--r--Stacklayout.v5701logstatsplain
-rw-r--r--TargetPrinter.ml28746logstatsplain
-rw-r--r--ValueAOp.v13155logstatsplain
-rw-r--r--extractionMachdep.v1735logstatsplain