Что означает сообщение о недоступной точке входа?

У меня есть файл, содержащий несколько утверждений ACSL (file.c):

#include <stdio.h>
#include <stdlib.h>

void foo()    {
  int a=0;
  //@ assert(a==0);
}

void print(const char* text)   {
    int a=0;
    //@ assert(a==0);
    printf("%s\n",text);
}

int main (int argc, const char* argv[])    {
    const char* a1 = argv[2];

    print(a1);
    foo();

    if (!a1)
      //@ assert(!a1);
        return 0;
    else
        return 1;
}

Я хочу нарезать все утверждения с помощью команды:

frama-c -slice-assert @all file.c -then-on 'Slicing export' -print -ocode slice.c

Однако слайс выглядит не так, как ожидалось (на самом деле он не содержит ни одной из функций, содержащихся в файлах):

/* Generated by Frama-C */
typedef unsigned int size_t;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;

  }
 */
void main(void)
{
  char const *a1;
  return;
}

Вместо этого я получаю вывод следующим образом:

file.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+2);
[value] Recording results for main
[value] done for function main
file.c:16:[value] Assertion 'Value,mem_access' got final status invalid.
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[pdg] computing for function foo
[pdg] warning: unreachable entry point (sid:1, function foo)
[pdg] Bottom for function foo
[slicing] bottom PDG for function 'foo': ignore selection
[pdg] computing for function main
file.c:21:[pdg] warning: no final state. Probably unreachable...
[pdg] done for function main
[pdg] computing for function print
[pdg] warning: unreachable entry point (sid:5, function print)
[pdg] Bottom for function print
[slicing] bottom PDG for function 'print': ignore selection

Что здесь не так, в частности, что делает unreachable entry point? Наблюдение: если я изменю argv[2] на argv[1], у меня не будет этих проблем (но все равно появится предупреждение в первой строке).


program-slicing frama-c
person Paddre    schedule 25.07.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Срезу необходимо вычислить PDG (программно-зависимый график), который использует результаты анализа значений. Предупреждение unreachable entry point означает, что в заданном вами контексте функция foo недостижима (т. е. она вызывается из операторов unreachable).

Без примера сложно сказать больше...

РЕДАКТИРОВАТЬ:

В предоставленном вами выводе обратите внимание на строки:

file.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+2);

а также

file.c:16:[value] Assertion 'Value,mem_access' got final status invalid.

Когда анализ значений обнаруживает недопустимое свойство, он не может двигаться дальше. Поскольку здесь тревога исходит из первого утверждения, все остальное становится недостижимым. Недопустимым свойством является \valid_read(argv+2);, так как значение по умолчанию для входного контекста должно иметь ширину 2 для argv. Это можно исправить либо с помощью опции -context-width 3, либо с помощью другой точки входа для анализа (и указать ее с помощью -main my_main), которая не принимает аргументов, явно определяет argc и argv и вызывает с ними настоящую main.

Рекомендуется использовать срезы только после проверки правильности результатов анализа стоимости. Вы можете запустить его отдельно с параметром -val и при необходимости настроить другие параметры.

person Anne    schedule 27.07.2016
comment
Спасибо за Ваш ответ. Я смог разработать наглядный пример и соответствующим образом отредактировал (/рефакторил) свой вопрос. - person Paddre; 27.07.2016