aboutsummaryrefslogtreecommitdiffstats
path: root/x86
ModeNameSize
-rw-r--r--Asm.v42946logstatsplain
-rw-r--r--AsmToJSON.ml1026logstatsplain
-rw-r--r--AsmToJSON.mli1006logstatsplain
-rw-r--r--Asmexpand.ml24162logstatsplain
-rw-r--r--Asmgen.v30557logstatsplain
-rw-r--r--Asmgenproof.v35375logstatsplain
-rw-r--r--Asmgenproof1.v63862logstatsplain
l---------BTL_SEsimplify.v27logstatsplain
-rw-r--r--Builtins1.v2267logstatsplain
-rw-r--r--CBuiltins.ml3016logstatsplain
-rw-r--r--CSE2deps.v1780logstatsplain
-rw-r--r--CSE2depsproof.v11854logstatsplain
-rw-r--r--CombineOp.v5047logstatsplain
-rw-r--r--CombineOpproof.v7102logstatsplain
-rw-r--r--ConstpropOp.vp18826logstatsplain
-rw-r--r--ConstpropOpproof.v40635logstatsplain
-rw-r--r--Conventions1.v18453logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1613logstatsplain
l---------ExpansionOracle.ml29logstatsplain
-rw-r--r--Machregs.v12059logstatsplain
-rw-r--r--Machregsaux.ml1082logstatsplain
-rw-r--r--Machregsaux.mli939logstatsplain
-rw-r--r--NeedOp.v9355logstatsplain
-rw-r--r--Op.v67325logstatsplain
-rw-r--r--PrepassSchedulingOracle.ml146logstatsplain
-rw-r--r--PrintOp.ml9471logstatsplain
-rw-r--r--SelectLong.vp13074logstatsplain
-rw-r--r--SelectLongproof.v24444logstatsplain
-rw-r--r--SelectOp.vp21189logstatsplain
-rw-r--r--SelectOpproof.v39381logstatsplain
-rw-r--r--Stacklayout.v6668logstatsplain
-rw-r--r--TargetPrinter.ml38889logstatsplain
-rw-r--r--ValueAOp.v11379logstatsplain
-rw-r--r--extractionMachdep.v1563logstatsplain
generated by cgit (git 2.34.1) at 2024-04-27 09:44:09 +0000