aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
ModeNameSize
-rw-r--r--Archi.v3101logstatsplain
-rw-r--r--Asm.v57066logstatsplain
-rw-r--r--AsmToJSON.ml1024logstatsplain
-rw-r--r--Asmblock.v68752logstatsplain
-rw-r--r--Asmblockdeps.v105956logstatsplain
-rw-r--r--Asmblockgen.v51161logstatsplain
-rw-r--r--Asmblockgenproof.v43099logstatsplain
-rw-r--r--Asmblockgenproof0.v31449logstatsplain
-rw-r--r--Asmblockgenproof1.v84630logstatsplain
-rw-r--r--Asmblockprops.v14533logstatsplain
-rw-r--r--Asmexpand.ml16522logstatsplain
-rw-r--r--Asmgen.v19849logstatsplain
-rw-r--r--Asmgenproof.v89829logstatsplain
-rw-r--r--Asmgenproof_orig_single_label_in_header.v.stash84218logstatsplain
-rw-r--r--Builtins1.v1551logstatsplain
-rw-r--r--CBuiltins.ml2717logstatsplain
-rw-r--r--CSE2deps.v1487logstatsplain
-rw-r--r--CSE2depsproof.v4729logstatsplain
-rw-r--r--CombineOp.v4511logstatsplain
-rw-r--r--CombineOpproof.v6424logstatsplain
-rw-r--r--ConstpropOp.vp18272logstatsplain
-rw-r--r--ConstpropOpproof.v34910logstatsplain
-rw-r--r--Conventions1.v11070logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1595logstatsplain
-rw-r--r--InstructionScheduler.ml43158logstatsplain
-rw-r--r--InstructionScheduler.mli4925logstatsplain
-rw-r--r--Machregs.v7790logstatsplain
-rw-r--r--Machregsaux.ml1581logstatsplain
-rw-r--r--NeedOp.v9857logstatsplain
-rw-r--r--Op.v78338logstatsplain
-rw-r--r--OpWeightsAsm.ml9532logstatsplain
-rw-r--r--OrigAsmgen.ml9409logstatsplain
-rw-r--r--PostpassScheduling.v17701logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml25765logstatsplain
-rw-r--r--PostpassSchedulingproof.v24077logstatsplain
-rw-r--r--PrintOp.ml13911logstatsplain
-rw-r--r--SelectLong.vp18098logstatsplain
-rw-r--r--SelectLongproof.v30092logstatsplain
-rw-r--r--SelectOp.vp21127logstatsplain
-rw-r--r--SelectOpproof.v39315logstatsplain
-rw-r--r--Stacklayout.v5751logstatsplain
-rw-r--r--TargetPrinter.ml27141logstatsplain
-rw-r--r--ValueAOp.v13155logstatsplain
-rw-r--r--extractionMachdep.v1211logstatsplain