Unproven validity of memory access
Description
According to the ACSL language implementation p.67 for Frama-C v26.0 and 26.1 (modulo potential alignment constraints), the valid {L}(p) <==> \valid{L}(((char *)p)+(0 .. sizeof(*p)-1))
equivalence should hold true for any pointer p
(and would be in line with C's behavior when trying to access any pointer as an array of bytes). But I've run into trouble trying to prove it in simple cases, be it using the Typed
memory model, or its extension using +cast
.
Steps to reproduce the issue
Running Frama-C with WP on the minimal code inlined below, or running frama-c-gui char_ptr.c -wp
and frama-c-gui char_ptr.c -wp -wp-model Typed+cast
using the attachments.
#include <stdio.h>
typedef struct {
int test_buffer[5];
} test_type;
int * test_ptr;
test_type * _test_type_ptr;
int dummy_valid()
{
/*@ check \valid(test_ptr) ==> \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) -
/*@ check \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) - 1)) ==> \valid(
/*@ check \valid(_test_type_ptr) ==> \valid(((char *) _test_type_ptr) + (0 .. (size_t) sizeof(*_test_type_ptr) -
/*@ check \valid((char *) _test_type_ptr + (0 .. (size_t) sizeof(*_test_type_ptr) - 1)) ==> \valid(_test_type_ptr);*/
return 0;
}
Expected behaviour
All check clauses should be proved when using the +cast
variant of Typed
.
Actual behaviour
None of the check clauses extending the validity of the original pointer to the validity of the corresponding byte array are proved.
My understanding/guess would be that it may be due to WP's ability to translate the cast to char *
to byte accesses, but I'm really not clear on what's actually happening there.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 26.0 (Iron)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
Additional information (optional)
- Alt-Ergo version : 2.4.2
FYI @nkosmatov