Changes between Version 38 and Version 39 of IR
- Timestamp:
- 11/23/15 17:15:11 (10 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
IR
v38 v39 56 56 The types are: 57 57 58 * `$type` : dynamic type. This allows a type to be realized as a value, a value of type `$type`. For example, when the type name `int[n]` is evaluated, the result is a value of type `$type`.59 58 * `$bool` : boolean type, values are `$true` and `$false` 60 59 * `$proc` : process type … … 97 96 A **type name** is a syntactic element that names a (pure or augmented) type Examples include `int[]` and `int[n*m]`. This is the same as in C. 98 97 99 The expression `$typefrom(T)`, where `T` is a type name, returns a value of type `$type` representing the type `T`. 100 101 The expression `$typeof(e)`, where `e` is an expression, returns the type of `e`, a value of type `$type`. 102 103 The expression `$initval(d)` takes a `$type` value `d` and returns the initial value for an object of type `d`. The initial value of `$integer` and other primitive (non-compound) types is "undefined". The initial value of `$integer[]` is an array of length 0 of `$integer`. The initial value of `$real*` is the undefined pointer to `$real`. The initial value of `$real[10]` is the array of length 10 in which each element is undefined. In general, the initial value of an array of length n is the sequence of length n in which every element is the initial value of the element type of the array. The initial value of a structure is the tuple in which each component is assigned the initial value for its type. 98 The expression `$initval(T)` takes a type name and returns the initial value for an object of that type. The initial value of `$integer` and other primitive (non-compound) types is "undefined". The initial value of `$integer[]` is an array of length 0 of `$integer`. The initial value of `$real*` is the undefined pointer to `$real`. The initial value of `$real[10]` is the array of length 10 in which each element is undefined. In general, the initial value of an array of length n is the sequence of length n in which every element is the initial value of the element type of the array. The initial value of a structure is the tuple in which each component is assigned the initial value for its type. 104 99 105 100 Example: … … 110 105 // variable decls 111 106 int n; 112 $type _S;107 struct S _S_init; 113 108 struct S x1; 114 109 struct S x2; … … 116 111 // statements (leaving out the chooses and whens for brevity) 117 112 n=10; 118 _S =$typefrom(struct S { int a[n]; };119 x1= $initval(_S);113 _S_init=$initval(struct S { int a[n]; }; 114 x1=_S_init; 120 115 n=20; 121 x2= $initval(_S);116 x2=_S_init; 122 117 }}} 123 118 … … 151 146 * If the system function is called anywhere in the program, it must be defined by providing Java code in an Enabler and Executor. Failure to do so will result in an exception. 152 147 * A system function may modify any memory it can reach. This includes allocating new data on heaps it can reach. 153 * A system function may have an implicit guard. This is specified **how**? 154 * A system function may have an explicit guard. This is specified **how**? 148 * A system function may have a guard. 155 149 156 150 Example of a declaration of a system function with guard. … … 179 173 * `NULL` : value of type `void*` 180 174 * variables 181 * `$typefrom(T)` : an expression of type `$type`, the type represented by the type name `T` 182 * `$typeof(e)` : expression of type `$type`, the type of the expression `e` 183 * `$sizeof(t)` : the size of that type. Note that the C `sizeof(expr)` can be translated as `$sizeof($typeof(expr))`. The C `sizeof(T)` can be translated as `$sizeof($typefrom(T))`. 184 * `$initval(t)` : initial value of type `t` 185 * `$defined(e)` 175 * `$sizeof(T)` : the size of the named type 176 * `$sizeof(e)` : the size of the value of expression `e` 177 * `$initval(T)` : initial value of the named type 178 * `$defined(e)` : is `e` defined? Type is `$bool` 186 179 * `$hasNextIn((i, j, k…), dom)`: an expression of boolean type, testing if the domain `dom` contains any element after `(i, j, k, ...)` 187 180 * `e1+e2` : addition. One of the following must hold: … … 198 191 * `!e` : logical not 199 192 * `-e` : negative 200 * `$cast(e,t)` : casts `e` to a value of type `t`193 * (T)e : casts `e` to a value of the named type 201 194 * need to list all of the legal casts and what they mean exactly 202 195 * cast of integer to array-of-boolean, and vice-versa? … … 206 199 * `e1<e2`, `e1<=e2` 207 200 * `e0(e1,...,en)` : pure function call? 208 * `$forall`, `$exists` 201 * `$forall`, `$exists` : **FILL IN** 209 202 * `e1.i`, some natural number i (tuple read) 210 203 * `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans 211 * **Memory UnitExpressions?**: are these literal values of type `$mem`?204 * **Memory set expressions**: are these literal values of type `$mem`? 212 205 * could we use Frama-C notation `p+(e1..e2)` for example? 213 206 * are there conversions between pointers and mems?
