A construct in an AGREE annex containing an array as a parameter to a node results in a Java ClassCastException. For example, the AGREE annex code below triggers the exception.
eq ar : int[1,3][3] = [| 1, 2, 3 |];
node nd(x : int[1,3][3]) returns (r : int);
let
r = x[1] + x [2] + x[3];
tel;
property P001 = nd(ar) > 0;
It appears that in com.rockwellcollins.atc.agree.analysis.lustre.visitors.RenamingVisitor#argToString(Arg) does not consider the case where the arg parameter may be an array rather than a primitive or named type. Since arrays are unnamed, this triggers the ClassCastException. The likely solution here is to add an else if branch to handle the case where the arg is an array. But there may be more places where this omission crops up.
This issue was discovered while working on issue #49.
A construct in an AGREE annex containing an array as a parameter to a node results in a Java ClassCastException. For example, the AGREE annex code below triggers the exception.
It appears that in com.rockwellcollins.atc.agree.analysis.lustre.visitors.RenamingVisitor#argToString(Arg) does not consider the case where the
argparameter may be an array rather than a primitive or named type. Since arrays are unnamed, this triggers the ClassCastException. The likely solution here is to add anelse ifbranch to handle the case where the arg is an array. But there may be more places where this omission crops up.This issue was discovered while working on issue #49.