| 156 | | * `\range(e1,e2,e3)` : value of type `Range` consisting of the integers e1, e1+e3, e1+2*e3, ... that are less than or equal to e2. |
| 157 | | * `\domain(<r1,...,rn>)` : value of type `Domain[n]`, the ordered Cartesian product of the n ranges (dictionary order) |
| 158 | | * `"abc"` : string literals: value of type `Array[Char, n+1]`, where n is the length of the string (the last element is the character `\0`) |
| | 181 | * `\tsel(e1, i)` : tuple selection of component i of e1. i must be a literal natural number. |
| | 182 | * Pointers and Memory |
| | 183 | * `NULL` : value of type `void*` |
| | 184 | * `\deref(e)` : pointer dereference |
| | 185 | * `\addr(e)` : address-of operator |
| | 186 | * `\padd(e1, e2)`: pointer addition. `e1` has pointer type and `e2` has an integer type or range type. If `e2` has integer type the result has pointer type. Otherwise, the result has `Mem` type. |
| | 187 | * `\psub(e1,e2)`: pointer subtraction |
| | 188 | * `\region(ptr)`, where `ptr` is an expression with a pointer type. This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself. |
| | 189 | * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`. This is the union of the two memory sets. |
| | 190 | * `\mem_intersect(mem1, mem1)` : set intersection |
| | 191 | * `\mem_comp(mem1)` : set complement (everything not in `mem1`) |
| | 192 | * Scopes and Processes |
| 161 | | * `NULL` : value of type `void*` |
| 162 | | * variables |
| 163 | | * `\sizeof_type(t)` : the size of the dynamic type t |
| 164 | | * `\sizeof_expr(e)` : the size of the value of expression `e` |
| 165 | | * `\new(t)` : new (default) value of dynamic type t |
| 166 | | * `\defined(e)` : is `e` defined? Type is `Bool` |
| 167 | | * `\has_next(dom, <i, j, …>)`: an expression of boolean type, testing if the domain `dom` contains any element after `<i, j, ...>` |
| 168 | | * `\add(e1, e2)` : numeric addition. |
| 169 | | * `e1` and `e2` have the same numeric type. Note that there are no "automatic conversions" as there are in C. If the original expressions have different types, explicit casts must be inserted. |
| 170 | | * `\padd(e1, e2)`: pointer addition. `e1` has pointer type and `e2` has an integer type or range type. If `e2` has integer type the result has pointer type. Otherwise, the result has `Mem` type. |
| 171 | | * `\sub(e1, e2)` : subtraction |
| 172 | | * `\psub(e1,e2)`: pointer subtraction |
| 173 | | * `\mul(e1, e2)` : multiplication |
| 174 | | * `\div(e1, e2)` : division |
| 175 | | * If both are integer types, the result is integer division. Otherwise it is real division. Need to define what happens for negative integers. |
| 176 | | * `\mod(e1, e2)` : modulus |
| 177 | | * `\asub(e1, e2)` : array subscript expression. Note that `e1` must have array type, not pointer type. (This is different from C.) If `e1` has pointer type, use `\deref(\padd(e1, e2))` instead. |
| 178 | | * `\deref(e)` : pointer dereference |
| 179 | | * `\addr(e)` : address-of operator |
| 180 | | * `\not(e)` : logical not |
| 181 | | * `\neg(e)` : negative |
| 182 | | * `\cast(T, e)` : casts `e` to a value of the named type |
| 183 | | * need to list all of the legal casts and what they mean exactly |
| 184 | | * cast of integer to array-of-boolean, and vice-versa? |
| 185 | | * **Instead of casts would it be better to have explicit functions for each legal kind of cast?** |
| 186 | | * `\eq(e1, e2)`, `\neq(e1, e2)`: equality/inequality test |
| 187 | | * `\and(e1, e2)`, `\or(e1, e2)`: logical and/or operation |
| 188 | | * `\cond(e1, e2, e3)`: conditional expression, equivalent to `e1?e2:e3` in C. |
| 189 | | * `\lt(e1, e2)`, `\lte(e1, e2)`: less than/less than or equal to |
| 190 | | * `e0(e1,...,en)` : a function invocation where `e` must evaluate to an abstract or pure system function |
| 191 | | * `\forall`, `\exists` : `\forall {Integer i | e0} e1`. `\exists` is similar. ** Is this the best notation? ** |
| 192 | | * `\tuple_read(e1, i)`, some natural number i (tuple read) |
| 193 | | * `\bit_and(e1, e2)`, `\bit_or(e1, e2)`, `\bit_xor(e1, e2)`, `\bit_comp(e1)` : bit-wise operations: arguments are arrays of booleans |
| 194 | | * a left-hand-side expression, when used in certain contexts, is automatically converted to `Mem`. The contexts are: arguments to the built-in functions `\access`, `\read`, and `\write` described below, or occurrence in the list of an `\assigns` clause |
| 195 | | * `\array_slice(a, dom)`, where `a` is an expression of array type and `dom` is an expression of `Domain` type. The dimension of the array must match the dimension of the domain. This represents all memory units which are the cells in the array indexed by a tuple in `dom`. |
| 196 | | * `\region(ptr)`, where `ptr` is an expression with a pointer type. This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself. |
| 197 | | * **\mem_reach ?** |
| 198 | | * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`. This is the union of the two sets. |
| 199 | | * **could we use Frama-C notation `p+(e1..e2)` for example?** |
| 200 | | |
| 201 | | Pointers: unlike C, there is no "array-pointer pun". If an array `a` needs to be converted to a pointer, you must use `\address_of(\address_of(\array_subscript(a, 0)))`. |
| | 195 | * Other |
| | 196 | * variables |
| | 197 | * `\sizeof_type(t)` : the size of the dynamic type t; `Integer` type |
| | 198 | * `\sizeof_expr(e)` : the size of the value of expression `e`; `Integer` type |
| | 199 | * `\new(t)` : new (default) value of `Dytype` t |
| | 200 | * `\defined(e)` : is `e` defined? `Bool` type |
| | 201 | * `\cast(e, T)` : casts `e` to a value of the named type |
| | 202 | * need to list all of the legal casts and what they mean exactly |
| | 203 | * cast of integer to array-of-boolean, and vice-versa? |
| | 204 | * **Instead of casts would it be better to have explicit functions for each legal kind of cast?** |
| | 205 | * `\ite(e1, e2, e3)`: if-then-else (conditional) expression, equivalent to `e1?e2:e3` in C. |
| | 206 | * `e0(e1,...,en)` : a function invocation where `e` must evaluate to either an abstract or pure system function |
| | 207 | |
| | 208 | Notes |
| | 209 | * unlike C, there is no "array-pointer pun". If an array `a` needs to be converted to a pointer, you must use \addr(\asub(a, 0))`. |
