Add --print-internal-representation to goto-instrument #991
Conversation
This flag pretty-prints every instruction in the entire program. I use it to learn about CPROVER's internal representation of particular constructs, by passing in --print-internal-representation on a one-line C program. CR: https://cr.amazon.com/r/7203184/
| " --check-invariant function instruments invariant checking function\n" | ||
| " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) | ||
| " --undefined-function-is-assume-false\n" | ||
| // NOLINTNEXTLINE(whitespace/line_length) |
There was a problem hiding this comment.
Please could you remove the line break introduced here.
There was a problem hiding this comment.
Thanks Martin. Not sure what you mean, I didn't introduce a line break, but just added two linter directives since the linter was complaining...
|
Thanks for this patch. It seems the key difference between this and --show-goto-functions is the use of pretty() for displaying the irepts. Is their a sane way that this functionality could be folded into --show-goto-functions (or maybe --show-symbol-table)? |
karkhaz
left a comment
karkhaz
left a comment
There was a problem hiding this comment.
Sure, good idea. I'll do that, please clarify about the line break.
| " --check-invariant function instruments invariant checking function\n" | ||
| " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) | ||
| " --undefined-function-is-assume-false\n" | ||
| // NOLINTNEXTLINE(whitespace/line_length) |
There was a problem hiding this comment.
Thanks Martin. Not sure what you mean, I didn't introduce a line break, but just added two linter directives since the linter was complaining...
3 participants
This flag pretty-prints every instruction in the entire program. I use
it to learn about CPROVER's internal representation of particular
constructs, by passing in --print-internal-representation on a one-line
C program.