loonwerks / AGREE

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

Spurious type error for on descendants of AADL Boolean #17

Closed kfhoech closed 4 years ago

kfhoech commented 4 years ago

Given the following package:

package Scratch
public
    with Base_Types;

    data bool_data_type extends Base_Types::Boolean
    end bool_data_type;

    data int_data_type extends Base_Types::Integer
    end int_data_type;

    data real_data_type extends Base_Types::Float
    end real_data_type;

    system SystemA
        features
            port1 : in data port bool_data_type;
            port2 : in data port int_data_type;
            port3 : in data port real_data_type;
        annex agree {**
            eq x : int [0, 5];
            eq y : int [10, 15];
            eq zb : bool = (port1 != false);
            eq zi : int = port2;
            eq zr : real = port3;
        **};
    end SystemA;

    system implementation SystemA.impl
        annex agree {**
            assign x = y;
        **};
    end SystemA.impl;

end Scratch;

The AGREE type inference reports an apparently incorrect "error" type for references to port1 with the error message "named thing must be an expression with a type."

Examination of the relevant code for type inference of type descending from the AADL data type Base_Types::Boolean shows that type extensions for Boolean are not considered whereas extensions for Integer and Real are considered.

kfhoech commented 4 years ago

The key omission in the type inference appears to be in com.rockwellcollins.atc.agree.AgreeTypeSystem at approximately line 260ff. There the type inference looks for extensions of the family of types that map to the AGREE int type and for extensions of the family of types that map to the AGREE real type. There is no consideration of types that map to the AGREE bool type.

Additionally, means of looking whether the name of the extension contains certain strings is not considering the actual AADL type extended, but merely a heuristic. This is likely to be the source of future bug and it should be fixed too. Consider opening another Issue report for this...

kfhoech commented 4 years ago

Fixed by #18.