Documentation

Either an LLVMValue paired with a tree of predicates explaining just when it is actually valid, or a type mismatch.

Take a partial value and assert its safety

An LLVMVal which is always valid.

Concatenate partial LLVM bitvector values. The least-significant (low) bytes are given first. The allocation block number of each argument is asserted to equal 0, indicating non-pointers.

Cons an element onto a partial LLVM array value.

Append two partial LLVM array values.

Make a partial LLVM array value.

It returns Err if any of the elements of the vector are Err. Otherwise, the Pred on the returned NoErr value is the And of all the assertions on the values.

Make a partial LLVM struct value.

It returns Err if any of the struct fields are Err. Otherwise, the Pred on the returned NoErr value is the And of all the assertions on the values.

Assert that the given LLVM pointer value is actually a raw bitvector and extract its value.

Convert a bitvector to a double, asserting that it is not a pointer

Convert a bitvector to a float, asserting that it is not a pointer

Convert a bitvector to an FP80 float, asserting that it is not a pointer

Select some of the most significant bytes of a partial LLVM bitvector value. The allocation block number of the argument is asserted to equal 0, indicating a non-pointer.

Select some of the least significant bytes of a partial LLVM bitvector value. The allocation block number of the argument is asserted to equal 0, indicating a non-pointer.

Look up an element in a partial LLVM array value.

Look up a field in a partial LLVM struct value.

Mux partial LLVM values.

Will panic if the values are not structurally related. This should never happen, as we only call muxLLVMVal from inside the memory model as we read values, and the shape of values is determined by the memory type at which we read values.