aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
ModeNameSize
-rw-r--r--Archi.v2680logstatsplain
-rw-r--r--Asm.v29108logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmaux.v191logstatsplain
-rw-r--r--Asmblock.v62380logstatsplain
-rw-r--r--Asmblockdeps.v58095logstatsplain
-rw-r--r--Asmblockgen.v39728logstatsplain
-rw-r--r--Asmblockgenproof.v88316logstatsplain
-rw-r--r--Asmblockgenproof1.v84768logstatsplain
-rw-r--r--Asmexpand.ml20478logstatsplain
-rw-r--r--Asmgen.v2139logstatsplain
-rw-r--r--Asmgenproof.v7659logstatsplain
-rw-r--r--CBuiltins.ml7400logstatsplain
-rw-r--r--CombineOp.v4700logstatsplain
-rw-r--r--CombineOpproof.v6792logstatsplain
-rw-r--r--ConstpropOp.v34970logstatsplain
-rw-r--r--ConstpropOp.vp12735logstatsplain
-rw-r--r--ConstpropOpproof.v29940logstatsplain
-rw-r--r--Conventions1.v15661logstatsplain
-rw-r--r--InstructionScheduler.ml39104logstatsplain
-rw-r--r--InstructionScheduler.mli4659logstatsplain
-rw-r--r--Machblock.v12815logstatsplain
-rw-r--r--Machblockgen.v18614logstatsplain
-rw-r--r--Machblockgenproof.v24425logstatsplain
-rw-r--r--Machregs.v9447logstatsplain
-rw-r--r--Machregsaux.ml1369logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v8018logstatsplain
-rw-r--r--Op.v60752logstatsplain
-rw-r--r--PostpassScheduling.v15897logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml30270logstatsplain
-rw-r--r--PostpassSchedulingproof.v24132logstatsplain
-rw-r--r--PrintOp.ml8958logstatsplain
-rw-r--r--SelectLong.vp13388logstatsplain
-rw-r--r--SelectLongproof.v26994logstatsplain
-rw-r--r--SelectOp.v49310logstatsplain
-rw-r--r--SelectOp.vp17560logstatsplain
-rw-r--r--SelectOpproof.v35080logstatsplain
-rw-r--r--Stacklayout.v6178logstatsplain
-rw-r--r--TargetPrinter.ml23208logstatsplain
-rw-r--r--ValueAOp.v9378logstatsplain
d---------abstractbb430logstatsplain
-rw-r--r--extractionMachdep.v1426logstatsplain
d---------lib99logstatsplain
d---------unittest80logstatsplain
generated by cgit (git 2.34.1) at 2024-07-06 15:06:10 +0000