what's the meaning of the circle node in pdgs which is generated by frama-c

Question

I use frama-c tool to analyse the code below.

  int main (int argc, char *argv[])
  {
     int i,a;
     for (i = 0; i < 100; i += 1)
     {
        a=0;
        if (a==0)
        {
            continue;
        }
        else
        {
            break;
        }
     }
     return 0;
  }

the cmd is

   frama-c -pdg -dot-pdg graph main.c

My question is about the control dependence. what's the circle node means? I try to explain the "while" node, maybe it stand for one time loop , because a loop start from "i<100",so there a control dependence ("i<100" ------o "while" ). Is what I guess right ? but what is the "break" node mean? I guess that node "goto __Cont;" is related to the "break;" statement in the "else" block.
I think I have no clear abstract model in my head for understanding the control dependence completely and accurately . Would you help me or give me any suggestion ?. Many Thanks in Advance Tao.

Answer 1

Use the command frama-c -print main.c to see how the program was translated (I include the translated version below).

The statement goto __Cont; in the normalized version is the translation of continue; in the original.

And, as Binyamin said, the for loop was normalized into a while loop.

int main(int argc, char **argv)
{
  int __retres;
  int i;
  int a;
  i = 0;
  while (i < 100) {
    a = 0;
    if (a == 0) { goto __Cont; }
    else { break; }
    __Cont: /* internal */ i ++;
  }
  __retres = 0;
  return (__retres);
}

Answer 2

Most of it is self explanatory:

• circle - flow control (branching)
• rhombus - condition (a == 0 etc.)
• square - assignment

Your for loop was translated to a while loop