Search code examples
cframa-c

bogus warning on write to pointer

I am a very newbie with Frama-c and have a very short program which causes frama-c to claim that 'out of bounds write. assert\valid(iptr):

f4.c:33:[kernel] warning: out of bounds write. assert \valid(iptr); f4.c:34:[value] Assigning imprecise value to __retres.

I don't see it. Help? I don't understand what the next line means either...

code:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
/*
 * f4.c example of a 'valid' clause:
 * foo 
 * and abort.
 *
 * cmd line: frama-c -val f4.c
 */

int fill( int * iptr, int length );

const int BUF_SIZE = 100;
int main( int argc, char ** argv )
{
    int * ptr = malloc( BUF_SIZE * sizeof( int ));
    memset( ptr, 0x00,  BUF_SIZE * sizeof( int ));
    int rv = fill( ptr, BUF_SIZE );
    printf("rv = %d\n", rv); 
    return 0;
}


/* 
 * @requires  \valid(iptr+(0..length+1));
 * @requires length >= 1;
 * @assigns *iptr;
 */

int fill( int * iptr,  int length )
{
    *iptr = 3;
    return( *iptr );
}

output: ...framac [0] > frama-c -val -wp f4.c

[kernel] preprocessing with "gcc -C -E -I.  f4.c"
/usr/include/i386-linux-gnu/bits/byteswap.h:47:[kernel] warning: Calling undeclared function __builtin_bswap32. Old style K&R code?
/usr/include/i386-linux-gnu/bits/byteswap.h:111:[kernel] warning: Calling undeclared function __builtin_bswap64. Old style K&R code?
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
        BUF_SIZE ∈ {100}
[value] computing for function malloc <- main.
        Called from f4.c:17.
[kernel] warning: Neither code nor specification for function malloc, generating default assigns from the prototype
[value] using specification for function malloc
[value] Done for function malloc
[value] computing for function memset <- main.
        Called from f4.c:18.
[kernel] warning: Neither code nor specification for function memset, generating default assigns from the prototype
[value] using specification for function memset
[value] Done for function memset
[value] computing for function fill <- main.
        Called from f4.c:19.
**f4.c:33:[kernel] **warning: out of bounds write. assert \valid(iptr);**
f4.c:34:[value] Assigning imprecise value to __retres.**
        The imprecision originates from Library function {f4.c:17}
[value] Recording results for fill
[value] Done for function fill
f4.c:20:[value] Reading left-value rv.
        It contains a garbled mix of {alloced_return_malloc} because of
        Library function {f4.c:17}.
[value] computing for function printf <- main.
        Called from f4.c:20.
[kernel] warning: Neither code nor specification for function printf, generating default assigns from the prototype
[value] using specification for function printf
[value] Done for function printf
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function fill:
          __retres ∈
                  {{ garbled mix of &{alloced_return_malloc}
                   (origin: Library function {f4.c:17}) }}
          alloced_return_malloc[...] ∈
                               {{ garbled mix of &{alloced_return_malloc}
                                (origin: Library function {f4.c:17}) }}
[value] Values at end of function main:
          ptr ∈ {{ NULL + [--..--] ; &alloced_return_malloc + [0..2147483647] }}
          rv ∈
            {{ garbled mix of &{alloced_return_malloc}
             (origin: Library function {f4.c:17}) }}
          __retres ∈ {0}
          alloced_return_malloc[...] ∈
                               {{ garbled mix of &{alloced_return_malloc}
                                (origin: Library function {f4.c:17}) }}
Solution

  • The bulk of your issue lies in the following warnings:

    [value] computing for function malloc <- main.
        Called from f4.c:17.
[kernel] warning: Neither code nor specification for function malloc, generating default assigns from the prototype
[value] using specification for function malloc

    Basically, the malloc function has no implementation and no ACSL specification, so that Value Analysis does not know what to do with it, and returns a very imprecise result (namely {{ garbled mix of &{alloced_return_malloc} (origin: Library function {f4.c:17}) }}). Starting from there, false alarms can be expected to flow.

    If you intend to provide a suitable initial context for the fill function, you should use a static array instead. Public releases of Frama-C do not provide built-ins for malloc, and emulating them in pure C will probably not get you very far.

    In addition, please note that the comment before the fill function is not an ACSL specification. Those are introduced by /*@, not by /* followed somewhere later by an @.