Каково значение узла окружности в 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.
Я думаю, что у меня нет четкой абстрактной модели в моей голове, чтобы понять зависимость от контроля полностью и точно. Вы поможете мне или дадите мне какое-нибудь предложение? Большое спасибо в Advance Tao.

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 и т.д.)
• площадь - назначение

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