Skip to content

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

@ghost

Description

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.

Metadata

Metadata

Assignees

Labels

MergableA fix is available on a branch to merge for releasebugIncorrect behaviour of the toollanguageIssues in parser, TC, interpreter, POG or CG

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions