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

[ bsd3, language, library ] [ Propose Tags ] [ Report a vulnerability ]

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

[Skip to Readme]

Modules

[Index] [Quick Jump]

Lang
- Crucible
  - Lang.Crucible.LLVM

Downloads

crucible-llvm-0.7.tar.gz [browse] (Cabal source package)
Package description (revised from the package)

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

ryanglscott, galoisinc, mccleeary

For package maintainers and hackage trustees

edit package information

Candidates

No Candidates

Versions [RSS]	0.6, 0.7
Change log	CHANGELOG.md
Dependencies	attoparsec, base (>=4.13 && <4.20), 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.1 && <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
Revised	Revision 1 made by ryanglscott at 2024-09-03T16:55:33Z
Category	Language
Source repo	head: git clone https://github.com/GaloisInc/crucible(crucible-llvm)
Uploaded	by mccleeary at 2024-08-30T20:08:39Z
Distributions
Reverse Dependencies	2 direct, 0 indirect [details]
Downloads	122 total (14 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-09-06 [all 3 reports]

Readme for crucible-llvm-0.7

[back to package description]

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

A translation of LLVM IR into the Crucible IR
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.