Name Analysis Reference Manual
 
The name analysis testing module is instantiated by
$/Name/SGProof.gnrc +instance=NAME +referto=IDENT :inst
The instance parameter must have the same value as that
of the instantiation of the ScopeGraphs module under test, and
the referto parameter must give the name of the
grammar symbol for identifiers.
Several instantiations may be used together in order to simultaneously
test the bindings in a collection of instantiations of the ScopeGraphs
module.
Without further specification, this module augments the ScopeGraphs
module so that the generated processor produces messages of the form:
"file1", line 2:22 NOTE: i ("file2", line 3:7)
One message is written to the standard error file for each
applied occurrence i
(see Applied Occurrences).
The first coordinate specifies the location of the applied occurrence,
the second specifies the location of the corresponding defining occurrence.
No message is output for unbound identifier occurrences.
The SGProof module provides one computational role,
*ProofAppliedOcc, that is automatically inherited by any symbol
inheriting any of the applied occurrence roles
(see Applied Occurrences).
It provides five attributes:
Sym
- is an integer-valued attribute specifying the identifier.
This attribute is usually set by a computation associated with the symbol
that inherits
*ProofAppliedOcc.
*Key
- is a
DefTableKey-valued attribute representing
the key of the corresponding defining occurrence.
This attribute is usually set by a computation associated with the symbol
that inherits *ProofAppliedOcc.
*NoteKey
- is a
DefTableKey-valued attribute representing the defining
occurrence whose coordinates are to be printed in the note.
This synthesized attribute is set to the value of the *Key
attribute by a module computation.
*msg
- is a
VOID attribute that is the post-condition for the computation
printing the note.
*doProof
- is an integer-valued attribute that controls the output of the note.
This attribute is set to 1 (print the note) by a module computation.
If the *Key attribute of the symbol inheriting
*ProofAppliedOcc does not represent the defining occurrence
corresponding to this applied occurrence, use a developer computation to
set the *NoteKey attribute to the correct key value.
The computation whose postcondition is the *msg attribute
is carried out if the value of the *doProof attribute is 1, and
is ignored if the value of the *doProof attribute is 0.
Override the computation of *msg to modify the output format or
change the precondition for printing the note.
Any symbol can inherit the ProofAppliedOcc role, provided that the
developer ensures that the Sym and *Key attributes have
appropriate values.
If the values are irrelevant for the particular symbol, set the Sym
attribute to NoIdn and the *Key attribute to NoKey.
|
