Changes between Version 51 and Version 52 of IR

Timestamp:

11/24/15 18:49:13 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -116 +116 @@
 {{{
 // type definitions
-Type S:=Tuple[Array[Integer]];
-_dynamic_S: Dytype;
+\type S=Tuple[Array[Integer]];
 
 // variable decls
 n: Integer;
-_S_init: S;
+S_d: Dytype[S];
 x1: S;
 x2: S;
@@ -127 +126 @@
 // statements (leaving out the chooses and whens for brevity)
 n:=10;
-_dynamic_S:=\dtype(Tuple[Array[Integer, n]]);
-x1:=\new(_dynamic_S);
+S_d:=\dytype(Tuple[Array[Integer, n]]);
+x1:=\new(S_d);
 n:=20;
-x2:=\new(_dynamic_S);
+x2:=\new(S_d);
 }}}
 
@@ -148 +147 @@
 == Expressions ==
 
-In the following list of expressions, `e`, `e0`, `e1`, etc., are expressions.  `T` is a type name. `t` is an expression of type `Type`.
+In the following list of expressions, `e`, `e0`, `e1`, etc., are expressions.  `T` is a type name. `t` is an expression of type `Dytype`.
 
 * literals
@@ -164 +163 @@
  * `NULL` : value of type `void*`
 * variables
-* `\sizeof_type(T)` : the size of the named type
+* `\sizeof_type(t)` : the size of the dynamic type t
 * `\sizeof(e)` : the size of the value of expression `e`
-* `\new(T)` : initial value of the named type
+* `\new(t)` : new (default) value of specified dynamic type
 * `\defined(e)` : is `e` defined? Type is `Bool`
 * `\has_next(dom, i, j, k, …)`: an expression of boolean type, testing if the domain `dom` contains any element after `(i, j, k, ...)`
@@ -200 +199 @@
  * `\mem_union(mem1, mem2)`, where `mem1` and `mem2` are expressions of type `Memory`.  This is the union of the two sets. 
  * **could we use Frama-C notation `p+(e1..e2)` for example?**
- * **are there conversions between pointers and mems?**
 
 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)))`.
@@ -216 +214 @@
  * `e:=\allocate(h,t,e);`, where 
   * `h` as type `Heap`
-  * `t` has type `Type`
+  * `t` has type `Dytype`
   * `e` has integer type.
  * Allocates `e` objects of type `t` on heap `h`