Changes between Version 119 and Version 120 of IR

Timestamp:

12/09/15 15:50:49 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -302 +302 @@
 * `call(e0,<e1,...,en>)` : function call
  * a function invocation where `e0` must evaluate to either an abstract or pure system function
-* `choose_int(e)` : nondeterministic choice of integer
 
 == The Primitive Statements ==
@@ -539 +538 @@
 === the basic library `civlc` ===
 
-* assertion
-  
-   `void $assert(_Bool expr, ...);`
-
-  It takes an boolean type expression and a number of optional expressions which are used to construct an error message. The optional arguments are similar in form to those used in C’s printf statement: a format string, followed by some number of arguments which are evaluated and substituted for successive codes in the format string.
-
-* assumption
-
-  `void $assume(_Bool expr);`
-
-  During verification, the given expression is assumed to hold. If this leads to a contradiction on some execution, that execution is simply ignored. It never reports a violation, it only restricts the set of possible executions that will be explored by the verification algorithm.
-
-* wait 
-
-  `void $wait($proc p);`
-
-  `void $waitall($proc *procs, int numProcs);`
-
-  When invoked, `$wait` will not return until the process referenced by p has terminated. Similarly, `$waitall` will not return until all the `numProcs` processes referenced by the memory specified by `procs` have terminated. 
-
-* abruption
- 
-  `void $exit(void);`
-
-  This function takes no arguments. It causes the calling process to terminate immediately, regardless of the state of its call stack.
-
 * non-deterministic choice of integer
   
-  `int $choose_int(int n);`
+  `fun[lib="civlc"] $choose_int(n: Integer): Integer;`
 
   This function takes as input a positive integer `n` and nondeterministicaly returns an integer in the range `[0, n − 1]`.
@@ -582 +555 @@
 
   It returns true if and only if the given object of `$proc` type is defined.
-
-* dynamic allocation and deallocation: `$malloc` and `$free`
-
-  `void * $malloc($scope scope, int size);`
-
-  `void $free(void *p);`
-
-  To allocate an object, one first needs a reference to the dynamic scope to be used. The function `$free` is used to deallocate a heap object; it is just like C’s free: An error is generated if the pointer is not one that was returned by $malloc, or if it was already freed.
-
 
 === Scope utilities `scope.cvh` ===