crucible-llvm: Support for translating and executing LLVM code in Crucible

[ bsd3, language, library ] [ Propose Tags ]

Library providing LLVM-specific extensions to the crucible core library for Crucible-based simulation and verification of LLVM-compiled applications.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.6
Change log CHANGELOG.md
Dependencies attoparsec, base (>=4.13 && <4.19), bv-sized (>=1.0.0), bytestring, containers (>=0.5.8.0), crucible (>=0.5), crucible-symio, extra, itanium-abi (>=0.1.1.1 && <0.2), lens, llvm-pretty (>=0.12 && <0.13), mtl, parameterized-utils (>=2.1.5 && <2.2), pretty, prettyprinter (>=1.7.0), template-haskell, text, transformers, utf8-string, vector, what4 (>=0.4.1) [details]
License BSD-3-Clause
Copyright (c) Galois, Inc 2014-2022
Author Galois Inc.
Maintainer rscott@galois.com, kquick@galois.com, langston@galois.com
Category Language
Source repo head: git clone https://github.com/GaloisInc/crucible(crucible-llvm)
Uploaded by ryanglscott at 2024-02-05T21:14:06Z
Distributions
Reverse Dependencies 2 direct, 0 indirect [details]
Downloads 37 total (7 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2024-02-05 [all 1 reports]

Readme for crucible-llvm-0.6

[back to package description]

This package implements an LLVM frontend for Crucible. The frontend provides two major things:

  1. A translation of LLVM IR into the Crucible IR
  2. Data types supporting that translation

Most clients of the library that just want to analyze LLVM IR (which usually means C and C++) will only need the Lang.Crucible.LLVM and Lang.Crucible.LLVM.Translation modules. The core data structure implementing the LLVM memory model (see Lang.Crucible.LLVM.MemModel) may be of interest to other clients. The memory model is documented in more detail in the docs.