How to mark unused pointers arguments?

[Arseniy Zaostrovnykh]

Hello, I have a function that needs a pointer for verification purpose (the pointer will go into some output predicate), but it does not really do anything with it, so when I compile the code with '-Werror=unused-parameter' I get an "unused parameter" error.
AFAIK, the cannonical way to locally suppress this error, is to put `(void)argp` in the beginning of the function. But it does not work for pointers with VeriFast: you can not cast a pointer type to a nonpointer type.
Is there a way to make both VeriFast and the compiler happy(without globally turning off the -Werror flag) in this situation?

[Bart Jacobs]

What you really want is a ghost parameter. VeriFast does not have ghost parameters, but it supports a "ghost parameter pattern", which uses the exists predicate defined in prelude.h:

void foo()
    //@ requires exists<void *>(?p) &*& ...;
    //@ ensures ...;
{
    //@ open exists(_);
    ...
}

At a call site:

    ...
    //@ void *myptr = ...;
    //@ close exists(myptr);
    foo();
    ...

The definition of exists is as follows:

predicate exists<t>(t x;) = true;

--
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 post to this group, send email to veri...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/49acb03c-9d6a-4ce6-a791-6adccd813387%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm for more information.

[Arseniy Zaostrovnykh]

Ghost parameters may do, but I want them to be real. Because these parameters make sense semantically even without verification in mind, and in a future implementation I may want to use them.

[Bart Jacobs]

Hi Arseniy,

Sorry for the super-late reply, but VeriFast does support casting a pointer to uintptr_t.

Best regards,

Bart

[arseniy.za...@dslab.org]

It works, thanks!