Proof obligation exception when assigning to a record's sequence by index

[ghost]

Description

The following exception is generated when attempting to generate the proof obligations for an operation that assigns a value to a record's sequence: org.overture.pog.utility.POException: Cannot invoke "org.overture.ast.intf.lex.ILexNameToken.clone()" because the return value of "org.overture.ast.statements.AFieldStateDesignator.getObjectfield()" is null.

Steps to Reproduce

Example VDM-SL:

module TestPO
definitions

types
    Record ::
        myMember: seq of nat
    ;

state myState of
    myRecord: Record

    init s == s = mk_myState(mk_Record([0]))
end;

operations
    assign() == (
        myRecord.myMember(1) := 1;
    );
end TestPO

Expected behavior: The proof obligations to be generated.

Actual behavior: Fails with exception org.overture.pog.utility.POException: Cannot invoke "org.overture.ast.intf.lex.ILexNameToken.clone()" because the return value of "org.overture.ast.statements.AFieldStateDesignator.getObjectfield()" is null

Reproduces how often: Every time

Versions

Tested on versions 3.0.2 and 2.7.4. (Tested on Linux)

Additional Information

This may also effect other compound types, however I have only seen this issue for sequences.

[nickbattle]

Thanks for reporting this. I'm able to reproduce it from your example. It looks like it's something that would work in VDM++ but not VDM-SL. I'm testing the fix now.

[nickbattle]

Fix now available in ncb/development.