You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The merged PR #3 makes ldrgen generate a spurious "break" label along each while statement. Such a label seems to be related to some exit condition/statement for the loop which, however, does not exist.
Snippet of such a generation:
This not a dreadful issue, but it would be better not to generate such useless labels (and respective; statements).
Hypothesis on the problem
The problem seems to be related to the -simplify-cfg machinery of Frama-C, which ldrgen seems to activate in some unclear way.
Indeed, the Frama-C's pretty-printer typically recognizes code patterns like:
while(1) { if (!cond) break; ... }
and turns them into:
while (cond) { ... }
When -simplify-cfg is activated and has called on a code, the first code pattern is turned into:
while(1) { if (!cond) goto while_0_break; ... } while_0_break: ;
and the pretty-printer goes on with its job but does not remove the label as it would be difficult to do in general.
This seems the most plausible explanation of the issue, at least this is what the senior devs of Frama-C told me, but I haven't found any evident mention of -simplify-cfg nor programmatic use of it in ldrgen.
The text was updated successfully, but these errors were encountered:
lambdaxdotx
changed the title
Spurious break labels generated along while statements
Spurious break labels generated along with while statements
Dec 6, 2020
The merged PR #3 makes
ldrgen
generate a spurious "break" label along eachwhile
statement. Such a label seems to be related to some exit condition/statement for the loop which, however, does not exist.Snippet of such a generation:
This not a dreadful issue, but it would be better not to generate such useless labels (and respective
;
statements).Hypothesis on the problem
The problem seems to be related to the
-simplify-cfg
machinery of Frama-C, whichldrgen
seems to activate in some unclear way.Indeed, the Frama-C's pretty-printer typically recognizes code patterns like:
and turns them into:
When
-simplify-cfg
is activated and has called on a code, the first code pattern is turned into:and the pretty-printer goes on with its job but does not remove the label as it would be difficult to do in general.
This seems the most plausible explanation of the issue, at least this is what the senior devs of Frama-C told me, but I haven't found any evident mention of
-simplify-cfg
nor programmatic use of it inldrgen
.The text was updated successfully, but these errors were encountered: