Dereferencing pointers of type uintptr_t not supported

245 views
Skip to first unread message

Mark Tuttle

unread,
May 19, 2021, 2:49:54 PM5/19/21
to VeriFast
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.

unread,
May 20, 2021, 4:46:57 AM5/20/21
to VeriFast
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

unread,
May 30, 2021, 1:56:49 PM5/30/21
to VeriFast

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.
Reply all
Reply to author
Forward
0 new messages