cframa-cacsl

How to assert that a point is unreachable?


For Frama-C and the WP plugin, how can a user assert that a point in a program is unreachable?

Looking for something like:

//@ assert \unreachable;

Solution

  • You can use //@ assert \false; for an assertion that a point is unreachable because:

    a (provably) unreachable assertion is always proved to be true

    via Introduction to C program proof with Frama-C and its WP plugin by Allan Blanchard.

    e.g. For a given file main.c:

    /*@
      assigns \nothing;
    */
    int foo(const int input) {
        int result = 0;
    
        if (input > 0) {
            result += 1;
    
            if (input < 0) {
                // This assertion will be proved successfully
                // because this location is provably unreachable.
                //@ assert \false;
    
                result += 1;
            }
        }
    
        return result;
    }
    

    To verify that the assertion is proved:

    $ frama-c -wp main.c
    [kernel] Parsing main.c (with preprocessing)
    [wp] Warning: Missing RTE guards
    [wp] 3 goals scheduled
    [wp] Proved goals:    3 / 3
      Qed:             3
    

    The above is using frama-c version 25.0 (Manganese).