cframa-cprogram-slicing

frama-c stops propagation: "Assertion got status invalid"

I want to slice the file test.c for all assertions.

test.c looks as follows:

#include <stdlib.h>

typedef struct {
   float r;
   float g;
   float b;
} Color;

typedef struct {
   int k;
   Color* colors;
} Colors;

void foo(int* a, int k, Colors *colors)
{
    int b=0;   
    colors->colors = (Color*) malloc(k*sizeof(Color));
    //@ assert (colors == NULL);
    if (colors==NULL)
        return;

    colors->k = k;
    int c=10;
    *a=8;
    //@ assert(*a>b);
}

I run frama-c with the following command:

frama-c -slice-assert @all -main foo test.c -then-on 'Slicing export' -print -ocode slice.c

The resulting slice.c looks as follows:

/* Generated by Frama-C */
typedef unsigned int size_t;
struct __anonstruct_Color_1 {
   float r ;
   float g ;
   float b ;
};
typedef struct __anonstruct_Color_1 Color;
struct __anonstruct_Colors_2 {
   int k ;
   Color *colors ;
};
typedef struct __anonstruct_Colors_2 Colors;
/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */

/*@
axiomatic dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;

  }
 */
void foo(int *a, Colors *colors)
{
  int b;
  /*@ assert colors ≡ (Colors *)((void *)0); */ ;
  return;
}

Looking at the sliced function foo, it seems as if the processing was somehow incomplete. The frama-c output tells me:

test.c:19:[kernel] warning: out of bounds write. assert \valid(&colors->colors);
test.c:20:[value] Assertion got status invalid (stopping propagation).

What is "status invalid" supposed to mean? Why does it stop propagating here and why does it work, when I change the first assertion to //@ assert (colors != NULL);?

Solution

  • The Slicing plug-in relies on information computed by Value Analysis. During its run, Value Analysis attempts to evaluate any ACSL annotation present on the branches it explores. This is in particular the case for assert colors == NULL; in your example, which is indeed deemed to be invalid.

    Why is that? First, we can note that colors is a formal argument of the main entry point. By default, Value Analysis will create an initial state in which such pointer is either NULL or a pointer to a block of two elements (see Value's user manual for more information about the default initial state of the analysis and how it can be customized if needed). Thus it would seem that the assertion would just remove the second possibility and keep NULL as the only possibility for colors.

    However, there is one other thing the function is doing with colors before reaching the assert: it assigns something in colors->colors. For this assignment to be valid, colors needs to point to a valid memory location. Hence the warning you see on line 19 (seemingly emitted by the kernel for historical reasons, but in reality emitted by Value), materialized by the generation of another assertion, \valid(&colors->colors), that you can see if you launch frama-c-gui with your options.

    After having emitted an alarm, Value attempts to reduce its internal state according to it, as a concrete execution can only go further (without venturing in Undefined Behavior land) if it validates the given condition. In our case, this means removing NULL for the set of possible values for colors. Hence, when we encounter the assertion, we only have one possibility for colors, and since it does not match the assertion, the status is invalid and propagation is stopped: no concrete execution can attain this point and validate the assertion.

    UPDATE If you change the first assertion to //@ assert (colors != NULL);, Value analysis will find it is valid, since, as said above, reaching the point where the assertion is evaluated can only be done with a valid colors pointer because of the colors->colors in the previous instruction. Thus Value proceeds with the analysis, and the Slicing is done on a program that terminates normally, leading to the expected result.

    Regarding your comment, an ACSL annotation is valid if during any concrete execution of the program which passes through the annotation, it evaluates to true, and invalid otherwise (and execution is supposed to stop in case the annotation evaluates to false). In practice, it is often not possible (at least not in a reasonable amount of time and/or memory) to perform all such evaluations, hence the unknown status, meaning that the plugin can't decide. Note that in any case, the status emitted by a given plugin depends on the configuration of this plugin. For instance for Value, the chosen entry point and initial configuration have an impact on the validity status of the annotations encountered by Value during its abstract execution. More precisely, each time the abstract execution reaches an annotation, the status is computed as follows: