Changes between Version 20 and Version 21 of IR

Timestamp:

11/22/15 11:25:28 (10 years ago)

Author:

siegel

Comment:

--

IR

@@ -60 +60 @@
  * lo, hi are integers, wrap is boolean
  * finite interval of integers [lo,hi].  If `wrap` is true then all operations "wrap", otherwise, any operation resulting in a value outside of the interval results in an exception being thrown.
+ * **Do we want to allow `lo` and `hi` to be any values of type `$integer`, which means they are dynamic types, like complete array types?**
 * `$hint` : Herbrand integers.  Values are unsimplified symbolic expressions.
 * `$real` : the mathematical real numbers
-* `$float(e,f)`, e, f are integers, each at least 1
+* `$float(e,f)`, e, f are integers, each at least 1.  **Same question for e and f as for lo and hi.**
  * IEEE754 floating point numbers
 * `$hreal` : Herbrand real numbers.  Values are unsimplified symbolic expressions.
 * `struct(T1,...,Tn)`
  * structure type with named fields.  Names may not seem necessary but if you want a subset of CIVL-C...
- * What about bit-widths?
+ * **What about bit-widths?**
 * `union(T1,...,Tn)` : similar to struct
 * `T[]` : array-of-T
@@ -79 +80 @@
 What are two types compatible?
 
+== Type names ==
+
+**Do we need another syntactic category for code that specifies a dynamic type**, for example
+* `int[n*m+3]`.
+
+This can be used in `sizeof`, ...
+
+**Do we need to clearly distinguish dynamic type names and static type names?**
+
+
 == Declarations ==
 
 Declarations follow the C notation.   Function prototypes are considered to be declarations similar to variable declarations.
 
-**Declarations for system, abstract/pure functions?**
+Example of declaration of a function:
+{{{
+$integer f($real x, $bool y);
+}}}
+
+Additional modifiers that may be placed on any of above: 
+* `$pure` : the function has no side effects, but may be nondeterministic
+* `$abstract`: function is a pure, mathematical function: deterministic function of inputs
+
+System functions:
+* A function declaration which is not abstract and for which no definition is provided is a system function.
+* If the system function is called anywhere in the program, it must be defined by providing Java code in an Enabler and Executor.  Failure to do so will result in an exception.
+* A system function may modify any memory it can reach.  This includes allocating new data on heaps it can reach.
+* A system function may have an implicit guard.  This is specified **how**?
+* A system function may have an explicit guard.  This is specified **how**?
+
+Example of a declaration of a system function with guard.  **Fix me:**
+{{{
+$bool g($real x, $bool y) { ... }
+$integer f($real x, $bool y) $guard g;
+}}}
 
 
@@ -125 +156 @@
  * e1,...,en are expressions of integer type
  * the type of this expression is T[e1]...[en]
- * array value with base type `T` and length e1,...,en
+ * array value with base type `T` and lengths e1,...,en
+ * **do we need this for more types?**  E.g., structs of arrays of structs of arrays of ...?
 * `$typeof(...)`: what is this for?
-* `$sizeof(T)` : T is a type name?
+* `sizeof(T)` : T is a type name?
 * `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans
+* **MemoryUnitExpressions?**: are these literal values of type `$mem`?
+ * could we use Frama-C notation `p+(e1..e2)` for example?
+ * are there conversions between pointers and mems?
 
 
@@ -174 +209 @@
 
 == Libraries ==
-