Updates the values in the range of the map using the given function. Notice that with other kind of map representations we would use `iter_mut` for th

Write spec hierarchy log files for all specs in the given targets. Only writes during `AssertsMode::Check` to avoid duplicate writes.

Writes a single spec's hierarchy tree to a log file. Creates a file named `{spec_name}.log.txt` containing: - Header line (function name or scenario

Helper to add a boogie error as a codespan Diagnostic.

Adds the prelude to the generated output.

Adjust a timeout value, given in seconds, for the runtime environment.

Entry point of the analysis

NOTE: we don't care about type cycles here, as they are resticted by Move type system/compiler

Apply parameter substitution if present.

Returns the set of function names referenced by any asserts_of declaration.

Delivers a location pointing to the end of this one.

Converts a biguint into an account address

Binds the type variables.

Bind `node` to `lhs` in the trie, overwriting the old value of `lhs`

Return a Boogie expression that evaluates to a fixed default value of the given Move type. Used to fill non-active variant fields when constructing an

Return field selector for given field.

Creates the name of the resource memory domain for any function for the given struct. This variable represents a local variable of the Boogie translat

Create boogie well-formed check. The result will be either an empty string or a newline-terminated assume statement.

Create boogie well-formed boolean expression.

Recursively builds the implementation tree for log files. Shows ALL functions in the call graph with their associated specs (if any). Stops recursing

Help generating vector functions for bv types

Calls boogie on the given file. On success, returns a struct representing the analyzed output of boogie.

Calls boogie and analyzes output.

Check whether operations in s conflicting

================================================================================================ # Modifies Checker Check modifies annotations. This i

Checks whether the expected tool versions are installed in the environment.

This will clear the state that the next `self.emit_with(..)` will add a debug comment.

Start from this node and follow-up the borrow chain until reaching a live/in-use ancestor. Collect possible paths (from this node to a live ancestor)

Collect dynamic field type information from a function's bytecode

Collect variables assigned multiple times and initialize the current version of each variable to itself (placeholder).

Computes the call trace for an assertion in an inline procedure by BFS backward through the reverse call graph to find the entry point, producing entr

Compute for each variable the last if-then-else block with a merge instruction. Returns the set of multi-assigned variables assigned in this block.

Computes a mapping from temporary indices to the objects and types of objects they reference

Like `compute_uid_info` but runs before `process` (no callee annotations available). Computes callee uid_info on-the-fly instead of reading annotation

Counts specs that will be displayed at the current tree level. This includes both direct specs and specs found by recursing through transparent (no-sp

Transpose the domain map in the model by aggregating values in it by the key into a standalone map

Creates data for a function, adding any information not contained in bytecode. This is a helper for adding a new module to the environment.

Create initial number operation state for expressions

Create the initial NumberOperationState

Populate default state for struct operation map