You are an expert in writing code in many different languages. Your goal is to perform code completion for the following code, keeping in mind the rest of the code and the file meta data.
    Metadata details:
    filename: loop_analysis.rs
    path of file: ./repos/diem/language/move-prover/bytecode/src
    
    the code of the file until where you have to start completion: // Copyright (c) The Diem Core Contributors
// SPDX-License-Identifier: Apache-2.0

use crate::{
    function_data_builder::{FunctionDataBuilder, FunctionDataBuilderOptions},
    function_target::{FunctionData, FunctionTarget},
    function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder},
    graph::{Graph, NaturalLoop},
    options::ProverOptions,
    stackless_bytecode::{AttrId, Bytecode, HavocKind, Label, Operation, PropKind},
    stackless_control_flow_graph::{BlockContent, BlockId, StacklessControlFlowGraph},
};
use move_binary_format::file_format::CodeOffset;
use move_model::{
    ast::{self, TempIndex},
    exp_generator::ExpGenerator,
    model::FunctionEnv,
};
use std::collections::{BTreeMap, BTreeSet};

const LOOP_INVARIANT_BASE_FAILED: &str = "base case of the loop invariant does not hold";
const LOOP_INVARIANT_INDUCTION_FAILED: &str = "induction case of the loop invariant does not hold";

/// A fat-loop captures the information of one or more natural loops that share the same loop
/// head
    
    fn build_loop_annotation(func_env: &FunctionEnv<'_>, data: &FunctionData) -> LoopAnnotation {
        // build for natural loops
        let func_target = FunctionTarget::new(func_env, data);
        let code = func_target.get_bytecode();
        let cfg = StacklessControlFlowGraph::new_forward(code);
        let entry = cfg.entry_block();
        let nodes = cfg.blocks();
        let edges: Vec<(BlockId, BlockId)> = nodes
            .iter()
            .flat_map(|x| {
                cfg.successors(*x)
                    .iter()
                    .map(|y| (*x, *y))
                    .collect::<Vec<(BlockId, BlockId)>>()
            })
            .collect();
        let graph = Graph::new(entry, nodes, edges);
        let natural_loops = graph.compute_reducible().expect(
            "A well-formed Move function is expected to have a reducible control-flow graph",
        );

        // collect shared headers from loops
        let mut fat_headers = BTreeMap::new();
        for single_loop in natural_loops {
            fat_headers
                .entry(single_loop.loop_header)
                .or_insert_with(Vec::new)
                .push(single_loop);
        }

        // build fat loops by label
        let mut fat_loops = BTreeMap::new();
        for (fat_root, sub_loops) in fat_headers {
            // get the label of the scc root
            let label = match cfg.content(fat_root) {
                BlockContent::Dummy => panic!("A loop header should never be a dummy block"),
                BlockContent::Basic { lower, upper: _ } => match code[*lower as usize] {
                    Bytecode::Label(_, label) => label,
                    _ => panic!("A loop header block is expected to start with a Label bytecode"),
                },
            };

            let invariants = Self::collect_loop_invariants(&cfg, &func_target, fat_root);
            let (val_targets, mut_targets) =
                Self::collect_loop_targets(&cfg, &func_target, &sub_loops);
            let back_edges = Self::collect_loop_back_edges(code, &cfg, label, &sub_loops);

            // done with all information collection
            fat_loops.insert(
                label,
                FatLoop {
                    invariants,
                    val_targets,
                    mut_targets,
                    back_edges,
                },
            );
        }

        // check for redundant loop invariant declarations in the spec
        let all_invariants: BTreeSet<_> = fat_loops
            .values()
            .map(|l| l.invariants.values().map(|(attr_id, _)| *attr_id))
            .flatten()
            .collect();

        let env = func_target.global_env();
        for attr_id in data.loop_invariants.difference(&all_invariants) {
            env.error(
                &func_target.get_bytecode_loc(*attr_id),
                "Loop invariants must be declared at the beginning of the loop header in a \
                consecutive sequence",
            );
        }

        LoopAnnotation { fat_loops }
    }