Changes between Version 87 and Version 88 of IR2
- Timestamp:
- 05/12/21 09:11:56 (5 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
IR2
v87 v88 54 54 function-definition: type-param-list? qualifier* type-specifier declarator contract-clause* block ; 55 55 qualifier: 56 '$input' /* input variable; only for global decls */ 57 | '$output' /* output variable; only for global decls */ 58 | '$abstract_f' /* abstract function; only for function decls */ 56 '$abstract_f' /* abstract function; only for function decls */ 59 57 | '$pure_f' /* function is a mathematical function of its parameters */ 60 58 | '$state_f' /* function is a mathematical function of the state */ … … 90 88 * `$state_f` can be applied to a system function or defined function only. It declares that the function has no side-effects, and the value returned is a mathematical function of the state in which the call occurred; i.e., the value returned may depend on the arguments in the call, the values of global variables, or any other component of the state. But, if called twice from the same state, it will always return the same value. If the function does not actually have this property, the behavior is undefined. Any `$pure_f` function is necessarily a `$state_f`, so at most one of these two qualifiers can occur in a declaration or definition. 91 89 * Contract clauses can occur only with system functions and defined functions (not with abstract functions, not with variables). 92 * A program must contain a function definition for a function named `main`. 93 * `$input` and `$output` can be used only on global variable declarations (not on function definitions, not in block scope). 90 * A program must contain a function definition for a function named `main`. (Signature?) 94 91 * The `expr` in a guard must have type `$bool`. 95 92
