aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
ModeNameSize
-rw-r--r--Archi.v2863logstatsplain
-rw-r--r--Asm.v49526logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmexpand.ml22064logstatsplain
-rw-r--r--Asmgen.v36486logstatsplain
-rw-r--r--Asmgenproof.v40365logstatsplain
-rw-r--r--Asmgenproof1.v61227logstatsplain
-rw-r--r--Builtins1.v1551logstatsplain
-rw-r--r--CBuiltins.ml2337logstatsplain
-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.v30000logstatsplain
-rw-r--r--Conventions1.v15745logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1613logstatsplain
-rw-r--r--Machregs.v9823logstatsplain
-rw-r--r--Machregsaux.ml1553logstatsplain
-rw-r--r--Machregsaux.mli1093logstatsplain
-rw-r--r--NeedOp.v6396logstatsplain
-rw-r--r--Op.v56687logstatsplain
-rw-r--r--PrintOp.ml8958logstatsplain
-rw-r--r--SelectLong.vp13041logstatsplain
-rw-r--r--SelectLongproof.v26726logstatsplain
-rw-r--r--SelectOp.vp16535logstatsplain
-rw-r--r--SelectOpproof.v34947logstatsplain
-rw-r--r--Stacklayout.v6178logstatsplain
-rw-r--r--TargetPrinter.ml28074logstatsplain
-rw-r--r--ValueAOp.v8252logstatsplain
-rw-r--r--extractionMachdep.v1420logstatsplain