Почему график зависимости этого scanf () - программы Frama-C выглядит так? - PullRequest
Новая
       35

Почему график зависимости этого scanf () - программы Frama-C выглядит так?

5 голосов
/ 25 марта 2012

Я использую инструмент Frama-C для генерации графика зависимости этой программы (main.c).

    #include<stdio.h>
    int main()
    {
        int n,i,m,j;
        while(scanf("%d",&n)!=EOF)
        { 
            m=n;
            for(i=n-1;i>=1;i--)
            {   
                m=m*i;
                while(m%10==0)
                {
                     m=m/10;
                }
                m=m%10000;
            }  
            m=m%10;
            printf("%5d -> %d\n",n,m);
        }
       return 0;
    }

Команда: 

    frama-c -pdg -dot-pdg main main.c 
    dot -Tpdf main.main.dot -o main.pdf

Результат enter image description here У меня вопрос, почему параметры "m = m * i;" ， "m = m% 10000"не отображаются на узлы.Результат кажется неправильным, потому что в коде есть три цикла.

1 Ответ

6 голосов
/ 25 марта 2012

Срез для программ на Си работает на практике, только если его заданная цель - сохранить определенные исполнения , а срезу разрешено изменять неопределенные исполнения .

В противном случае слайсер не сможет удалить оператор, такой как x = *p;, как только он не сможет определить, что p является действительным указателем в этой точке, даже если он знает, что ему не нужен x, простопотому что если оператор удален, исполнения, в которых p равен NULL в этой точке, будут изменены.

Frama-C не обрабатывает сложные библиотечные функции, такие как scanf().Из-за этого он думает, что локальная переменная n используется без инициализации.

Тип frama-c -val main.c Вы должны получить предупреждение вроде: 

main.c:10:[kernel] warning: accessing uninitialized left-value:
               assert \initialized(&n);
...
[value] Values for function main:
      NON TERMINATING FUNCTION

Слово assert означаетчто опция Frama-C -val не может определить, что все исполнения определены, и «НЕ ПРЕКРАЩАЮЩАЯ ФУНКЦИЯ» означает, что она не может найти одно определенное выполнение программы для продолжения.

Не определеноиспользование неинициализированной переменной является причиной, по которой PDG удаляет большинство операторов.Алгоритм PDG считает, что может удалить их, потому что они приходят после того, что он считает неопределенным поведением, при первом доступе к переменной n.

Я немного изменил вашу программу, чтобы заменить вызов scanf() на более простойутверждение: 

#define EOF (-1)
int unknown_int();

int scan_unknown_int(int *p)
{
  *p = unknown_int();
  return unknown_int();
}

int main()
{
  int n,i,m,j;
  while(scan_unknown_int(&n) != EOF)
    { 
      m=n;
      for(i=n-1;i>=1;i--)
      {   
        m=m*i;
        while(m%10==0)
        {
          m=m/10;
        }
        m=m%10000;
      }  
      m=m%10;
      printf("%5d -> %d\n",n,m);
    }
  return 0;
}

и я получил PDG ниже.Это выглядит полным, насколько я могу судить.Если вы знаете программы компоновки лучше, чем dot, но которые принимают формат dot, это хороший шанс использовать их.

Complex PDG Обратите внимание, что условие while стало tmp != -1.Узлы графа являются утверждениями внутреннего нормализованного представления программы.Условие tmp != -1 имеет зависимость данных от узла для оператора tmp = unknown_int();.Вы можете отобразить внутреннее представление с помощью frama-c -print main.c, и оно покажет, что условие внешнего цикла было разбито на: 

  while (1) {
    int tmp;
    tmp = scan_unknown_int(& n);
    if (! (tmp != -1)) { break; }

Это помогает, помимо прочего, разрезать, чтобы удалить только частисложное утверждение, которое можно удалить вместо того, чтобы хранить весь сложный оператор.

...