This repository has been archived by the owner. It is now read-only.
Generation of type predicates clutters results with trivial obligations #159
Comments
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Generation of AGREE type predicates from AADL range properties always generates a property check even in the case where no such range predicate exists (leaving a trivially true property). This clutters up the results to an onerous degree.
Refactor the generation to omit the trivial properties.
The text was updated successfully, but these errors were encountered: