aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
ModeNameSize
-rw-r--r--Archi.v2680logstatsplain
-rw-r--r--Asm.v36897logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmaux.v191logstatsplain
-rw-r--r--Asmblock.v13328logstatsplain
-rw-r--r--Asmblockdeps.v60781logstatsplain
-rw-r--r--Asmblockgen.v45160logstatsplain
-rw-r--r--Asmblockgenproof.v74501logstatsplain
-rw-r--r--Asmblockgenproof0.v36322logstatsplain
-rw-r--r--Asmblockgenproof1.v111504logstatsplain
-rw-r--r--Asmexpand.ml23835logstatsplain
-rw-r--r--Asmgen.v2035logstatsplain
-rw-r--r--Asmgenproof.v3725logstatsplain
-rw-r--r--Asmvliw.v67567logstatsplain
-rw-r--r--CBuiltins.ml8035logstatsplain
-rw-r--r--Chunks.v505logstatsplain
-rw-r--r--CombineOp.v4700logstatsplain
-rw-r--r--CombineOpproof.v6792logstatsplain
-rw-r--r--ConstpropOp.vp12784logstatsplain
-rw-r--r--ConstpropOpproof.v29930logstatsplain
-rw-r--r--Conventions1.v15643logstatsplain
-rw-r--r--DecBoolOps.v297logstatsplain
-rw-r--r--ExtValues.v18614logstatsplain
-rw-r--r--InstructionScheduler.ml40971logstatsplain
-rw-r--r--InstructionScheduler.mli4793logstatsplain
-rw-r--r--Machregs.v9992logstatsplain
-rw-r--r--Machregsaux.ml1503logstatsplain
-rw-r--r--Machregsaux.mli1093logstatsplain
-rw-r--r--NeedOp.v18605logstatsplain
-rw-r--r--Op.v77834logstatsplain
-rw-r--r--Peephole.v5485logstatsplain
-rw-r--r--PostpassScheduling.v16133logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml34457logstatsplain
-rw-r--r--PostpassSchedulingproof.v33476logstatsplain
-rw-r--r--PrintOp.ml8897logstatsplain
-rw-r--r--SelectLong.vp18308logstatsplain
-rw-r--r--SelectLongproof.v42111logstatsplain
-rw-r--r--SelectOp.vp24804logstatsplain
-rw-r--r--SelectOpproof.v53450logstatsplain
-rw-r--r--Stacklayout.v6178logstatsplain
-rw-r--r--TargetPrinter.ml31585logstatsplain
-rw-r--r--ValueAOp.v19339logstatsplain
d---------abstractbb248logstatsplain
-rwxr-xr-xbitmasks.py314logstatsplain
-rw-r--r--extractionMachdep.v1570logstatsplain
d---------lib180logstatsplain
d---------unittest80logstatsplain