Changes between Version 56 and Version 57 of Language


Ignore:
Timestamp:
05/25/23 13:00:08 (3 years ago)
Author:
Alex Wilton
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Language

    v56 v57  
    598598In the symbolic semantics, this function assigns a fresh symbolic constant of the appropriate type to the object pointed to by `ptr`.
    599599
    600 ===  Hiding pointers: `$hide`, `$reveal`, and `$hidden` #hide-reveal-hidden
     600===  Hiding pointers: `$hide`, `$reveal`, and `$hidden` (''experimental'')#hide-reveal-hidden
    601601
    602602The partial order reduction algorithm used by the CIVL Model Checker computes the set of memory locations that a process ''p'' can reach.
    … …  
    618618Nothing can be done with this hidden pointer until it is "revealed", i.e., extracted from the opaque object.
    619619The function `$hidden` tells whether its argument is a value returned by `$hide`.
     620
     621Note: This is an experimental and generally unsound feature meant for developers. Use with caution.
    620622
    621623=== Checking pointer safety: `$is_derefable` #is_derefable