Changes between Version 25 and Version 26 of IR
- Timestamp:
- 11/22/15 20:39:32 (10 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
IR
v25 v26 56 56 The types are: 57 57 58 * `$ dytype` : dynamic type: a value of this type represents a "dynamic type", a type which is created at runtime. For example when the type name `int[n]` is evaluated, the result is a value of type `$dytype`.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 59 * `$bool` : boolean type, values are `$true` and `$false` 60 60 * `$proc` : process type … … 91 91 Type names: 92 92 93 A type name is a syntactic element that names a type, together with possibly more information that makes the type "complete". All of the names listed above are type names, such as `int[]`, but so is `int[n*m]`. 94 95 The expression `$ dytypeof(typeName)` takes a type name and returns a value of type `$dytype` representing that type.96 97 The expression `$init _val(d)` takes a `$dytype` value `d` and returns the initial value for an object of type `d`.93 A type name is a syntactic element that names a type, together with possibly more information that makes the type "complete". All of the names listed above are type names, such as `int[]`, but so is `int[n*m]`. This is the same as in C. 94 95 The expression `$typeof(T)`, where `T` is a type name, returns a value of type `$type` representing the type `T`. 96 97 The expression `$initval(d)` takes a `$type` value `d` and returns the initial value for an object of type `d`. 98 98 99 99 Example: … … 104 104 // variable decls 105 105 int n; 106 $ dytype _S;106 $type _S; 107 107 struct S x1; 108 108 struct S x2; … … 110 110 // statements (leaving out the chooses and whens for brevity) 111 111 n=10; 112 _S=$ dytypeof(struct S { int a[n]; };113 x1=$init _val(_S);112 _S=$typeof(struct S { int a[n]; }; 113 x1=$initval(_S); 114 114 n=20; 115 x2=$init _val(_S);115 x2=$initval(_S); 116 116 }}} 117 117 … … 172 172 * `NULL` : value of type `void*` 173 173 * variables 174 * `$dytypeof(T)` : an expression of type `$dytype` 175 * `$init_val(e)`, where `e1` is an expression of type `$dytype` 174 * `$typeof(T)` : an expression of type `$type` 175 * `sizeof(T)` : the size of the type named `T` 176 * `$initval(e)`, where `e` is an expression of type `$type` 176 177 * `$defined(e)` 177 178 * `e1+e2` : addition … … 194 195 * `$forall`, `$exists` 195 196 * `e1.i`, some natural number i (tuple read) 196 * `sizeof(T)` : T is a type name?197 197 * `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans 198 198 * **MemoryUnitExpressions?**: are these literal values of type `$mem`? … … 244 244 245 245 == Libraries == 246
