scanf not working as expected in Frama-C

Question

In the program below, function dec uses scanf to read an arbitrary input from the user.

dec is called from main and depending on the input it returns 1 or 0 and accordingly an operation will be performed. However, the value analysis indicates that y is always 0, even after the call to scanf. Why is that?

Answer 1

Note: the comments below apply to versions earlier than Frama-C 15 (Phosphorus, 20170501); in Frama-C 15, the Variadic plugin is enabled by default (and its short name is now -variadic).

Solution

• Enable Variadic (-va) before running the value analysis (-val), it will eliminate the warning and the program will behave as expected.

Detailed explanation

Strictly speaking, Frama-C itself (the kernel) only does the parsing; it's up to the plug-ins themselves (e.g. Value/EVA) to evaluate the program.

From your description, I believe you must be using Value/EVA to analyze a program. I do not know exactly which version you are using, so I'll describe the behavior with Frama-C Silicon.

One limitation of ACSL (the specification language used by Frama-C) is that it is not currently possible to specify contracts for variadic functions such as scanf. Therefore, the specifications shipped with the Frama-C standard library are insufficient. You can notice this in the following program:

#include <stdio.h>
int d;

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

Running frama-c -val file.c will output, among other things:

...
[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})
...

That warning means that the specification is incorrect, which explains the odd behavior.

The solution in this case is to use the Variadic plug-in (-va, or -va-help for more details), which will specialize variadic calls and add specifications to them, thus avoiding the warning and behaving as expected. Here's the resulting code (-print) after running the Variadic plug-in on the example above:

$ 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;
}

In this example, scanf was specialized to scanf_0, with a proper ACSL annotation. Running EVA on this program will not emit any warnings and produce the expected output:

@ frama-c -va file.c -val 

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

Note: the GUI in Frama-C 14 (Silicon) does not allow the Variadic plug-in to be enabled (even after ticking it in the Analyses panel), so you must use the command-line in this case to obtain the expected result and avoid the warning. Starting from Frama-C 15 (Phosphorus, to be released in 2017), this won't be necessary: Variadic will be enabled by default and so your example would work from the start.