Conversation
This introduces a type for control-flow graphs made up of basic blocks that can include the same sorts of commands that structured statements do. It includes a translation from structured statements to unstructured CFGs.
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
What will be the semantics of jumping into a block while skipping over a declaration? In C one can do:
goto lab;
int x = 42;
lab: ++x; // x is considered declared, but is uninitialisedI believe programs like the above can now be represented, but we also need to be clear on their semantics.
|
|
||
| [l_6: | ||
| [init (i : int) := init_i_0] | ||
| cgoto #true l_5 l_5, |
There was a problem hiding this comment.
Why is a comma being printed?
There was a problem hiding this comment.
Oh, I think that's a mistake. Thanks for catching!
You caught one of the key reasons I hadn't moved this from a draft yet! My current plan is to require that declarations be procedure-level when translating to CFG, but I haven't yet decided how best to enforce that. As you've probably noticed, the example you commented on with the errant comma has an |
Labels exist only in CFGs now, not blocks themselves.
Fewer `[] .goto l` blocks
2 participants
This introduces a type for control-flow graphs made up of basic blocks that can include the same sorts of commands that structured statements do. It includes a translation from structured statements to unstructured CFGs.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.