Next: , Previous: , Up: Implementation Defined Pragmas   [Contents][Index]


2.146 Pragma Refined_Depends

Syntax:

pragma Refined_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 Refined_Depends in the SPARK 2014 Reference Manual, section 6.1.5.