Search code examples
frama-c

Invalid location in Frama-c value analysis

I am trying to analyze some program that resemble the following using the value analysis:

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

After normalization and analysis the program looks like:

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

where the status of the first two assert is 'unknown' and the status of the third one is 'invalid'. Moreover the value analysis tells me that *(argv0 + 2) is an invalid location and flags all code after it as dead.

I'd like to understand why the last assert is invalid (and not the first two) and why *(argv0 + 2) is an invalid location.

I'm using Frama-c Silicon-20161101

Solution

  • Thanks to anol's comment I was able to find the relevant section in the user manual of Value Analysis (http://frama-c.com/download/frama-c-value-analysis.pdf).

    Here is an extract:

    5.2.4 Tweaking the automatic generation of initial values (p58)

    (...)

    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.