/// This generates boogie code for everything after the function signature
/// The function body is only generated for the `FunctionEntryPoint::Definition`
/// version of the function.
This generates boogie code for everything after the function signature
The function body is only generated for the `FunctionEntryPoint::Definition`
version of the function.
This generates boogie code for everything after the function signature The function body is only generated for the ` FunctionEntryPoint :: Definition ` version of the function .
fn generate_inline_function_body(&self, func_target: &FunctionTarget<'_>) {
        // Construct context for bytecode translation.
        let context = BytecodeContext::new(func_target);
        // Be sure to set back location to the whole function definition as a default, otherwise
        // we may get unassigned code locations associated with condition locations.
        self.writer.set_location(&func_target.get_loc());
        emitln!(self.writer, "{");
        self.writer.indent();
        // Generate local variable declarations. They need to appear first in boogie.
        emitln!(self.writer, "// declare local variables");
        let num_args = func_target.get_parameter_count();
        for i in num_args..func_target.get_local_count() {
            let local_name = func_target.get_local_name(i);
            let local_type = func_target.get_local_type(i);
            emitln!(
                self.writer,
                "var {}: {}; // {}",
                local_name.display(func_target.symbol_pool()),
                boogie_local_type(local_type),
                boogie_type_value(self.module_env.env, local_type)
            );
        }
        emitln!(self.writer, "var $tmp: $Value;");
        emitln!(self.writer, "\n// initialize function execution");
        emitln!(self.writer, "assume !$abort_flag;");
        emitln!(self.writer, "\n// track values of parameters at entry time");
        for i in 0..func_target.get_parameter_count() {
            let local_name = func_target.get_local_name(i);
            let local_str = format!("{}", local_name.display(func_target.symbol_pool()));
            let s = self.track_local(func_target, func_target.get_loc(), i, &local_str);
            if !s.is_empty() {
                emitln!(self.writer, &s);
            }
        }
        emitln!(self.writer, "\n// bytecode translation starts here");
        // Generate bytecode
        let code = func_target.get_bytecode();
        for (offset, bytecode) in code.iter().enumerate() {
            self.translate_bytecode(func_target, &context, offset as CodeOffset, bytecode);
        }
        // Generate abort exit.
        let end_loc = func_target.get_loc().at_end();
        self.writer.set_location(&end_loc);
        self.writer.unindent();
        emitln!(self.writer, "Abort:");
        self.writer.indent();
        emitln!(self.writer, "$abort_flag := true;");
        for (i, ty) in func_target.get_return_types().iter().enumerate() {
            let ret_str = format!("$ret{}", i);
            if ty.is_reference() {
                emitln!(self.writer, "{} := $DefaultReference;", &ret_str);
            } else {
                emitln!(self.writer, "{} := $DefaultValue();", &ret_str);
            }
        }
        self.writer.unindent();
        emitln!(self.writer, "}");
    }
fn generate_inline_function_body ( & self , func_target : & FunctionTarget < ' _ > ) { // Construct context for bytecode translation. let context = BytecodeContext :: new ( func_target ) ; // Be sure to set back location to the whole function definition as a default, otherwise // we may get unassigned code locations associated with condition locations. self . writer . set_location ( & func_target . get_loc ( ) ) ; emitln ! ( self writer " " ) ; self . writer . indent ( ) ; // Generate local variable declarations. They need to appear first in boogie. emitln ! ( self writer " " ) ; let num_args = func_target . get_parameter_count ( ) ; for i in num_args .. func_target . get_local_count ( ) { let local_name = func_target . get_local_name ( i ) ; let local_type = func_target . get_local_type ( i ) ; emitln ! ( self writer " " local_name display ( func_target symbol_pool ( ) ) boogie_local_type ( local_type ) boogie_type_value ( self module_env env local_type ) ) ; } emitln ! ( self writer " " ) ; emitln ! ( self writer " \n " ) ; emitln ! ( self writer " " ) ; emitln ! ( self writer " \n " ) ; for i in 0 .. func_target . get_parameter_count ( ) { let local_name = func_target . get_local_name ( i ) ; let local_str = format ! ( " " local_name display ( func_target symbol_pool ( ) ) ) ; let s = self . track_local ( func_target , func_target . get_loc ( ) , i , & local_str ) ; if ! s . is_empty ( ) { emitln ! ( self writer s ) ; } } emitln ! ( self writer " \n " ) ; // Generate bytecode let code = func_target . get_bytecode ( ) ; for ( offset , bytecode ) in code . iter ( ) . enumerate ( ) { self . translate_bytecode ( func_target , & context , offset as CodeOffset , bytecode ) ; } // Generate abort exit. let end_loc = func_target . get_loc ( ) . at_end ( ) ; self . writer . set_location ( & end_loc ) ; self . writer . unindent ( ) ; emitln ! ( self writer " " ) ; self . writer . indent ( ) ; emitln ! ( self writer " " ) ; for ( i , ty ) in func_target . get_return_types ( ) . iter ( ) . enumerate ( ) { let ret_str = format ! ( " " i ) ; if ty . is_reference ( ) { emitln ! ( self writer " " ret_str ) ; } else { emitln ! ( self writer " " ret_str ) ; } } self . writer . unindent ( ) ; emitln ! ( self writer " " ) ; }
This generates boogie code for everything after the function signature
The function body is only generated for the `FunctionEntryPoint::Definition`
version of the function.
This generates boogie code for everything after the function signature The function body is only generated for the ` FunctionEntryPoint :: Definition ` version of the function .
&self
func_target
&FunctionTarget<'_>