aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
ModeNameSize
-rw-r--r--Archi.v3319logstatsplain
-rw-r--r--Asm.v59878logstatsplain
-rw-r--r--AsmToJSON.ml1024logstatsplain
-rw-r--r--Asmblock.v40907logstatsplain
-rw-r--r--Asmblockdeps.v103245logstatsplain
-rw-r--r--Asmblockgen.v49704logstatsplain
-rw-r--r--Asmblockgenproof.v61700logstatsplain
-rw-r--r--Asmblockgenproof0.v28425logstatsplain
-rw-r--r--Asmblockgenproof1.v82650logstatsplain
-rw-r--r--Asmblockprops.v3946logstatsplain
-rw-r--r--Asmexpand.ml17166logstatsplain
-rw-r--r--Asmgen.v24470logstatsplain
-rw-r--r--Asmgenproof.v87095logstatsplain
-rw-r--r--Builtins1.v1551logstatsplain
-rw-r--r--CBuiltins.ml2631logstatsplain
-rw-r--r--CSE2deps.v1624logstatsplain
-rw-r--r--CSE2depsproof.v7126logstatsplain
-rw-r--r--CombineOp.v4511logstatsplain
-rw-r--r--CombineOpproof.v6424logstatsplain
-rw-r--r--ConstpropOp.vp18272logstatsplain
-rw-r--r--ConstpropOpproof.v36024logstatsplain
-rw-r--r--Conventions1.v11070logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1595logstatsplain
-rw-r--r--ExpansionOracle.ml830logstatsplain
-rw-r--r--Machregs.v7790logstatsplain
-rw-r--r--Machregsaux.ml1082logstatsplain
-rw-r--r--NeedOp.v9857logstatsplain
-rw-r--r--Op.v78281logstatsplain
-rw-r--r--OpWeights.ml14383logstatsplain
-rw-r--r--OpWeightsAsm.ml7251logstatsplain
-rw-r--r--PeepholeOracle.ml25709logstatsplain
-rw-r--r--PostpassScheduling.v5075logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml19622logstatsplain
-rw-r--r--PostpassSchedulingproof.v15907logstatsplain
-rw-r--r--PrepassSchedulingOracle.ml16532logstatsplain
-rw-r--r--PrepassSchedulingOracleDeps.ml871logstatsplain
-rw-r--r--PrintOp.ml13911logstatsplain
-rw-r--r--RTLpathSE_simplify.v1620logstatsplain
-rw-r--r--SelectLong.vp18098logstatsplain
-rw-r--r--SelectLongproof.v30461logstatsplain
-rw-r--r--SelectOp.vp21127logstatsplain
-rw-r--r--SelectOpproof.v39698logstatsplain
-rw-r--r--Stacklayout.v5751logstatsplain
-rw-r--r--TargetPrinter.ml27454logstatsplain
-rw-r--r--ValueAOp.v13227logstatsplain
-rw-r--r--extractionMachdep.v1433logstatsplain