aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
ModeNameSize
-rw-r--r--Archi.v2927logstatsplain
-rw-r--r--Asm.v37969logstatsplain
-rw-r--r--AsmToJSON.ml1028logstatsplain
-rw-r--r--Asmaux.v1051logstatsplain
-rw-r--r--Asmblock.v13444logstatsplain
-rw-r--r--Asmblockdeps.v68274logstatsplain
-rw-r--r--Asmblockgen.v45925logstatsplain
-rw-r--r--Asmblockgenproof.v74465logstatsplain
-rw-r--r--Asmblockgenproof1.v104316logstatsplain
-rw-r--r--Asmblockprops.v14448logstatsplain
-rw-r--r--Asmexpand.ml24557logstatsplain
-rw-r--r--Asmgen.v2028logstatsplain
-rw-r--r--Asmgenproof.v3920logstatsplain
-rw-r--r--Asmvliw.v67423logstatsplain
-rw-r--r--Builtins1.v2475logstatsplain
-rw-r--r--CBuiltins.ml8506logstatsplain
-rw-r--r--CSE2deps.v1626logstatsplain
-rw-r--r--CSE2depsproof.v5049logstatsplain
-rw-r--r--Chunks.v1365logstatsplain
-rw-r--r--CombineOp.v4811logstatsplain
-rw-r--r--CombineOpproof.v6839logstatsplain
-rw-r--r--ConstpropOp.vp12895logstatsplain
-rw-r--r--ConstpropOpproof.v29866logstatsplain
-rw-r--r--Conventions1.v15589logstatsplain
-rw-r--r--DecBoolOps.v1224logstatsplain
-rw-r--r--DuplicateOpcodeHeuristic.ml1613logstatsplain
-rw-r--r--ExtFloats.v1860logstatsplain
-rw-r--r--ExtValues.v21243logstatsplain
-rw-r--r--Machregs.v9812logstatsplain
-rw-r--r--Machregsaux.ml1364logstatsplain
-rw-r--r--Machregsaux.mli939logstatsplain
-rw-r--r--NeedOp.v14159logstatsplain
-rw-r--r--Op.v75154logstatsplain
-rw-r--r--OpWeights.ml3858logstatsplain
-rw-r--r--Peephole.v6415logstatsplain
-rw-r--r--PostpassScheduling.v17857logstatsplain
-rw-r--r--PostpassSchedulingOracle.ml39847logstatsplain
-rw-r--r--PostpassSchedulingproof.v24071logstatsplain
l---------PrepassSchedulingOracle.ml37logstatsplain
l---------PrepassSchedulingOracleDeps.ml41logstatsplain
-rw-r--r--PrintOp.ml13210logstatsplain
-rw-r--r--SelectLong.vp17259logstatsplain
-rw-r--r--SelectLongproof.v38548logstatsplain
-rw-r--r--SelectOp.vp25772logstatsplain
-rw-r--r--SelectOpproof.v58927logstatsplain
-rw-r--r--Stacklayout.v6283logstatsplain
-rw-r--r--TargetPrinter.ml36352logstatsplain
-rw-r--r--ValueAOp.v21657logstatsplain
d---------abstractbb220logstatsplain
-rwxr-xr-xbitmasks.py314logstatsplain
-rw-r--r--extractionMachdep.v1459logstatsplain
d---------lib227logstatsplain
d---------unittest80logstatsplain