Handling of arguments of array type incomplete
Closed this issue · 0 comments
kfhoech commented
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.