Pragma Refined_Depends - GNAT Reference Manual

Next: Pragma Refined_Global, Previous: Pragma Ravenscar, Up: Implementation Defined Pragmas

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