Accessing struct in struct produces internal error

[DrSkunk]

The following code give the error: "Verification failed due to an internal error. See the console window for details."

struct xARP_HEADER
{
    int usHardwareType;
};

struct xARP_PACKET
{
    struct xARP_HEADER xARPHeader;
};

void main( struct xARP_PACKET * pxARPFrame )
//@ requires xARP_PACKET_xARPHeader(pxARPFrame, _);
//@ ensures true;
{}

Entry in console:

VeriFast internal error:
File "verifast1.ml", line 301, characters 23-29: Assertion failed

When struct xARP_HEADER xARPHeader; is changed to struct xARP_HEADER * xARPHeader; the verification goes through.

Tested with Verifast 15.11

[btj]

You should mention each leaf field separately. This works:

struct xARP_HEADER
{
    int usHardwareType;
};

struct xARP_PACKET
{
    struct xARP_HEADER xARPHeader;
};

void main( struct xARP_PACKET * pxARPFrame )
//@ requires pxARPFrame->xARPHeader.usHardwareType |-> _;
//@ ensures true;
{}