Skip to content

Commit

Permalink
Rework initial_env of contract pragmas.
Browse files Browse the repository at this point in the history
This makes sure there is parent-children relation between the pragma node
and the type or subprogram it is associated with, to make it easier to
know whether we are inside such a contract.
  • Loading branch information
Roldak committed Oct 27, 2023
1 parent d224456 commit 3c459e5
Showing 1 changed file with 17 additions and 22 deletions.
39 changes: 17 additions & 22 deletions ada/ast.py
Original file line number Diff line number Diff line change
Expand Up @@ -10156,26 +10156,6 @@ def is_ghost_code():
'Assert', 'Assert_And_Cut', 'Assume', 'Loop_Invariant'
)

@langkit_property()
def xref_initial_env():
"""
Contract pragmas such as ``Precondition`` have full visibility on their
associated subprogram's formals although they are not in an internal
scope. We handle that by overriding this ``xref_initial_env`` property
which will make sure that name resolution uses the env returned by this
property when constructing xref_equations.
"""
return If(
Entity.id.name_symbol.any_of(
"Pre", "Post", "Pre'Class", "Post'Class",
"Precondition", "Postcondition",
"Precondition'Class", "Postcondition'Class",
"Test_Case", "Contract_Cases", "Predicate"
),
Entity.associated_entities.at(0).children_env,
Entity.children_env
)

@langkit_property()
def xref_equation():
return Cond(
Expand Down Expand Up @@ -10487,11 +10467,26 @@ def associated_entities():
def initial_env():
"""
Return the initial env name for a pragma clause. We use the
Standard package for top level use clauses.
Standard package for top level use clauses. For contract pragmas such
as ``Precondition`` or ``Predicate``, we use the env of the entity the
pragma is associated with in order to properly resolve references to
formals or to the type's ``SyntheticTypePredicateObjectDecl`` instance.
"""
return If(
return Cond(
Self.parent.parent.is_a(CompilationUnit),
named_env('Standard'),

Self.as_bare_entity.id.name_symbol.any_of(
"Pre", "Post", "Pre'Class", "Post'Class",
"Precondition", "Postcondition",
"Precondition'Class", "Postcondition'Class",
"Test_Case", "Contract_Cases", "Predicate"
),
Self.as_bare_entity.associated_entities.at(0).then(
lambda ent: direct_env(ent.children_env),
default_val=current_env()
),

current_env()
)

Expand Down

0 comments on commit 3c459e5

Please sign in to comment.