2

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

Frama-C screenshot of function dec

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?

anol
  • 8,264
  • 3
  • 34
  • 78
karan
  • 67
  • 4
  • 1
    It would be helpful if you could give more concrete examples or better detail your question. Frama-C follows the C standard for initialization (globals are set to 0), but there is also a `-lib-entry` option that treats globals as uninitialized. Though usually the way to handle I/O variables is to define them as `volatile`. – anol Feb 28 '17 at 15:10
  • for example a global variable is reading value from standard input by using scanf. But frama-c still takes 0 as its value. – karan Mar 01 '17 at 03:59
  • I've posted an answer to what I believe might be your issue. If it is, please reword your question to match the actual issue here (otherwise, clarify the question, if possible with a concrete example so that we can understand what exactly is the issue). – anol Mar 01 '17 at 07:50
  • @anol Please see the images having an example related to my doubt. – karan Mar 01 '17 at 09:16
  • The *Messages* tab on the bottom indicates `(1)`, which is precisely the warning I mentioned in my answer. I **really** recommend using the command-line for analyses with Value/EVA; while the GUI does allow it, it is **not** a good approach for beginners (use it for visualization, never for parametrization). In particular, there is an issue with the GUI that prevents the Variadic plug-in from being properly enabled (even if you activate it via the "Analyses" panel). If you start the GUI with `-va` (to force Variadic to run), the warning will disappear and your program will behave as expected. – anol Mar 01 '17 at 10:06
  • as the value of y will be taken at run time, why frama-c shows else part to be dead code ? – karan Mar 06 '17 at 10:43
  • As I explained in my answer, without the Variadic plug-in, Frama-C is unable to put an ACSL specification on variadic functions such as printf. In the absence of specifications, Frama-C/EVA emits a warning and introduces the (possibly unsound, hence the warning) assumption that no parameters are assigned by the function. Therefore `x`, `y` and `z` retain their initial value (zero), which explains why the other branch is considered dead. – anol Mar 06 '17 at 12:32
  • in other case if a function say _read_ is present in a library file which does the job of reading serial port and updates the value of a variable say _y_, and in project we have only prototype of _read_, and y is denominator in next statement. Is there any way to solve this? – karan Mar 07 '17 at 11:49
  • For functions without body, you need either to stub a body simulating the original behavior, or use ACSL specifications. The [Frama-C blog](http://blog.frama-c.com/index.php?post/2016/09/23/mini-acsl-tutorial) contains some posts about it. Or you can ask a separate question here in SO about that, because it seems unrelated from the variadic issue in this question. – anol Mar 07 '17 at 12:34

1 Answers1

2

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.

anol
  • 8,264
  • 3
  • 34
  • 78