Pragma Depends (GNAT Reference Manual) (original) (raw)

2.48 Pragma Depends ¶

Syntax:

pragma Depends (DEPENDENCY_RELATION);

DEPENDENCY_RELATION ::= null | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE})

DEPENDENCY_CLAUSE ::= OUTPUT_LIST =>[+] INPUT_LIST | NULL_DEPENDENCY_CLAUSE

NULL_DEPENDENCY_CLAUSE ::= null => INPUT_LIST

OUTPUT_LIST ::= OUTPUT | (OUTPUT {, OUTPUT})

INPUT_LIST ::= null | INPUT | (INPUT {, INPUT})

OUTPUT ::= NAME | FUNCTION_RESULT INPUT ::= NAME

where FUNCTION_RESULT is a function Result attribute_reference

For the semantics of this pragma, see the entry for aspect Depends in the SPARK 2014 Reference Manual, section 6.1.5.