aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
ModeNameSize
-rw-r--r--Archi.v2308logstatsplain
-rw-r--r--Asm.v60454logstatsplain
-rw-r--r--AsmToJSON.ml22250logstatsplain
-rw-r--r--AsmToJSON.mli899logstatsplain
-rw-r--r--Asmexpand.ml32519logstatsplain
-rw-r--r--Asmgen.v34479logstatsplain
-rw-r--r--Asmgenproof.v37725logstatsplain
-rw-r--r--Asmgenproof1.v68308logstatsplain
-rw-r--r--CBuiltins.ml6350logstatsplain
-rw-r--r--CombineOp.v4747logstatsplain
-rw-r--r--CombineOpproof.v7063logstatsplain
-rw-r--r--ConstpropOp.vp9444logstatsplain
-rw-r--r--ConstpropOpproof.v21751logstatsplain
-rw-r--r--Conventions1.v18293logstatsplain
-rw-r--r--Machregs.v10697logstatsplain
-rw-r--r--Machregsaux.ml1453logstatsplain
-rw-r--r--Machregsaux.mli1058logstatsplain
-rw-r--r--NeedOp.v5810logstatsplain
-rw-r--r--Op.v51641logstatsplain
-rw-r--r--PrintOp.ml7774logstatsplain
-rw-r--r--SelectLong.vp12397logstatsplain
-rw-r--r--SelectLongproof.v27364logstatsplain
-rw-r--r--SelectOp.vp20241logstatsplain
-rw-r--r--SelectOpproof.v38721logstatsplain
-rw-r--r--Stacklayout.v5644logstatsplain
-rw-r--r--TargetPrinter.ml39627logstatsplain
-rw-r--r--ValueAOp.v8036logstatsplain
-rw-r--r--extractionMachdep.v1665logstatsplain