Return boogie name of given function Currently bv_flag is used when generating vector functions

Build the least upper bound of two join results, where `Unchanged` is bottom element of the semilattice.

Defines a type parameter.

Creates a display container for the given value. There must be an implementation of fmt::Display for an instance to work in formatting.

Enters a new scope in the locals table.

extract boolean value from ModelValue

Generate a check whether the target can modify the given memory provided (a) the target constraints the given memory (b) the target is the verificatio

Return the specification of the callee function if the specification can be used instead of the callee by the caller. This is the case if and only if

Gets mutable function data for a variant.

Returns the address where the extensions libs are defined.

Get the information computed by this analysis.

Returns return type at given index.

Returns an iterator over structs in this module.

Gets a variant by its tag.

Attempt to convert this type into a normalized::Type

Checks whether a node is in use. A node is used if it is in the live_nodes set or if it is borrowed by a node which is used.

Determines whether the type needs a pack ref.

Checks if a field access at the given offset is accessing the single UID field. Returns true if: - The struct has the `key` ability and the offset is

Makes a symbol from a string.

Walk the structured control flow, tracking versions, collecting merges, and performing substitutions.

Qualifies the given symbol by the current module.

Resolve loop invariant candidates into the final map. When multiple invariant functions target the same (target_func, label), prefer the one from the

Run the pipeline on all functions in the targets holder, with no hooks in effect

Sets instantiation for the given node id. Must not have been set before.

Takes the StateMap resulting from `analyze_function` and converts it into a map from each code offset into a derived state `A`. This re-executes the a

table/object_table struct names

Converts a Loc as used by the move-compiler compiler to the one we are using here. TODO: move-compiler should use FileId as well so we don't need this

Translates a structured block.

Helper to unify two type vectors.

vec_map struct name

Visits expression, calling visitor on each sub-expression. `visitor(false, ..)` will be called before descending into expression, and `visitor(true, .

Adds a source to this environment, returning a FileId for it.

Return field selector for given field.

Recursively builds a spec-only tree for terminal output. Similar to `build_implementation_tree` but: - Only DISPLAYS opaque specs (specs without `no_

Return whether a specific TempIndex involves in bitwise operations

Convert an IfElseChain into nested IfThenElse structures. `if c1 { A } else if c2 { B } else { C }` becomes `if c1 { A } else { if c2 { B } else { C }

Check whether operation of dest and src conflict, if not propagate the merged operation

Update operation in dests and srcs using oper

This function computes the loop headers and natural loops of a reducible graph. If the graph is irreducible, None is returned.

Create bytecode and process it.

Returns the number of diagnostics.

Implements set difference, which is not following standard APIs for rust sets in OrdSet

Emits a sequence of bytecodes.