aboutsummaryrefslogtreecommitdiffstats
path: root/arm
ModeNameSize
-rw-r--r--Archi.v3619logstatsplain
-rw-r--r--Asm.v42306logstatsplain
-rw-r--r--AsmToJSON.ml16279logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml22927logstatsplain
-rw-r--r--Asmgen.v30354logstatsplain
-rw-r--r--Asmgenproof.v37603logstatsplain
-rw-r--r--Asmgenproof1.v62443logstatsplain
-rw-r--r--Builtins1.v1551logstatsplain
-rw-r--r--CBuiltins.ml2487logstatsplain
-rw-r--r--CombineOp.v4223logstatsplain
-rw-r--r--CombineOpproof.v6429logstatsplain
-rw-r--r--Constantexpand.ml5870logstatsplain
-rw-r--r--ConstpropOp.vp13557logstatsplain
-rw-r--r--ConstpropOpproof.v28805logstatsplain
-rw-r--r--Conventions1.v17154logstatsplain
-rw-r--r--Machregs.v7121logstatsplain
-rw-r--r--Machregsaux.ml1298logstatsplain
-rw-r--r--Machregsaux.mli1010logstatsplain
-rw-r--r--NeedOp.v7507logstatsplain
-rw-r--r--Op.v46716logstatsplain
-rw-r--r--PrintOp.ml7314logstatsplain
-rw-r--r--SelectLong.vp1117logstatsplain
-rw-r--r--SelectLongproof.v1221logstatsplain
-rw-r--r--SelectOp.vp19114logstatsplain
-rw-r--r--SelectOpproof.v32750logstatsplain
-rw-r--r--Stacklayout.v5435logstatsplain
-rw-r--r--TargetPrinter.ml23457logstatsplain
-rw-r--r--ValueAOp.v7989logstatsplain
-rw-r--r--extractionMachdep.v1843logstatsplain