CODEWITHSUNDEEP
frama-c
MEE
MEE

Reputation: 2412

Frama-C non-terminating evaluation

I am trying to slice the following program on the printf call:

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

int main(int argc, char **argv) {

  if (argc < 3) return 1;

  int x = atoi(argv[1]);
  int y = atoi(argv[2]);

  printf("%d %d\n", x, y);

  return 0;
}

However, the Value Analysis plugin gives the following message:

foo.c:9:[value] Non-termination in evaluation of function call expression argument (char const )(argv + 2),

and the sliced program is empty! Is this a bug/feature in Frama-C? Or am I doing something wrong?

Here's a complete trace: 

$ frama-c -slice-calls printf foo.c -then-on 'Slicing export' -print
[slicing] slicing requests in progress...
[kernel] preprocessing with "gcc -C -E -I.  foo.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
foo.c:8:[kernel] warning: out of bounds read. assert \valid(argv+1);
[value] computing for function atoi <- main.
        Called from foo.c:8.
[kernel] warning: No code for function atoi, default assigns generated
[value] Done for function atoi
foo.c:9:[kernel] warning: out of bounds read. assert \valid(argv+2);
foo.c:9:[value] Non-termination in evaluation of function call expression argument
        (char const *)*(argv + 2)
[value] Recording results for main
[value] done for function main
[slicing] making slicing project 'Slicing'...
[slicing] interpreting slicing requests from the command line...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[slicing] exporting project to 'Slicing export'...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */

Upvotes: 2

Views: 411

Answers (1)

Pascal Cuoq
Pascal Cuoq

Reputation: 80276

See 5.2.3 Analysis of an incomplete application in the value analysis manual:

For a variable of a pointer type, there is no way for the analyzer to guess whether the pointer should be assumed to be pointing to a single element or to be pointing at the beginning of an array — or indeed, in the middle of an array, which would mean that it is legal to take negative offsets of this pointer. By default, a pointer type is assumed to point at the beginning of an array of two elements. This number can be changed with option -context-width. Example: if the prototype for the entry point is void main(int *t), the analyzer assumes t points to an array int S_t[2].

The same applies to the argument argv of the main() function of your program. Build a proper array of pointers that you expect to correspond to main() arguments in practice as explained elsewhere in the manual (e.g. main_2.c page 23). If you only intend to verify or slice your program for well-formed integers in the range 0 .. 1000, you can insert /*@ assert 0 <= x <= 1000 ; */ in the program after x has been assigned.

[kernel] warning: No code for function atoi, default assigns generated

You should also read 2.3.3 Missing functions in the same manual. Tell you what, read the manual first and try to use the value analysis and slicing plug-in later. This is a steep learning curve for a piece of software nowadays, but that is really how it is intended to be used.

Anyway, an implementation or a minimal specification should be provided for all functions that are encountered by the analyzer. The most recent release of Frama-C contains in share/libc some pretty good specifications for a lot of standard functions, which may have been installed in /usr/local/lib/Frama-C/libc on your computer.

Upvotes: 2

Related Questions