WP Plugin: Why does the following simplified code fail to verify

Question

I am a new Frama-C User and I am trying to prove certain properties for a large project. I was seeing a particular proof fail, and tried reducing the problem to a minimum reproducible example, and the following is the code:

#include <stdlib.h>

/*@ requires (x != 0) && (y + 1 >= 1024);
*/
int f1(unsigned int x, unsigned int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

I use the following command to verify:

frama-c -wp -wp-prover=alt-ergo,z3,cvc4 a.c -kernel-warn-key annot-error=active -then -no-unicode -report

The above code fails to verify with frama-c with the following message:

Assertion x != 0 && y >= 1024: Unproven

Could you please explain why does this verification fail?

I tried simplifying my original proof manually and came up with the above example. I expect the verification to go through. I believe I may be misunderstanding how frama-c treats "y+1" for C data types, as opposed to purely mathematical datatypes like Int.

Edit:

The following code verifies successfully (I just changed the variable types from unsigned to signed):

#include <stdlib.h>

/*@ requires (x != 0) && (y + 1 >= 1024);
*/
int f1(int x, int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

Edit 2: Versions: Frama-C: 27.1 (Cobalt) Alt-ergo: 2.4.3 CVC4: 1.6 Z3: 4.12.2

Edit3:

I tried in the frama-c version 28.1 as well and it still fails.

Answer 1

The main issue is that y + 1 in ACSL does not mean the same thing as y+1 in C. More precisely, as mentioned in the ACSL manual, arithmetic operations are evaluated in ACSL over mathematical, unbounded, integers. Hence the fact that y+1>=1024 in the requires clause is not sufficient to conclude that y>=1024 after the y=y+1 in the assignment: if we pass UINT_MAX to f, we end up with y == 0. Adding another requires, e.g. y+1 <= UINT_MAX + 1, will solve the issue.

Regarding the variant with int, things are a little bit different. In fact, while an unsigned overflow is perfectly defined in C (we simply wrap up the value), signed overflow is not: we have an undefined behavior. Thus, by default Frama-C will consider that a signed overflow is a runtime-error. For Wp, this means that it will assume that no such overflow can occur, and checking that is delegated to the generation of annotation with the Rte plug-in by using -wp-rte: with this option, you get a non-proved assertion, namely the one generated by Rte.

Similarly, if you add option -warn-unsigned-overflow to the unsigned variant, everything seems proved at first, but adding -wp-rte reveals an unproved, Rte-generated, assertion, while add option -no-warn-signed-overflow to the signed variant gives you the same behavior as the unsigned.

To summarize, if we use the following C file t.c and launch frama-c with various set of options, we obtain the following results:

#include<limits.h>

/*@ requires (x != 0) && (y + 1 >= 1024);
#ifdef ACSL_NO_OVERFLOW
  requires no_overflow: y + 1 <= UINT_MAX;
#endif
*/
int f1(unsigned int x, unsigned int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

/*@ requires (x != 0) && (y + 1 >= 1024);
#ifdef ACSL_NO_OVERFLOW
  requires no_overflow: y + 1 <= INT_MAX;
#endif
*/
int f2(int x, int y) {
    y = y + 1;
    //@ assert (x != 0) && (y >= 1024);
    return 0;
}

frama-c command	Proved Goals
frama-c -wp t.c	5/6
frama-c -wp t.c -wp-rte	5/7
frama-c -wp t.c -wp-rte -cpp-extra-args="-DACSL_NO_OVERFLOW"	7/7
frama-c -wp t.c -warn-unsigned-overflow	6/6
frama-c -wp t.c -warn-unsigned-overflow -wp-rte	6/8
frama-c -wp t.c -no-warn-signed-overflow	4/6
frama-c -wp t.c -no-warn-signed-overflow -wp-rte	4/6
frama-c -wp t.c -warn-unsigned-overflow -wp-rte -cpp-extra-args="-DACSL_NO_OVERFLOW"	8/8
frama-c -wp t.c -no-warn-signed-overflow -wp-rte -cpp-extra-args="-DACSL_NO_OVERFLOW"	6/6