Checking bits in an unsigned integer using frama-c lemma does not work

Question

Using frama-c I was working on code which uses a bit-field to represent a set. Say something like

typedef uint32_t  myset_t;

#define EMPTY_SET  UINT32_C(0)
#define FULL_SET   UINT32_C(0x0ffffff)

so I'm using the n lowest bits of a 32-bit unsigned integer only. Then I wanted to implement a predicate for checking if a bit is set in the "myset_t". This did not work as expected (frama-c with alt-ergo capable of proving stuff about such sets) and I could produce the a simple lemma which already shows my problem. On my installation (frama-c 21.1 Scandium), it is not capable to automatically prove the following simple lemma:

    lemma test:
        \forall integer i;
        (0U <= i < 16U) ==> (0xFFFFU & (1U << (unsigned int)i)) != 0U;

Is anyone able to explain to me what I'm doing wrong and where the problem is? Or are the theorem-provers not capable of getting these trivial arithmetic things right automatically (I mean it's just 16-cases, one could just enumerate them).

Ksass'Peuk Ksass'Peuk · Accepted Answer · 2020-08-03T08:43:55

It seems that the automatic solvers cannot deal with the property generated by WP. Maybe because they cannot or maybe because of the encoding of the property.

Nevertheless, as you said:

it's just 16-cases, one could just enumerate them

And WP GUI provides a tactic to generate such a proof. Once the proof as failed, double click on the proof goal in the "WP Goal" panel at the bottom of the window. Then select the variable to enumerate. Click on the tactic "Range" and set the lower to 0 and the upper to 15. Finally, click on the green arrow next to the name of the tactic. WP will generate 18 proof goals:

< 0 and > 15: trivial as the condition is 0 <= i <= 15
0, 1, 2, 3 ..., 15: discharged automatically by WP Qed

Then you can click on the save icon so that the proof can be replayed easily.

If you then want to replay the proof, from the GUI, you can use the arrow that appears in the "WP Goal" panel when there exists a proof script. Or you can directly ask to use the existing scripts in the command line by adding tip to the list of the provers:

frama-c -wp -wp-prover alt-ergo,tip file.c

Note that the WP scripts are saved in the WP session, which is by default in the directory ./.frama-c/wp/scripts. The WP session directory can be configured using the option wp-session <directory>.

Checking bits in an unsigned integer using frama-c lemma does not work

1 Answers