linearscan-1.0.0: Linear scan register allocator, formally verified in Coq

Index

allocateLinearScan
applyAllocsLinearScan
blockIdLinearScan
BlockInfo 
1 (Type/Class)LinearScan
2 (Data Constructor)LinearScan
blockOpsLinearScan
blockSuccessorsLinearScan
InputLinearScan
InputOutputLinearScan
IsBranchLinearScan
IsCallLinearScan
IsNormalLinearScan
moveOpLinearScan
OpInfo 
1 (Type/Class)LinearScan
2 (Data Constructor)LinearScan
OpKindLinearScan
opKindLinearScan
opRefsLinearScan
OutputLinearScan
PhysRegLinearScan
regRequiredLinearScan
restoreOpLinearScan
saveOpLinearScan
setBlockOpsLinearScan
showOp1LinearScan
splitCriticalEdgeLinearScan
TempLinearScan
UseVerifierLinearScan
VarIdLinearScan
varIdLinearScan
VarInfo 
1 (Type/Class)LinearScan
2 (Data Constructor)LinearScan
VarKindLinearScan
varKindLinearScan
VerifyDisabledLinearScan
VerifyEnabledLinearScan
VerifyEnabledStrictLinearScan