Panic: Failure("Not of correct form (unlikely case - i's not matching)")

[yav]

The following program causes a crash:

void even_odd(unsigned long size, int *p)
/*@
requires
  take a1 = each(u64 i; i < size) { Owned<int>(array_shift<int>(p,i)) };
ensures
  take a2 = each(u64 i; i < size) { Owned<int>(array_shift<int>(p,i)) };
@*/
{
}

The error is

cn: internal error, uncaught exception:
    Failure("Not of correct form (unlikely case - i's not matching)")

Commit: 53c1e48

[ZippeyKeys12]

Both this and #6 are from the executable spec requiring the permission for an each to be <term> <op> <index> && ..., where index is the variable the each is quantified over and op is either < or <=. This inequality must also be the leftmost operand of &&s.

This error is because size is a variable, so it mostly matches the pattern, except size is not i.

The error in #6 is because you used a cast, so it doesn't match the pattern.

The test generation itself also has a similar restriction, that there is an upper bound, but it is not syntactic and so more general. It isn't reachable though, since the executable spec will always fail first.

[yav]

Moved to rems-project#689 in main repo