aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
ModeNameSize
-rw-r--r--Archi.v2766logstatsplain
-rw-r--r--Asm.v60965logstatsplain
-rw-r--r--AsmToJSON.ml21704logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml36934logstatsplain
-rw-r--r--Asmgen.v35737logstatsplain
-rw-r--r--Asmgenproof.v38989logstatsplain
-rw-r--r--Asmgenproof1.v74116logstatsplain
-rw-r--r--Builtins1.v2863logstatsplain
-rw-r--r--CBuiltins.ml6529logstatsplain
-rw-r--r--CombineOp.v4747logstatsplain
-rw-r--r--CombineOpproof.v7086logstatsplain
-rw-r--r--ConstpropOp.vp14699logstatsplain
-rw-r--r--ConstpropOpproof.v33917logstatsplain
-rw-r--r--Conventions1.v14177logstatsplain
-rw-r--r--Machregs.v10610logstatsplain
-rw-r--r--Machregsaux.ml913logstatsplain
-rw-r--r--Machregsaux.mli904logstatsplain
-rw-r--r--NeedOp.v5962logstatsplain
-rw-r--r--Op.v52524logstatsplain
-rw-r--r--PrintOp.ml8343logstatsplain
-rw-r--r--SelectLong.vp12397logstatsplain
-rw-r--r--SelectLongproof.v26423logstatsplain
-rw-r--r--SelectOp.vp20962logstatsplain
-rw-r--r--SelectOpproof.v40099logstatsplain
-rw-r--r--Stacklayout.v5608logstatsplain
-rw-r--r--TargetPrinter.ml38967logstatsplain
-rw-r--r--ValueAOp.v8048logstatsplain
-rw-r--r--extractionMachdep.v2003logstatsplain