Invalid место в анализе стоимости Frama-с

Я пытаюсь проанализировать какую-то программу, которая выглядеть следующим образом с помощью анализа значения:Invalid место в анализе стоимости Frama-с

int main(int argc, char **argv){ 
    char *argv0 = argv[0]; 
    char x = argv0[1]; 
    char y = argv0[2]; 
    return 0; 
}

После нормализации и анализа выглядит программа, как:

int main(int argc, char **argv){ 
    int __retres; 
    char *argv0; 
    char x; 
    char y; 
    /*@ assert Value: mem_access: \valid_read(argv + 0); */ 
    argv0 = *(argv + 0); 
    /*@ assert Value: mem_access: \valid_read(argv0 + 1); */ 
    x = *(argv0 + 1); 
    /*@ assert Value: mem_access: \valid_read(argv0 + 2); */ 
    y = *(argv0 + 2); 
    __retres = 0; 
    return __retres; 
}

где статус первых двух утверждений «неизвестен», а статус третьего - «недействителен». Более того, анализ стоимости говорит мне, что * (argv0 + 2) является недопустимым местоположением и помещает весь код после его смерти.

Я хотел бы понять, почему последнее утверждение недействительно (а не первые два) и почему * (argv0 + 2) является недопустимым местоположением.

Я использую Frama-с кремниево-20161101

источник

2017-01-26 rsaill

Я дам более опытный ответ разработчику, но это связано с опцией '-context-width'. В целом, я не рекомендую использовать его при запуске Value, но вместо этого определяю другую функцию 'main', где вы явно инициализируете' argc' и 'argv', чтобы содержать недетерминированные значения, а затем вызываете свою оригинальную функцию' main' из другой один. – anol

anol прав, и этот комментарий должен стать самостоятельным ответом. В настоящее время 'argv' не обрабатывается особым образом; следовательно, это ограничение на два аргумента. – byako

Благодаря Anol Прокомментируем я был в состоянии найти соответствующий раздел в руководстве пользователя Analysis Value (http://frama-c.com/download/frama-c-value-analysis.pdf).

Вот выдержка:

5.2.4 Tweaking автоматическую генерацию начальных значений (P58)

(...)

Для переменной типа указателя, существует это не значит, что анализатор должен угадать, следует ли считать указатель указывать на один элемент или указывать в начале массив - или, действительно, в середине массива, что означает, что это право принимать отрицательные смещения этого указателя.

По умолчанию предполагается, что тип указателя указывает на начало массива из двух элементов. Этот номер можно изменить с помощью опции -context-width.

источник

2017-01-26 20:07:54 rsaill

Invalid место в анализе стоимости Frama-с

ответ

Смежные вопросы