Changes between Version 116 and Version 117 of IR

Timestamp:

12/09/15 15:29:36 (10 years ago)

Author:

zmanchun

Comment:

--

IR

@@ -340 +340 @@
   var p:Array[Proc];
 
-  fun f()
+  fun f(i, j)
   {
     S;
@@ -523 +523 @@
 == Libraries ==
 
+The CIVL core libraries include:
+
+* `civlc.cvh`: the basic library of CIVL, usually included in a CIVL-C program, defining types and functions that are frequently used;
+
+* `scope.cvh`: providing utility functions related to dynamic scopes;
+
+* `pointer.cvh`: providing utility functions dealing with pointers;
+
+* `seq.cvh`: providing operations on sequences which is realized using arrays;
+
+* `concurrency.cvh`: providing concurrency utilities such as barrier and collective record;
+
+* `bundle.cvh`: defining bundle types and their operations;
+
+* `comm.cvh`: defining communicators and their operations.
+
+=== 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);`
+
+  This function takes as input a positive integer `n` and nondeterministicaly returns an integer in the range `[0, n − 1]`.
+
+* is a scope reference defined?
+
+  `_Bool $scope_defined($scope s);`
+
+  It returns true if the dynamic scope specified by `s` is defined, else it returns false.
+
+* is a process reference defined?
+
+  `_Bool $proc_defined($proc p);`
+
+  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` ===
+The header `scope.cvh` declares one function: `$scope` parent, which has signature
+
+`$scope $scope_parent($scope s);`
+
+This function returns the parent dynamic scope of the dynamic scope referenced by `s`. If `s` is the root dynamic scope, it returns the undefined value of type `$scope`.
+
+=== Pointer utilities `pointer.cvh` ===
+The header `pointer.cvh` declares functions taking pointers as the arguments for different purposes, including:
+
+* equality checking:
+  `_Bool $equals(void *x, void *y);` 
+  this function returns true iff the objects pointed to by the pointers `x` and `y` have the same type and value.
+
+* membership testing:
+  `_Bool $contains(void *ptr1, void *ptr2);`
+  this function returns true iff the object pointed to by `ptr1` contains the object pointed to by `ptr2`. For example, `$contains(&a, &a[1].x)` would return true.
+
+* pointer creation:
+ $translate ptr for pointer translation; 
+* copy through pointers:
+
 Which libraries require system functions?
 pointer, ...