Changes between Version 115 and Version 116 of IR2

Timestamp:

06/04/21 08:41:56 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -166 +166 @@
   * Arrays are mutable.   As in C, the left hand size of an assignment may have the form `a[i]`, where `a` is an object of array type.  Sequences are immutable.
   * Elements of an array are addressable, i.e., one can form a pointer such as `&a[i]`.  This is not possible with sequences, sets, maps, or relations---there is no way to have a pointer to any component of such a type.
-  * A function may neither consume nor return an object of array type.  There is no such restriction for sequences.  
+  * A function may neither consume nor return an object of array type. [why?] There is no such restriction for sequences.  
 * The difference between the function type and map type:
-  * a function cannot return a function; nor can a function consume an argument of functional type
+  * a function cannot return a function; nor can a function consume an argument of functional type [why?]
   * a function may return a pointer to a function and may consume an argument of type pointer to function...
   * a function pointer is formed by `&f`, where `f` is the name of a function
@@ -185 +185 @@
 };
 }}}
-* A *pure type name* is one in which the optional length expression for an array type never occurs.
-* A *complete type name* is defined recursively as follows: a struct or union type is complete if and only if all the member types are complete; an array type is complete if and only if the element type is complete and the length is specified; all other types are complete.
+* A **pure type name** is one in which the optional length expression for an array type never occurs.  Type arguments in angular brackets must be pure types.  Declarations are pure types by the grammar.
+* A **complete type name** is defined recursively as follows: a struct or union type is complete if and only if all the member types are complete; an array type is complete if and only if the element type is complete and the length is specified; all other types are complete.
 
 
@@ -213 +213 @@
 
 * For function calls and spawns, the first expression shall have a functional type.   That function must be a system or defined function (not an abstract function).
-* The first expression following `$alloc` has type `$heap*`.  It is a pointer to the heap that will be modified by allocating the new memory.  The second expression has type `$int` and is the number of elements being allocated.    This is followed by the element type.    The function returns a pointer to the first element of an array, similar to C's malloc.    It is deallocated using function`$free`.
 
 
@@ -294 +293 @@
   * A pointer becomes defined when assigned the result of an `$alloc`.   Each element in the newly allocated object is undefined.
   * Example: to determine whether it is safe to read `*(p+i)`, assert `$summable(p, i) && $valid(p+i) && $defined(*(p+i))`.  You must check (1) you can sum `p` and `i`, (2) `p+i` points to an object of the base type, so dereference is safe, and (3) the object is defined (has been assigned a value).  If you aren't sure `p` and `i` have been defined, you can add `$defined(p) && $defined(i)` to the assertion.   It may be more efficient to use temporary variables and break this up into multiple assertions.
-  * `$fresh` and `$new` consume an argument of type `$type<T>` and return a value of type `T`.  For `$new`, the argument must specify a complete type.
+  * `$fresh` and `$new` consume an argument of type `$type<T>` and return a value of type `T`.  For `$new`, the argument must specify a complete type.  Fresh accepts any type name.
+
 
 === How to implement `$defined` using symbolic execution ===