| | 30 | |
| | 31 | == Pointers & Alias == |
| | 32 | Pointers can be asserted as valid pointers via using ACSL constructor `\valid`. ACSL allows programmers specify a set of valid |
| | 33 | pointers which requires CIVL to be able to represent a `set`. |
| | 34 | |
| | 35 | CIVL has a typing rule: {{{ pointer PLUS CIVL_Range ==> An array of pointers }}}. Other sets of different types may have the similar typing rule. |
| | 36 | |
| | 37 | For CIVL, coping with a `\valid` expression is tricky. For `\valid` expressions appear in assurances, one can implement the evaluation semantics |
| | 38 | on a specific state. However, `\valid` appears in requirements brings problems, it heavily affects how CIVL constructs an initial state. |
| | 39 | |
| | 40 | For example: |
| | 41 | {{{ |
| | 42 | |
| | 43 | |
| | 44 | }}} |
