Changes between Version 17 and Version 18 of Language

Timestamp:

05/18/23 22:11:14 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -497 +497 @@
 === `$elaborate_domain`
 
+Forces explicit enumeration of the elements of a finite domain.  Signature
+{{{
+$system void $elaborate_domain($domain d);
+}}}
+In the concrete semantics, this is a no-op.
+
 === `$exit`
 
-=== `$free`
+Terminates the calling process.  Signature:
+{{{
+$system void $exit(void);
+}}}
 
 === `$havoc`
@@ -515 +524 @@
 === `$local_start`
 
-=== `$malloc`
+=== Heap memory allocation: `$malloc` and `$free`
+
+Allocate and deallocate heap memory.  Signatures:
+{{{
+$system void* $malloc($scope s, int size);
+$system void $free(void *p);
+}}}
+Each dynamic scope has a heap.
+Function `$malloc` allocates `size` bytes in the heap of scope `s`.
+Unlike C's `malloc`, `$malloc` cannot fail. 
+Note that `malloc` is implemented as `$malloc($root, size)`.
+
+Function `$free` deallocates the object pointed to by `p`, which should be a pointer that was returned
+by an earlier call to `$malloc`. 
+An error is generated if the pointer is not one that was returned by $malloc, or if it was already freed.
 
 === `$pathCondition`
 
-=== `$pow` 
-
-`$pow(double, double)` 
+Prints the current effective path condition.
+{{{
+$system void $pathCondition(void);
+}}}
+
+=== Power function: `$pow` 
+
+Computes ''x^y^``.
+{{{
+$system double $pow(double base, double exp);
+}}}
 
 === `$reveal`