search

loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
12 stars 5 forks source link

ClassCastException scoping DoubleDotRef #96

Closed kfhoech closed 2 years ago

kfhoech commented 2 years ago

In com.rockwellcollins.atc.agree.scoping.AgreeScopeProvider#scope_DoubltDotRef_elm(DoubleDotRef, EReference) the container of ctx may not be an instance of com.rockwellcollins.atc.agree,agree.GetPropertyExpr resulting in a Java ClassCastException.

This occurs with constructs like the following at the very least and likely other cases as well.

eq n : int;

node nd1 (n : int) returns (r : int);
let
    r = n + 1;
tel;

property P002 = nd1(n) > n;