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

Duplication: equalValsPred and Crucible's Value.testEqual #439

Closed
langston-barrett opened this issue May 16, 2019 · 1 comment
Closed

Duplication: equalValsPred and Crucible's Value.testEqual #439

langston-barrett opened this issue May 16, 2019 · 1 comment
Assignees
@robdockins
Labels
crucible/llvm Related to crucible-llvm verification tech-debt
Milestone
0.7

Comments

@langston-barrett
Copy link
Contributor

This one is my fault :) These two functions are notably similar:
Crucible.LLVM.MemModel.Value.testEqual

testEqual :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)
          => sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))

SAWScript.CrucibleResolveSetupValue.equalValsPred

equalValsPred ::
  CrucibleContext wptr ->
  LLVMVal ->
  LLVMVal ->
  IO (W4.Pred Sym)

We should probably rephrase the latter so that it uses the former, which is more complete.
@langston-barrett langston-barrett added the crucible/llvm Related to crucible-llvm verification label Jun 7, 2019
@robdockins robdockins self-assigned this Oct 5, 2020
@robdockins robdockins added this to the 0.7 milestone Oct 16, 2020
@robdockins
Copy link
Contributor

This was fixed via 9c6d6ab

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robdockins robdockins

Labels
crucible/llvm Related to crucible-llvm verification tech-debt
Projects
None yet
Milestone
0.7
Development

No branches or pull requests
3 participants
@brianhuffman @langston-barrett @robdockins