Changes between Version 18 and Version 19 of Language

Timestamp:

05/18/23 22:20:00 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -512 +512 @@
 === `$havoc`
 
-=== `$hidden`
+Assigns an arbitrary value of the object's type to an object.  Signature:
+{{{
+$system void $havoc(void *ptr);
+}}}
+In the concrete semantics, this function assigns an arbitrary value of the appropriate type to the object pointed to by `ptr`.
+
+In the symbolic semantics, this function assigns a fresh symbolic constant of the appropriate type to the object pointed to by `ptr`.
+
+===  Hiding pointers from the reachability analyzer: `$hide`, `$hidden`, and `$reveal`
+
+
+{{{
+$abstract void* $hide(const void* ptr);
+$system _Bool $hidden(const void* ptr);
+$system void* $reveal(const void* ptr);
+}}}
 
 === `$hide`
@@ -549 +564 @@
 === Power function: `$pow` 
 
-Computes ''x^y^``.
+Computes ''x^y^''.
 {{{
 $system double $pow(double base, double exp);