Dereferencing pointers of type uintptr_t not supported

[Mark Tuttle]

I notice that verifast cannot verify

#include <stdlib.h>

void test()

//@ requires true;

//@ ensures true;

{

  size_t *ptr = malloc(sizeof(size_t));

  if (ptr == 0) abort();

  

  *ptr = 42;

  assert(*ptr == 42);

  free(ptr);

}

but can verify the same code if I replace size_t with int.  I notice that the heap chunks with size_t are

integer_(ptr, sizeof_ptr, false, 42)
malloc_block(ptr, sizeof_ptr)

and the heap chunks with int are 

integer(ptr, 42)
malloc_block_ints(ptr, 2)

Are there predicates or lemmas I could write to teach verifast how to dereference a size_t pointer?  I'm looking to prelude.h for guidance on how verifast handles ints.

Thanks!

[t. r.]

Hi Mark,

you can verify the program if you dereference the pointer outside of the assert statement. For instance, you can introduce a new variable ptr_val storing the pointer. Then you could substitute *ptr by ptr_val in the assert statement.

#include <stdlib.h>

void test()
//@ requires true;
//@ ensures true;
{
    size_t *ptr = malloc(sizeof(size_t));
    if (ptr == 0) abort();
 
    *ptr = 42;

    size_t ptr_val = *ptr;
    assert(ptr_val == 42);
    free(ptr);
}

Since you asked about lemma functions, a lemma to dereference size_t pointers would have the form:

/*@
lemma int deref_size_t_ptr(size_t* ptr)
requires integer_(ptr, ?size, ?signed_, ?value);
ensures integer_(ptr, size, signed_, value) &*& result == value;
{
    return value;
}
@*/

But you can't use such a lemma directly inside a ghost assert statement. So, I would recommend to simply introduca a new (ghost) variable and use that in the assert.

Best,

Tobias

[Bart Jacobs]

There was some code missing in the symbolic execution engine. I just added it.

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/7b438bab-8850-41a5-b4d8-353a39f2bae0n%40googlegroups.com.