2021-03-01 04:41 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002119Frama-CKernelpublic2016-01-26 13:50
Assigned Toyakobowski 
Product Version 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002119: "If" statement with only one successor
DescriptionWhen a "If" statements contains in its true block the sequence "do {} while (0);", in the CFG, this statement will have only one successor.
Steps To ReproduceYou can simply try with this C program and compute List.length stmt.succs
void f(int n) {
  if (n == 0) do {} while (0);
TagsNo tags attached.
Attached Files




yakobowski (manager)

Last edited: 2015-05-23 11:58

View 2 revisions

To clarify a bit: the AST is not outright incorrect, because the statement corresponding to 'return' is indeed the successor of both the 'then' and 'else' branch. Thus one unique successor may make sense.

On the other hand, it is much better for everyone to always have two successors for an 'if', furthermore ordered by 'then < else'.


yakobowski (manager)

Fix committed to master branch.


monate (reporter)

C'est en cours !


monate (reporter)

Mais avec une petite vérification de cohérence de sid quand même, donc ça sera un peu plus long...


yakobowski (manager)

Hum, honnêtement, c'est tellement obscur que ça ne concernera personne, et je n'arriverai pas à l'expliquer dans le Changelog.

-Issue History
Date Modified Username Field Change
2015-05-20 15:11 hugo.illous New Issue
2015-05-22 10:15 signoles Assigned To => virgile
2015-05-22 10:15 signoles Status new => assigned
2015-05-23 11:32 yakobowski Assigned To virgile => yakobowski
2015-05-23 11:58 yakobowski Note Added: 0005922
2015-05-23 11:58 yakobowski Note Edited: 0005922 View Revisions
2015-05-29 11:25 yakobowski Source_changeset_attached => framac master 1de56f50
2015-05-29 11:25 yakobowski Note Added: 0005926
2015-05-29 11:25 yakobowski Status assigned => resolved
2015-05-29 11:25 yakobowski Resolution open => fixed
2015-06-10 14:16 monate Note Added: 0005940
2015-06-10 14:17 monate Note Added: 0005941
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-01-26 13:50 yakobowski Note Added: 0006135
+Issue History