aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
ModeNameSize
-rw-r--r--Archi.v2616logstatsplain
-rw-r--r--Asm.v61631logstatsplain
-rw-r--r--AsmToJSON.ml21794logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml37492logstatsplain
-rw-r--r--Asmgen.v36056logstatsplain
-rw-r--r--Asmgenproof.v38902logstatsplain
-rw-r--r--Asmgenproof1.v74523logstatsplain
-rw-r--r--Builtins1.v1556logstatsplain
-rw-r--r--CBuiltins.ml6973logstatsplain
-rw-r--r--CombineOp.v4747logstatsplain
-rw-r--r--CombineOpproof.v7086logstatsplain
-rw-r--r--ConstpropOp.vp14699logstatsplain
-rw-r--r--ConstpropOpproof.v33919logstatsplain
-rw-r--r--Conventions1.v18306logstatsplain
-rw-r--r--Machregs.v10626logstatsplain
-rw-r--r--Machregsaux.ml1637logstatsplain
-rw-r--r--Machregsaux.mli1093logstatsplain
-rw-r--r--NeedOp.v6010logstatsplain
-rw-r--r--Op.v53440logstatsplain
-rw-r--r--PrintOp.ml7933logstatsplain
-rw-r--r--SelectLong.vp12407logstatsplain
-rw-r--r--SelectLongproof.v26470logstatsplain
-rw-r--r--SelectOp.vp21053logstatsplain
-rw-r--r--SelectOpproof.v40418logstatsplain
-rw-r--r--Stacklayout.v5648logstatsplain
-rw-r--r--TargetPrinter.ml39113logstatsplain
-rw-r--r--ValueAOp.v8178logstatsplain
-rw-r--r--extractionMachdep.v1887logstatsplain