aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
ModeNameSize
-rw-r--r--Archi.v2678logstatsplain
-rw-r--r--Asm.v49144logstatsplain
-rw-r--r--AsmToJSON.ml945logstatsplain
-rw-r--r--Asmexpand.ml22073logstatsplain
-rw-r--r--Asmgen.v35770logstatsplain
-rw-r--r--Asmgenproof.v39969logstatsplain
-rw-r--r--Asmgenproof1.v61240logstatsplain
-rw-r--r--CBuiltins.ml2766logstatsplain
-rw-r--r--CombineOp.v4700logstatsplain
-rw-r--r--CombineOpproof.v6769logstatsplain
-rw-r--r--ConstpropOp.vp12099logstatsplain
-rw-r--r--ConstpropOpproof.v28506logstatsplain
-rw-r--r--Conventions1.v16295logstatsplain
-rw-r--r--Machregs.v9818logstatsplain
-rw-r--r--Machregsaux.ml1369logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v6396logstatsplain
-rw-r--r--Op.v54136logstatsplain
-rw-r--r--PrintOp.ml8958logstatsplain
-rw-r--r--SelectLong.vp13031logstatsplain
-rw-r--r--SelectLongproof.v26685logstatsplain
-rw-r--r--SelectOp.vp16134logstatsplain
-rw-r--r--SelectOpproof.v33631logstatsplain
-rw-r--r--Stacklayout.v6175logstatsplain
-rw-r--r--TargetPrinter.ml29259logstatsplain
-rw-r--r--ValueAOp.v8252logstatsplain
-rw-r--r--extractionMachdep.v1198logstatsplain
generated by cgit (git 2.34.1) at 2024-06-02 23:35:21 +0000