-
Piotr Trojanek authored
Invariant procedure bodies are created either by expansion of freezing nodes (but only in ordinary compilation mode) or at the end of package private declarations (but not for with private types in the type derivation chain). In GNATprove mode we didn't create invariant procedure bodies in lightweight expansion, so we didn't create them at all when there were private types in the type derivation chain. This patch copies the relevant freezing part from ordinary to lightweight expansion. This obviously involves code duplication, but it seems better to duplicate whole sections that work properly instead of small pieces that are incomplete. There are other pieces of freezing that are similarly duplicated, so this patch doesn't make the code substantially worse. gcc/ada/ * exp_spark.adb (SPARK_Freeze_Type): Copy whole handling of DIC and Type_Invariant from Freeze_Type.
Piotr Trojanek authoredInvariant procedure bodies are created either by expansion of freezing nodes (but only in ordinary compilation mode) or at the end of package private declarations (but not for with private types in the type derivation chain). In GNATprove mode we didn't create invariant procedure bodies in lightweight expansion, so we didn't create them at all when there were private types in the type derivation chain. This patch copies the relevant freezing part from ordinary to lightweight expansion. This obviously involves code duplication, but it seems better to duplicate whole sections that work properly instead of small pieces that are incomplete. There are other pieces of freezing that are similarly duplicated, so this patch doesn't make the code substantially worse. gcc/ada/ * exp_spark.adb (SPARK_Freeze_Type): Copy whole handling of DIC and Type_Invariant from Freeze_Type.