Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP and incompatible casts

  • Subject: [Frama-c-discuss] WP and incompatible casts
  • From: mrtuttle at amazon.com (Tuttle, Mark)
  • Date: Sun, 26 Jul 2020 18:58:08 +0000
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>