Changes between Version 111 and Version 112 of IR2

Timestamp:

05/28/21 14:19:15 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -17 +17 @@
 
 1. **Do variables have default initial values?**
-  * An object variable may or may not include an explicit initializer.   If it does not include an initializer, the variable is "undefined".  Even in this case, the variable has some unspecified value of its type.   Details are below.
+  * An object variable may or may not include an explicit initializer.   If it does not include an initializer, it is the same as if the initializer were `$new(T)`, where `T` is the type of the variable.  Even in this case, the variable has some unspecified value of its type.   Details are below.
 1. **How do you initialize a variable?**
-  * In the declaration.   For example `$int n=$new($int);` will assign `n` an arbitrary integer, while `$int n=0;` will assign the integer `0` to `n`.
+  * In the declaration.   For example `$int n=$fresh($int);` will initialize `n` with an arbitrary integer, while `$int n=$new($int);` will initialize `n` with an undefined integer, and `$int n=0` will initialize `n` with `0`.
 1. **How is an array allocated?**
-  * An array variable `a` is declared with a decl such as `T a[] = $new_array(n, T);` which assigns to `a` a new array value for an array of length `n` of elements of type `T` in which all entries are undefined.   (Alternatively, `T a[] = $new(T[n])` will create an array of arbitrary defined values.)  For heap-allocation, `T * p = $undef;` followed by the statement `p = $alloc<T>(&heap, n);` will add a new object to the heap and return a pointer to the first element.  An `$alloc`-ed object can be deallocated with `$free(p);`.
+  * An array variable `a` is declared with a decl such as `T a[] = $new(T[n]);` which assigns to `a` a new array value for an array of length `n` of elements of type `T` in which all entries are undefined.   (Alternatively, `T a[] = $fresh(T[n])` will create an array of arbitrary defined values.)
 1. **Is there an "array-pointer pun", as in C?**
   * No, if you want a pointer to element 0 of an array, you have to explicitly write something like `&a[0]`.
@@ -251 +251 @@
   | '&' lvalue  /* address-of */
   | expr type-args? '(' expression-list? ')'  /* application of abstract function (and perhaps other functions?) */
-  | '$new' '(' type-name ')'  /* returns a new arbitrary value of the given type */
-  | '$new_array' '(' expr ',' type-name ')'  /* allocation of array of undefined values*/
+  | '$fresh' '(' allocator ')'  /* returns a new arbitrary value of the given type */
+  | '$new' '(' allocator ')'  /* returns a new arbitrary and undefined value of the given type */
   | '$forall' '(' decl expr? ')' expr  /* universal quantification */
   | '$exists' '(' decl expr? ')' expr  /* existential quantification */