search

loonwerks / AGREE

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

AGREE ArgType Validator Check Not Catching Wrong Syntax #128

Open aaurandt opened 1 year ago

aaurandt commented 1 year ago

Validator check in question: https://github.com/loonwerks/AGREE/blob/d412a065da678a2018766210cf3254fc2c0db1db/com.rockwellcollins.atc.agree/src/com/rockwellcollins/atc/agree/validation/AgreeValidator.java#L483-L493

This error should be raised with the following code, but it is not:

package AwfulExtension
public
    with Base_Types;

    data AwfulType extends Base_Types::Boolean
    end AwfulType;

    data implementation AwfulType.impl
        subcomponents
            ugly : data Base_Types::Boolean;
    end AwfulType.impl;

    system Top
        features
            inp : in data port AwfulType.impl;
            outp : out data port AwfulType.impl;
        annex agree {**
            eq x : AwfulType.impl;
            guarantee G01 "Rule" : outp = inp;
        **};
    end Top;

end AwfulExtension;