Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[WIP] LLVM term annotations #453

Merged
merged 10 commits into from
Apr 2, 2020
Merged

[WIP] LLVM term annotations #453

merged 10 commits into from
Apr 2, 2020

Commits on Mar 26, 2020

  1. Update various .cabal files to upgrade certain warnings to errors. 

    These are: incomplete-patterns, overlapping-patterns, and missing-methods.
    @robdockins @andreistefanescu
    robdockins authored and andreistefanescu committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    56f883c View commit details
    Browse the repository at this point in the history

  2. Remove the use of the WithAssertion expression from crucible-jvm 

    Remove the use of the `WithAssertions` expression former in crucible-llvm.
Instead, a language-extension expression former `LLVM_SideConditions` has
been added that directly references the `LLVM_SafetyCondition` type.

Remove the `WithAssertions` syntax constructor and related
typeclass constraints.
    @robdockins @andreistefanescu
    robdockins authored and andreistefanescu committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    5bb779b View commit details
    Browse the repository at this point in the history

  3. Replace uses of AssertionTree with term annotations in the LLVM memor… 

    …y model.
    @robdockins @andreistefanescu
    robdockins authored and andreistefanescu committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    5c9b3e3 View commit details
    Browse the repository at this point in the history

  4. Remove the AssertionTree datatype, and crucible safety extension 

    mechanism, and the `HasStructuredAssertions` typeclass.

These ideas are largely being replace with term annotations.
    @robdockins @andreistefanescu
    robdockins authored and andreistefanescu committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    c606bc2 View commit details
    Browse the repository at this point in the history

  5. Export PartLLVMVal constructors.

    @andreistefanescu
    andreistefanescu committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    5527658 View commit details
    Browse the repository at this point in the history

  6. Fix evaluateExpr for Annotation.

    @andreistefanescu
    andreistefanescu committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    729d3ec View commit details
    Browse the repository at this point in the history

Commits on Mar 30, 2020

  1. Cleanup.

    @andreistefanescu
    andreistefanescu committed Mar 30, 2020
    Configuration menu
    Copy the full SHA
    98f7e45 View commit details
    Browse the repository at this point in the history

  2. Simplify muxLLVMVal.

    @andreistefanescu
    andreistefanescu committed Mar 30, 2020
    Configuration menu
    Copy the full SHA
    0622138 View commit details
    Browse the repository at this point in the history

Commits on Mar 31, 2020

  1. Comments regarding muxLLVMVal

    @robdockins
    robdockins committed Mar 31, 2020
    Configuration menu
    Copy the full SHA
    c0d241c View commit details
    Browse the repository at this point in the history

  2. Fix crucible-syntax test suite

    @robdockins
    robdockins committed Mar 31, 2020
    Configuration menu
    Copy the full SHA
    41e5c78 View commit details
    Browse the repository at this point in the history