properties Data_Model::Data_Representation => Struct; end A_Struct2; data implementation A_Struct2.impl subcomponents f1 : data c2 : data Base_Types::Character; end A_Struct2.impl; data A_Union2 properties Data_Model::Data_Representation => end A_Union2; data implementation A_Union2.impl subcomponents f1 : data Base_Types::Float; c2 : data Base_Types::Character; end A_Union2.impl; data An_Enum properties Data_Model::Data_Representation => Enum; Data_Model::Enumerators => ("foo", "bar"); Data_Model::Representation => ("00", "11"); end An_Enum; end Base_Types::Example_Types; Important Note About Types in AGREE Currently all bit-sized integer and unsigned types are approximated by unbound integers in AGREE. Similarly, all floating point numbers are approximated by rational numbers. This is due to the representation used by the underlying jkind solver. This means that AGREE results are not guaranteed to be sound with respect to system implementations that use bit-level representations. We expect that future versions of jkind will support bit-level integers, as these are widely supported by solvers. On the other hand, floating point solvers are currently immature, so it is likely that reals will be used for the forseeable future. If exact floating point behavior (including rounding and truncation) are important to your verification problem, AGREE may provide incorrect answers.
properties Data_Model::Data_Representation => Struct; end A_Struct2; data implementation A_Struct2.impl subcomponents f1 : data c2 : data Base_Types::Character; end A_Struct2.impl; data A_Union2 properties Data_Model::Data_Representation => end A_Union2; data implementation A_Union2.impl subcomponents f1 : data Base_Types::Float; c2 : data Base_Types::Character; end A_Union2.impl; data An_Enum properties Data_Model::Data_Representation => Enum; Data_Model::Enumerators => ("foo", "bar"); Data_Model::Representation => ("00", "11"); end An_Enum; end Base_Types::Example_Types; Important Note About Types in AGREE Currently all bit-sized integer and unsigned types are approximated by unbound integers in AGREE. Similarly, all floating point numbers are approximated by rational numbers. This is due to the representation used by the underlying jkind solver. This means that AGREE results are not guaranteed to be sound with respect to system implementations that use bit-level representations. We expect that future versions of jkind will support bit-level integers, as these are widely supported by solvers. On the other hand, floating point solvers are currently immature, so it is likely that reals will be used for the forseeable future. If exact floating point behavior (including rounding and truncation) are important to your verification problem, AGREE may provide incorrect answers.