aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
ModeNameSize
-rw-r--r--Archi.v3548logstatsplain
-rw-r--r--Asm.v59876logstatsplain
-rw-r--r--AsmToJSON.ml1024logstatsplain
-rw-r--r--Asmblock.v40925logstatsplain
-rw-r--r--Asmblockdeps.v103245logstatsplain
-rw-r--r--Asmblockgen.v49704logstatsplain
-rw-r--r--Asmblockgenproof.v61704logstatsplain
-rw-r--r--Asmblockgenproof0.v28399logstatsplain
-rw-r--r--Asmblockgenproof1.v82650logstatsplain
-rw-r--r--Asmblockprops.v3946logstatsplain
-rw-r--r--Asmexpand.ml18333logstatsplain
-rw-r--r--Asmgen.v24469logstatsplain
-rw-r--r--Asmgenproof.v87095logstatsplain
-rw-r--r--Asmgenproof1.v76095logstatsplain
-rw-r--r--BTL_SEsimplify.v1317logstatsplain
-rw-r--r--Builtins1.v1625logstatsplain
-rw-r--r--CBuiltins.ml3194logstatsplain
-rw-r--r--CSE2deps.v1624logstatsplain
-rw-r--r--CSE2depsproof.v7126logstatsplain
-rw-r--r--CombineOp.v4511logstatsplain
-rw-r--r--CombineOpproof.v6424logstatsplain
-rw-r--r--ConstpropOp.vp18321logstatsplain
-rw-r--r--ConstpropOpproof.v36022logstatsplain
-rw-r--r--Conventions1.v14101logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1595logstatsplain
-rw-r--r--ExpansionOracle.ml782logstatsplain
-rw-r--r--Machregs.v7811logstatsplain
-rw-r--r--Machregsaux.ml1156logstatsplain
-rw-r--r--Machregsaux.mli1004logstatsplain
-rw-r--r--NeedOp.v9857logstatsplain
-rw-r--r--Op.v78273logstatsplain
-rw-r--r--OpWeights.ml14383logstatsplain
-rw-r--r--OpWeightsAsm.ml7251logstatsplain
-rw-r--r--PeepholeOracle.ml25734logstatsplain
-rw-r--r--PostpassScheduling.v5075logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml19784logstatsplain
-rw-r--r--PostpassSchedulingproof.v15925logstatsplain
-rw-r--r--PrepassSchedulingOracle.ml11427logstatsplain
-rw-r--r--PrepassSchedulingOracleDeps.ml871logstatsplain
-rw-r--r--PrintOp.ml13911logstatsplain
-rw-r--r--SelectLong.vp18098logstatsplain
-rw-r--r--SelectLongproof.v30433logstatsplain
-rw-r--r--SelectOp.vp21438logstatsplain
-rw-r--r--SelectOpproof.v39914logstatsplain
-rw-r--r--Stacklayout.v5701logstatsplain
-rw-r--r--TargetPrinter.ml31467logstatsplain
-rw-r--r--ValueAOp.v13227logstatsplain
-rw-r--r--extractionMachdep.v1807logstatsplain