| | 240 | * `$system void $set_default(void *obj);` |
| | 241 | * Updates the leaf nodes of a status variable to the default value 0 |
| | 242 | * `$system void $apply(void *obj1, $operation op, void *obj2, void *result);` |
| | 243 | * Applies the operation op on obj1 and obj2 and stores the result |
| | 244 | * `$system _Bool $equals(void *x, void *y);` |
| | 245 | * Are the object pointed to equal? |
| | 246 | * `$system void $assert_equals(void *x, void *y, ...);` |
| | 247 | * Assert that the two objects pointed are equal |
| | 248 | * `$system _Bool $contains(void *obj1, void *obj2);` |
| | 249 | * Semantics: Does the object pointed to by obj1 contain that pointed to by obj1? |
| | 250 | * `$system void * $translate_ptr(void *ptr, void *obj);` |
| | 251 | * Translates a pointer into one object to a pointer into a different object with similar structure. |
| | 252 | * `$system void $copy(void *ptr, void *value);` |
| | 253 | * Copies the value pointed to by the right operand to the memory location specified by the left operand |
| | 254 | * `$system void $leaf_node_ptrs(void *array, void *obj);` |
| | 255 | * copy the references to the leaf nodes of obj to the given array obj: pointer to type T' whose leaf node types are all type T array: pointer to array of pointer to type T |
| | 256 | * `$system _Bool $is_identity_ref(void *obj);` |
| | 257 | * returns true if the given pointer is referencing to an object by identity reference |
| | 258 | * `$system void $set_leaf_nodes(void *obj, int value);` |
| | 259 | * updates the leaf nodes of the given objects to with the given integer value |
| | 260 | * `$system _Bool $leaf_nodes_equal_to(void *obj, int value);` |
| | 261 | * returns true iff all leaf nodes of the given object equal to the given value |
| | 262 | * `$system _Bool $has_leaf_node_equal_to(void *obj, int value);` |
| | 263 | * returns true iff at least one leaf nodes of the given object equal to the given value |
| | 264 | * `$system _Bool $is_derefable_pointer(void *ptr);` |
| | 265 | * can the given pointer be safely referenced? A derefable pointer is not NULL and is referring to a memory location of some dyscope. |
| | 266 | * `$system void * $pointer_add(const void *ptr, int offset, int type_size);` |
| | 267 | * Gives a pointer addition operation. Note that the input pointer will always be casted to the form of a pointer to a primitive data type. |
