This constraint captures the idea that there is a distinguished pointer width in scope which is appropriate according to the C notion of pointer, and object size. In particular, it must be at least 16-bits wide (as required for the size_t type).

Crucible type of pointers/bitvector values of width w.

Symbolic LLVM pointer or bitvector values of width w.

A pointer with an existentially-quantified width

This pattern synonym makes it easy to build and destruct runtime representatives of LLVMPointerType w.

This pattern creates/matches against the TypeRepr for LLVM pointer values that are of the distinguished pointer width.

This pattern creates/matches against the TypeRepr for raw bitvector values that are of the distinguished pointer width.

A pointer is a base point offset.

Compute the width of a pointer value.

Alternative to the LLVMPointer pattern synonym, this function can be used as a view constructor instead to silence incomplete pattern warnings.

Mux function specialized to LLVM pointer values.

Convert a raw bitvector value into an LLVM pointer value.

Produce the distinguished null pointer value.

Generate a concrete offset value from an Addr value.

Test whether two pointers are equal.

Test whether one pointer is less than or equal to the other.

The returned predicates assert (in this order): * the first pointer is less than or equal to the second * the comparison is valid: the pointers are to the same allocation

Add an offset to a pointer.

Compute the difference between two pointers. The returned predicate asserts that the pointers point into the same allocation block.

Subtract an offset from a pointer.

Test if a pointer value is the null pointer.

Look up a pointer in the memImplGlobalMap to see if it's a global.

This is best-effort and will only work if the pointer is fully concrete and matches the address of the global on the nose. It is used in SAWscript for friendly error messages.

For when you don't know 1 <= w