--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on July 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP and incompatible casts



Can you help me validate the following snippet of system code with Frama-C?

Please see the attached file foo.c (reproduced below), and try “frama-c -wp foo.c”.

#include <stdint.h>

typedef struct {
  unsigned id1;
  unsigned id2;
} header_t;

uint8_t buffer_data[100]; // normally allocated on the heap

void foo(){
  uint8_t *buffer = buffer_data;
  header_t *header = (header_t *)buffer;
  //@ assert buffer == (uint8_t *)header;
  return;
}

It is common for system code to receive a buffer of bytes, and for those bytes to be interpreted as a header followed by data.  Frama-C considers the two casts (header_t *)buffer and (uint8_t *)header to be incompatible.  The first may be incompatible due to data alignment, but not the second.  And whether it is reasonable or not, it is allowed by compilers like gcc and routinely done.

The problem is that the assert seems unprovable.  It seems to become the goal “Prove: buffer at L1 = w_0.” where w_0 seems to be an unconstrained symbolic value.

Thanks,
Mark






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200726/6eadeee6/attachment.html>