Pointer to stack variable considered possibly null

[Mark Tuttle]

I notice that verifast (vfide) cannot verify

  void test()

  //@ requires true;

  //@ ensures true;

  {

    int i = 42;

    int *ptr = &i;

    assert(ptr != 0);

  }

because it cannot prove `!(i_addr = 0)` but it can verify 

  void test()

  //@ requires true;

  //@ ensures true;

  {

    int i = 42;

    int *ptr = &i;

    //@ assume(ptr != 0);

    assert(ptr != 0);

  }

Famous last words, but it seems obvious that &i is nonnull.  Is it necessary always to tell verifast that a pointer to a stack variable is nonnull?  What should I read to learn more about the memory model? (I've read the tutorial.)

Thanks!

Mark

[bart....@cs.kuleuven.be]

Hi Mark,

At the moment, you need to call the integer_limits lemma declared in prelude.h. So, before the assert, insert

//@ integer_limits(ptr);

At the moment, VeriFast's memory model is simply that memory is a flat array of bytes, and pointers are simply indices into that array. This is not sound with respect to the static analyses that C compilers do (such as provenance-based alias analysis and type-based alias analysis), however; we plan to fix this eventually.

Best,

Bart

[Mark Tuttle]

I see.  Thanks.  This was a simplification of my real example where the type is actually size_t and not int.   I will replicate your integer predicate and integer_limits lemma for size_t and see how that goes.  Thanks again!  -Mark

[Bart Jacobs]

In that case, you'll need integer__limits, which was missing. I just added it.

--
You received this message because you are subscribed to a topic in the Google Groups "VeriFast" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/verifast/qOMS0ui2_vo/unsubscribe.
To unsubscribe from this group and all its topics, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/37bc031c-819b-4195-9080-96e854c07dbcn%40googlegroups.com.