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

Pretty printer for CFG.Expr doesn't show argument to withAssertion #337

Closed
brianhuffman opened this issue Nov 12, 2019 · 0 comments · Fixed by #339
Closed

Pretty printer for CFG.Expr doesn't show argument to withAssertion #337

brianhuffman opened this issue Nov 12, 2019 · 0 comments · Fixed by #339

Comments

@brianhuffman
Copy link
Contributor

When pretty printing a Crucible CFG (as when using show_cfg in saw-script) the withAssertion expressions are printed with <some assertion> in place of the argument, like this:

  % 28:12
  $17 = withAssertion(BVRepr 64, <some assertion>)

This is not very useful when trying to inspect a CFG.

The problem is in the PrettyApp (App ext) instance in module Lang.Crucible.CFG.Expr:

crucible/crucible/src/Lang/Crucible/CFG/Expr.hs

Lines 1287 to 1291 in 6fdb562

, ( U.ConType [t|PartialExpr|] `U.TypeApp` U.AnyType
`U.TypeApp` U.AnyType
`U.TypeApp` U.AnyType
, [| \_ _ -> text "<some assertion>" |]
)

Instead of \_ _ -> text "<some assertion>" it should contain something like \pp pe -> pp (pe ^. value), so that at least it would show the value part of the PartialExpr inside the WithAssertion constructor.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Update CFG.Expr pretty printer to show partial expressions. GaloisInc/crucible
1 participant
@brianhuffman