[WP] Trivial goals of two integer pointer cannot be verified
Steps to reproduce the issue
In this function fix_target_val
, the goal is to prove that in certain case, pointers target & offset are modified correctly.
I found that ensures mode == 0 && val < 4 ==> *offset == 1;
can't be verified but ensures mode == 0 && val < 4 ==> *target == 0;
cannot.
Both ensures clauses are expected to be valid.
[kernel] Parsing test2.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
[wp] [Failed] Goal typed_cast_fix_target_val_ensures_2
Coq 8.15.2: Unknown (Qed:8ms)
CVC4 1.7: Unknown (Qed:8ms) (cached)
[wp] [Cache] found:1
[wp] Proved goals: 11 / 12
Qed: 11 (0.93ms-3ms-6ms)
CVC4 1.7: 0 (unknown: 1) (cached: 1)
Coq 8.15.2: 0 (unknown: 1)
#include <stdio.h>
typedef unsigned char U8;
typedef unsigned long U32;
/*@
requires \valid(target) && \valid(offset);
requires 0 <= val < 1024;
requires 0 <= mode <= 2;
assigns *offset, *target;
ensures mode == 0 && val < 4 ==> *target == 0;
ensures mode == 0 && val < 4 ==> *offset == 1;
@*/
void fix_target_val(U32 val, U8 *offset, U8 *target, U8 mode)
{
if (mode == 0)
{
if (val < 4)
{
*offset = 1;
*target = 0;
}
}
}
In another case, I switch the order of the assignment of offset & target.
Here's what I got.
[kernel] Parsing test2.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
[wp] [Failed] Goal typed_cast_fix_target_val_ensures
Coq 8.15.2: Unknown (Qed:8ms)
CVC4 1.7: Unknown (Qed:8ms) (cached)
[wp] [Cache] found:1
[wp] Proved goals: 11 / 12
Qed: 11 (0.93ms-2ms-6ms)
CVC4 1.7: 0 (unknown: 1) (cached: 1)
Coq 8.15.2: 0 (unknown: 1)
/*@
requires \valid(target) && \valid(offset);
requires 0 <= val < 1024;
requires 0 <= mode <= 2;
assigns *offset, *target;
ensures mode == 0 && val < 4 ==> *target == 0;
ensures mode == 0 && val < 4 ==> *offset == 1;
@*/
void fix_target_val(U32 val, U8 *offset, U8 *target, U8 mode)
{
if (mode == 0)
{
if (val < 4)
{
*target = 0;
*offset = 1;
}
}
}
The commend I use:
frama-c -wp -wp-no-rte \
-wp-prover cvc4,coq \
-wp-model 'Typed+Cast' \
-c11 \
-main fix_target_val \
-lib-entry ./test.c \
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 25.0 (Manganese) (as reported by
frama-c -version
) - Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.6 LTS