Changes between Version 114 and Version 115 of IR2

Timestamp:

06/03/21 22:36:30 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -130 +130 @@
   | '$heap'  /* heap type, for dynamic allocation */
   | '$mem'  /* set of memory locations */
+  | '$type' '<' type-name '>'  /* a value type of a named static type */
   | 'struct' ID  type-param-list?  /* structure type */
   | 'union' ID  type-param-list?  /* union type */
@@ -252 +253 @@
   | '&' lvalue  /* address-of */
   | expr type-args? '(' expression-list? ')'  /* application of abstract function (and perhaps other functions?) */
-  | '$fresh' '(' allocator ')'  /* returns a new arbitrary value of the given type */
-  | '$new' '(' allocator ')'  /* returns a new arbitrary and undefined value of the given type */
+  | '$typeof' '(' type-name ')'  /* value type named by the extended type name */
+  | '$fresh' '(' expr ')'  /* returns a new arbitrary value of the given type */
+  | '$new' '(' expr ')'  /* returns a new arbitrary and undefined value of the given complete type */
   | '$forall' '(' decl expr? ')' expr  /* universal quantification */
   | '$exists' '(' decl expr? ')' expr  /* existential quantification */
@@ -292 +294 @@
   * 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.
 
 === How to implement `$defined` using symbolic execution ===