что означает узел круга в pdgs, который генерируется frama-c

Question

Я использую инструмент frama-c для анализа кода ниже.

  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;
  }

см

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

Мой вопрос о зависимости от контроля. что означает круговой узел? Я пытаюсь объяснить узел «while», возможно, он обозначает один цикл времени, потому что цикл начинается с «i <100», поэтому существует зависимость от управления («i <100» ------ o «while» ). Что я думаю, верно? но что означает "разрывный" узел? Я думаю, что узел "goto __Cont;" связано с "перерывом"; оператор в блоке else <br> Я думаю, что у меня нет четкой абстрактной модели для полного и точного понимания зависимости от контроля. Не могли бы вы мне помочь или дать какое-нибудь предложение? Большое спасибо заранее Тао.

Answer 1

Используйте команду frama-c -print main.c, чтобы увидеть, как была переведена программа (я включил переведенную версию ниже).

Заявление goto __Cont; в нормализованном варианте является переводом continue; в оригинале.

И, как сказал Биньямин, петля for была нормализована в петлю while.

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

Большая часть говорит само за себя:

• круг - управление потоком (ветвление)
• ромб - условие (a == 0 и т. Д.)
• квадрат -присваивание

Ваш цикл for был переведен в цикл while