This project is read-only.

Termination checking and block contracts - VCC error?

Jan 9, 2014 at 8:21 PM
Edited Jan 10, 2014 at 2:03 AM
Hi all. I am getting a VCC error when I have a termination-checked code with a block within it whose contract mentions \wrapped
#include <vcc.h>
#include <stdlib.h> //malloc

typedef struct MyObject
{
    int field;
} MyObject;

void VCCError_TerminationChecking_Wrapped()
    _(decreases 0)
{
    size_t size = 3;
    MyObject* arr = malloc(sizeof(MyObject) * size);
    if (arr != NULL)
    {
        _(wrap arr+0)
        _(wrap arr+1)
        _(wrap arr+2)

        _(decreases 0)  //with or without this, same error
        _(requires \forall size_t j; j < size ==> \wrapped(arr+j))
        {
            _(unwrap arr+0)
            //anything here
        }
    }
}
The error:
error VC9600: OOPS: unhandled expr {
  if (@check_termination(2))
    {
      uint64_t j#1;
      if (<(j#1, size))
        {
          _Bool stmtexpr0#22;
          stmtexpr0#22 := @_vcc_wrapped(@state, arr[j#1]);
        }
      else
        skip;
      assume false;
    }
  else
    skip;
  forall(uint64_t j; @in_range_u8(j); ==>(<(j, size), @skip_termination_check(pure(@_vcc_wrapped(@state, arr[j])))))}

Verification errors in 2 function(s)
Exiting with 3 (1 error(s).)
Is this a problem on my end or something in VCC? I can't find any similar examples in the documentation/testsuite.

For the time-being I can disable termination checking for my own work... I was just hoping to have the termination warnings for ghost loops in my code go away and that is when I found this issue.

Also, I notice that replacing my block _(requires ...) contract above with _(requires \full_context()) causes this VCC output: "confused, will now die
Exiting with 3 (1 error(s).)"

This simpler example also causes "confused, will now die":
void VCCError_TerminationChecking_Wrapped_Obj()
    _(decreases 0)
{
    MyObject obj;
    _(wrap &obj)

    _(decreases 0)
    _(requires \wrapped(&obj))
    //_(requires \full_context())
    {
        _(unwrap &obj)
            //anything
    }
}