Changes between Version 41 and Version 42 of IR

Timestamp:

11/23/15 17:42:42 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -140 +140 @@
 * `$pure` : the function has no side effects, but may be nondeterministic
 * `$abstract`: function is a pure, mathematical function: deterministic function of inputs
-* `$atomic_f`: function definition is atomic, and there is it is never blocked
+* `$atomic_f`: function definition is atomic, and it never blocks
 
 System functions:
@@ -204 +204 @@
 * `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans
 * **Memory set expressions**: 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?
-
+ * a left-hand-side expression, when used in certain contexts, is automatically converted to `$mem`.  The contexts are: arguments to the built-in functions `$access`, `$read`, and `$write` described below, or occurrence in the list of an `$assigns` clause
+ * `a[dom]`, where `a` is an expression of array type and `dom` is an expression of `$domain` type.   The dimension of the array must match the dimension of the domain.   This represents all memory units which are the cells in the array indexed by a tuple in `dom`.
+ * `$region(ptr)`, where `ptr` is an expression with a pointer type.  This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself.
+ * `mem1+mem2`, where `mem1` and `mem2` are expressions of type `$memory`.  This is the union of the two sets.  **Problem this is ambiguous with numeric +, as in x+y.**
+ * **could we use Frama-C notation `p+(e1..e2)` for example?**
+ * **are there conversions between pointers and mems?**
 
 Pointers: unlike C, there is no "array-pointer pun".   If an array `a` needs to be converted to a pointer, you must use `&a[0]`.