loonwerks / AGREE

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

AGREE ConstStatement and EqStatement Recursive Validation Check Required #131

Open aaurandt opened 1 year ago

aaurandt commented 1 year ago

Currently a cyclic expression is checked by performing the following (lines 1856-1865 specifically):

https://github.com/loonwerks/AGREE/blob/8d101f31460c3f539bb06d6ed123fdcb4226ee96/com.rockwellcollins.atc.agree/src/com/rockwellcollins/atc/agree/validation/AgreeValidator.java#L1846-L1873

The ExprCycleVisitor just goes down the AST, but it does not search for recursive loops. For example, the following code should produce an error, but it does not:

package TestPackage
public

system sys
    annex agree {**
        eq test1 : int = test2 + 10;
        eq test2 : int = test1 - 10;
    **};
end sys;

end TestPackage;