aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
ModeNameSize
-rw-r--r--Archi.v2879logstatsplain
-rw-r--r--Asm.v61015logstatsplain
-rw-r--r--AsmToJSON.ml21727logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml36701logstatsplain
-rw-r--r--Asmgen.v38232logstatsplain
-rw-r--r--Asmgenproof.v39847logstatsplain
-rw-r--r--Asmgenproof1.v78351logstatsplain
l---------BTL_SEsimplify.v27logstatsplain
-rw-r--r--Builtins1.v3244logstatsplain
-rw-r--r--CBuiltins.ml6603logstatsplain
-rw-r--r--CSE2deps.v1620logstatsplain
-rw-r--r--CSE2depsproof.v7431logstatsplain
-rw-r--r--CombineOp.v4747logstatsplain
-rw-r--r--CombineOpproof.v7086logstatsplain
-rw-r--r--ConstpropOp.vp14699logstatsplain
-rw-r--r--ConstpropOpproof.v33917logstatsplain
-rw-r--r--Conventions1.v14263logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1586logstatsplain
l---------ExpansionOracle.ml29logstatsplain
-rw-r--r--Machregs.v10624logstatsplain
-rw-r--r--Machregsaux.ml1097logstatsplain
-rw-r--r--Machregsaux.mli939logstatsplain
-rw-r--r--NeedOp.v5962logstatsplain
-rw-r--r--Op.v56173logstatsplain
l---------PrepassSchedulingOracle.ml33logstatsplain
-rw-r--r--PrintOp.ml8343logstatsplain
-rw-r--r--SelectLong.vp12407logstatsplain
-rw-r--r--SelectLongproof.v26464logstatsplain
-rw-r--r--SelectOp.vp21154logstatsplain
-rw-r--r--SelectOpproof.v40833logstatsplain
-rw-r--r--Stacklayout.v5608logstatsplain
-rw-r--r--TargetPrinter.ml39081logstatsplain
-rw-r--r--ValueAOp.v8048logstatsplain
-rw-r--r--extractionMachdep.v2142logstatsplain