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.

Retrieve this pointer's block number.

Use of this function is discouraged, as it is abstraction-breaking.

Retrieve this pointer's offset.

Use of this function is discouraged, as it is abstraction-breaking.

Mux function specialized to LLVM pointer values.

Convert a raw bitvector value into an LLVM pointer value.

Produce the distinguished null pointer value.

A concrete LLVM pointer

Concretize a symbolic pointer to a particular ConcLLVMPtr that is feasible in a model.

Create a symbolic pointer from a concrete one

An IntrinsicConcFn for LLVM pointers

A singleton map suitable for use in a ConcCtx if LLVM pointers are the only intrinsic type in use

A IntrinsicConcToSymFn for LLVM pointers

A singleton map suitable for use in concToSym if LLVM pointers are the only intrinsic type in use

Generate a concrete offset value from an Addr value.

Test whether two pointers point to the same allocation (i.e., have the same block number).

Using this function is preferred to pattern matching on LLVMPointer or llvmPointerBlock, because it operates at a higher level of abstraction (i.e., if the representation of pointers were changed, it could continue to work as intended).

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 a bitvector (i.e., has a block number of 0)

Using this function is preferred to pattern matching on LLVMPointer or llvmPointerBlock, because it operates at a higher level of abstraction (i.e., if the representation of pointers were changed, it could continue to work as intended).

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