aboutsummaryrefslogtreecommitdiffstats
path: root/arm
ModeNameSize
-rw-r--r--Archi.v3728logstatsplain
-rw-r--r--Asm.v42331logstatsplain
-rw-r--r--AsmToJSON.ml16304logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml23026logstatsplain
-rw-r--r--Asmgen.v30636logstatsplain
-rw-r--r--Asmgenproof.v37944logstatsplain
-rw-r--r--Asmgenproof1.v62871logstatsplain
l---------BTL_SEsimplify.v27logstatsplain
-rw-r--r--Builtins1.v1625logstatsplain
-rw-r--r--CBuiltins.ml2088logstatsplain
-rw-r--r--CSE2deps.v1620logstatsplain
-rw-r--r--CSE2depsproof.v7121logstatsplain
-rw-r--r--CombineOp.v4223logstatsplain
-rw-r--r--CombineOpproof.v6429logstatsplain
-rw-r--r--Constantexpand.ml5897logstatsplain
-rw-r--r--ConstpropOp.vp13557logstatsplain
-rw-r--r--ConstpropOpproof.v28803logstatsplain
-rw-r--r--Conventions1.v17190logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1405logstatsplain
l---------ExpansionOracle.ml29logstatsplain
-rw-r--r--Machregs.v7182logstatsplain
-rw-r--r--Machregsaux.ml1101logstatsplain
-rw-r--r--Machregsaux.mli939logstatsplain
-rw-r--r--NeedOp.v7503logstatsplain
-rw-r--r--Op.v50136logstatsplain
l---------PrepassSchedulingOracle.ml33logstatsplain
-rw-r--r--PrintOp.ml7314logstatsplain
-rw-r--r--SelectLong.vp1127logstatsplain
-rw-r--r--SelectLongproof.v1262logstatsplain
-rw-r--r--SelectOp.vp19301logstatsplain
-rw-r--r--SelectOpproof.v33464logstatsplain
-rw-r--r--Stacklayout.v5395logstatsplain
-rw-r--r--TargetPrinter.ml25626logstatsplain
-rw-r--r--ValueAOp.v7989logstatsplain
-rw-r--r--extractionMachdep.v1917logstatsplain