Changes between Version 26 and Version 27 of IR2

Timestamp:

04/28/21 10:19:50 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -4 +4 @@
 
 * CIVL-IR is a subset of CIVL-C.  A CIVL-IR program is a CIVL-C program, and has the same semantics.
+
+Questions
+* how to allocate an array
+* how to initialize a variable (what are initial values?)
+* how to go between sequences and arrays
+* can you make types values? (reification)
+* pure functions?  A pure function is a mathematical function of its arguments.  It cannot modify the state.
+* state functions? A state function is a function of the current state (including arguments, global variables, ...).  It cannot modify the state.  Every pure function is a state function.
+* declarators need parentheses
+* `$depends_on`
+* read/write sets: function calls to start, stop monitoring reads/writes?  All part of mem library
+* function calls for atomic enter/exit
+* a type for $state ? 
+
 
 === Grammar ===
@@ -42 +56 @@
 * a `$system` function has no definition in CIVL-IR, but is instead defined elsewhere (for example, in C or Java code).  Such a function will always be executed atomically.   The first string specifies a path (e.g., Java package) to the library containing the function, the second is the name of the library.    These two Strings should be enough to tell CIVL where to find the system definition of the function.
 * the `expr` in a guard must have type `$bool`
+* add statement `$new`: 
 
+{{{
+  int a[];
+  void main() {
+    a = (int[10])$lambda(int i; $undefined);
+    a = $new(int[10]); // 
+    ... initialized a somehow ...
+   $assume($defined(a, 0, 10)); // ?
+}}}
 
 === Types ===
@@ -81 +104 @@
 * The difference between the function type and map type: a function is really a procedure in the language, so it can modify the state as well as return a value.    This is like the C notion of "function".   A map is a logical partial function: it is defined on some subset of the domain type, it will always "return" the same value on a given input, and reading it cannot modify the state.
 
-Questions
-* how to allocate an array
-* how to initialize a variable (what are initial values?)
-* how to go between sequences and arrays
-* can you make types values? (reification)
+
 
 === Statements ===