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] void * and uintptr_t?

  • Subject: [Frama-c-discuss] void * and uintptr_t?
  • From: MarkoSchuetz at web.de (Marko Schütz Schmuck)
  • Date: Mon, 21 Apr 2014 14:29:33 -0400
Dear All,

I would expect to be able to show that the precondition of func is
satisfied:

#include <stdint.h>

//@ requires ptr != \null;
void func(void *ptr) {
  int i;
  i = *(int *)ptr;
}

int main() {
  void *p;
  int a[1000];
  p = (void *)((uintptr_t)a + 3*sizeof(int));
  func(p);
  return 0;
}

but frama-c complains

Goal func_pre_5: Pre-condition (file test.c, line 3) in 'main' at call 'func' (file test.c, line 13):
test.c:12: warning from Typed Model:
 - Warning: Hide sub-term definition
   Reason: Forbidden cast of int to pointer
Assume { (* Heap *) Have: (linked Malloc_2). }
Prove: p_0!=null.
Prover Alt-Ergo returns Unknown

but shouldn't a cast from uintptr_t to void * be legal?

What is the recommended way to deal with code that uses these casts?

Best regards,

Marko
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140421/5b5bb1d9/attachment.pgp>