aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
ModeNameSize
-rw-r--r--Archi.v2933logstatsplain
-rw-r--r--Asm.v50442logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmexpand.ml29162logstatsplain
-rw-r--r--Asmgen.v45986logstatsplain
-rw-r--r--Asmgenproof.v41807logstatsplain
-rw-r--r--Asmgenproof1.v70960logstatsplain
-rw-r--r--BTL_SEsimplify.v74373logstatsplain
-rw-r--r--Builtins1.v2480logstatsplain
-rw-r--r--CBuiltins.ml2757logstatsplain
-rw-r--r--CSE2deps.v1626logstatsplain
-rw-r--r--CSE2depsproof.v5020logstatsplain
-rw-r--r--CombineOp.v4700logstatsplain
-rw-r--r--CombineOpproof.v6792logstatsplain
-rw-r--r--ConstpropOp.vp12735logstatsplain
-rw-r--r--ConstpropOpproof.v31453logstatsplain
-rw-r--r--Conventions1.v17158logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1613logstatsplain
-rw-r--r--ExpansionOracle.ml37930logstatsplain
-rw-r--r--ExtValues.v2943logstatsplain
-rw-r--r--Machregs.v10849logstatsplain
-rw-r--r--Machregsaux.ml1109logstatsplain
-rw-r--r--Machregsaux.mli1006logstatsplain
-rw-r--r--NeedOp.v8403logstatsplain
-rw-r--r--Op.v87765logstatsplain
-rw-r--r--OpWeights.ml12429logstatsplain
l---------PrepassSchedulingOracle.ml37logstatsplain
l---------PrepassSchedulingOracleDeps.ml41logstatsplain
-rw-r--r--PrintOp.ml14516logstatsplain
-rw-r--r--SelectLong.vp13041logstatsplain
-rw-r--r--SelectLongproof.v25672logstatsplain
-rw-r--r--SelectOp.vp17911logstatsplain
-rw-r--r--SelectOpproof.v37771logstatsplain
-rw-r--r--Stacklayout.v6122logstatsplain
-rw-r--r--TargetPrinter.ml28272logstatsplain
-rw-r--r--ValueAOp.v20146logstatsplain
-rw-r--r--extractionMachdep.v1494logstatsplain
generated by cgit (git 2.34.1) at 2024-04-27 10:18:07 +0000