LLVM M.D.ContentsIndex
LLVM M.D.

This is a research prototype of a denotational translation validator for a subset of LLVM.

Please see http://llvm-md.seas.harvard.edu for more infomation.

Modules
show/hideMD
MD.AliasingAliasing Rules.
MD.ConvertConvert basic blocks to GDSA form.
MD.DriverValidator main program.
MD.GenerateSmtTranslation of symbolic values into an SMT script.
MD.GraphData.Graph with a few extra functions.
MD.LoopDetectionSimple loop detection.
MD.MuGenerate mu-rules.
show/hideMD.ParserParser for LLVM assembly.
MD.Parser.AtomsParsers for atoms.
MD.Parser.BasicBasic parser definitions and combinators.
MD.Parser.ModuleLLVM module parser.
show/hideMD.Parser.ParsecModified Parsec library.
MD.Parser.Parsec.CharUTF8 character parsers.
MD.Parser.Parsec.CombinatorBasic parser combinators.
MD.Parser.Parsec.ErrorParser errors.
MD.Parser.Parsec.PosSource file locations.
MD.Parser.Parsec.PrimPrimitive parser combinators
MD.Parser.TypesParsers for LLVM types.
MD.PhiGenerate guarded phi-nodes.
MD.RewriteSymbolic evaluation.
MD.StructuralStructural analysis.
show/hideSyntax
MD.Syntax.EnumEnumerations.
MD.Syntax.GDSAGDSA abstract syntax.
MD.Syntax.LLVMLLVM abstract syntax.
MD.Syntax.MetaMeta-data for enumerations.
MD.Syntax.SymbolicSymbolic value abstract syntax.
Produced by Haddock version 2.6.0