Scanf не работает должным образом в Frama-C

Question

В программе ниже функция dec использования scanf прочитать произвольный ввод от пользователя.

dec вызывается из main и в зависимости от входа он возвращает 1 или 0 и, соответственно, будет выполнена операция. Тем не менее, анализ стоимости показывает, что y всегда 0даже после звонка scanf, Это почему?

Answer 1

Примечание: приведенные ниже комментарии относятся к версиям, предшествующим Frama-C 15 (Phosphorus, 20170501); в Frama-C 15 плагин Variadic включен по умолчанию (и его короткое имя теперь -variadic).

Решение

• Включить Variadic (-va) перед запуском анализа значений (-val), это устранит предупреждение, и программа будет вести себя как ожидалось.

Детальное объяснение

Строго говоря, сама Frama-C (ядро) выполняет только разбор; это зависит от самих плагинов (например, Value/EVA) для оценки программы.

Из вашего описания я считаю, что вы должны использовать Value / EVA для анализа программы. Я не знаю точно, какую версию вы используете, поэтому я опишу поведение Frama-C Silicon.

Одним из ограничений ACSL (языка спецификации, используемого Frama-C) является то, что в настоящее время невозможно указать контракты для функций с переменными параметрами, таких как scanf, Поэтому спецификации, поставляемые со стандартной библиотекой Frama-C, недостаточны. Вы можете заметить это в следующей программе:

#include <stdio.h>
int d;

int main() {
  scanf("%d", &d);
  Frama_C_show_each(d);
  return 0;
}

Бег frama-c -val file.c будет выводить, между прочим:

...
[value] using specification for function scanf
FRAMAC_SHARE/libc/stdio.h:150:[value] warning: no \from part for clause 'assigns *__fc_stdin;' of function scanf
[value] Done for function scanf
[value] Called Frama_C_show_each({0})
...

Это предупреждение означает, что спецификация неверна, что объясняет странное поведение.

Решением в этом случае является использование плагина Variadic (-va, или же -va-help для получения более подробной информации), которая будет специализироваться на вызовах с переменным номером и добавлять к ним спецификации, что позволит избежать предупреждений и вести себя, как ожидается. Вот результирующий код (-print) после запуска плагина Variadic в приведенном выше примере:

$ frama-c -va file.c -print

[... lots of definitions from stdio.h ...]

/*@ requires valid_read_string(format);
    requires \valid(param0);
    ensures \initialized(param0);
    assigns \result, *__fc_stdin, *param0;
    assigns \result
      \from (indirect: *__fc_stdin), (indirect: *(format + (0 ..)));
    assigns *__fc_stdin
      \from (indirect: *__fc_stdin), (indirect: *(format + (0 ..)));
    assigns *param0
      \from (indirect: *__fc_stdin), (indirect: *(format + (0 ..)));
 */
int scanf_0(char const *format, int *param0);

int main(void)
{
  int __retres;
  scanf_0("%d",& d);
  Frama_C_show_each(d);
  __retres = 0;
  return __retres;
}

В этом примере scanf был специализирован на scanf_0, с правильной аннотацией ACSL. Запуск EVA в этой программе не выдаст никаких предупреждений и даст ожидаемый результат:

@ frama-c -va file.c -val 

...
[value] Done for function scanf_0
[value] Called Frama_C_show_each([-2147483648..2147483647])
...

Примечание. Графический интерфейс в Frama-C 14 (Silicon) не позволяет включать подключаемый модуль Variadic (даже после того, как он отмечен галочкой на панели "Анализы"), поэтому в этом случае для получения ожидаемого результата необходимо использовать командную строку. и избежать предупреждения. Начиная с Frama-C 15 (Phosphorus, будет выпущен в 2017 году), в этом нет необходимости: Variadic будет включен по умолчанию, поэтому ваш пример будет работать с самого начала.