Skip to content
Snippets Groups Projects
  • Piotr Trojanek's avatar
    c6370764
    ada: Build invariant procedure while freezing in GNATprove mode · c6370764
    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.
    c6370764
    History
    ada: Build invariant procedure while freezing in GNATprove mode
    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.