| | 36 | |
| | 37 | Notes |
| | 38 | * a program must contain a function definition for a function named `main` |
| | 39 | * `$input` and `$output` can be used only on global variable declarations (not on function definitions, not in block scope) |
| | 40 | * `$abstract` can be used only in a declaration of a variable of function type. The function becomes a new uninterpreted function. |
| | 41 | * `$atomic_f` indicates that a defined function is to behave atomically, i.e., every call to such a function will behave as if the call occurred in an `$atomic` block. |
| | 42 | * a `$system` function has no definition in CIVL-IR, but is instead defined elsewhere (for example, in C or Java code). Such a function will always be executed atomically. The first string specifies a path (e.g., Java package) to the library containing the function, the second is the name of the library. These two Strings should be enough to tell CIVL where to find the system definition of the function. |
| | 43 | * the `expr` in a guard must have type `$bool` |
| | 44 | |
