Bind `root` to `data`

Return boogie name for function representing a lifted `some` expression.

Generate vectors for constant values TODO(tengzhang): add support for bv types

Return boogie name of given global spec variable.

Build the Boogie expression for an `Operation::VariantMerge`: a right-folded `(if (enum->$variant_id == i) then arm_exprs[i] else ...)` chain with `ar

Return the destination(s) if self is a branch/jump instruction

Parses a .bpl file and builds the analysis data needed for trace output. Returns a `BplAnalysis` containing assertion descriptions, procedure info, an

NOTE: If there are now renamings, then the root package has the global resolution of all named addresses in the package graph in scope. So we can simp

Collect all dynamic field function QualifiedIds from the environment

Check whether two operations are conflicting

Creates data for a enum declared in Move. Currently all information is contained in the byte code. This is a helper for adding a new module to the env

Creates data for a struct declared in Move. Currently all information is contained in the byte code. This is a helper for adding a new module to the e

Defines a local in the most inner scope. This produces an error if the name already exists. The operation option is used for names which represent spe

Adds a diagnostic of given severity to this environment, with secondary labels.

Emits a Bytecode::Prop based on given kind and expression.

Emit a bodyless `function $name$pure(params) returns (rets);` for a native uninterpreted function that has no FunctionTarget data.

Extract a $Value box value.

Extracts a $Select map with self the variable in the model.

Finalize the the given type, producing an error if it is not complete.

Finalizes types in this build, producing errors if some could not be inferred and remained incomplete.

Gets a StructEnv in this module by its `StructTag`

Find a module by its bytecode format ID

Fix the given type, replacing any remaining free type variables with a type parameter.

Fork this function data, without annotations, and mark it as the given variant.

Formats a parsed `$at(file_idx, start, end)` location into a readable string.

Formats spec properties as a string for display in the tree. Returns a string like " (prove, no_opaque)" or empty string if no properties.

Returns true if the given filter string matches the function environment. Supports three forms: - `<function>` — matches by simple function name - `<m

Returns the attributes of this module.

Returns command line to call boogie.

Gets display information for a function call, including its name and associated spec. If the function has a spec in the current targets, returns the

Returns the debug comment, if any, associated with the given attribute.

Returns the function enclosing this location.

Return the module enclosing this location.

Returns the file id for a file name, if defined.

Get the information computed by this analysis for a function

Gets an iterator for all functions and variants in this holder.

Get verification information for this function.

Returns the variant jump tables for this function.

Get the name to be used for a local. If the local is an argument, use that for naming, otherwise generate a unique name.

Returns line/column position for a location, if available.

Get's the memory associated with a Call(Global,..) or Call(Exists, ..) node. Crashes if the the node is not typed as expected.

Get all modifies targets, as instantiated struct ids.

Gets all modify targets

Gets modify targets for a type

Gets the number of modules in this environment.

Gets the type parameter instantiation associated with the given node, if it is available.

Short cut for getting node instantiation.

Short cut for getting node type.

Return an iterator over the non-parameter local variables of this function

Get field offset.

Return a mutable reference to the node mapped to `o` from self (if any)

Returns the regular parameters associated with this function.