Next: , Previous: Pragma Default_Storage_Pool, Up: Implementation Defined Pragmas


2.46 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.