ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
jimple_full_method_body Class Reference

A Jimple method definition. More...

#include <jimple_method_body.h>

Inheritance diagram for jimple_full_method_body:
[legend]

Public Types

enum class  statement {
  Assignment , Identity , StaticInvoke , SpecialInvoke ,
  VirtualInvoke , Return , Label , Goto ,
  If , Declaration , Throw , Location
}

Public Member Functions

virtual void from_json (const json &j) override
 Initializes the current instance by parsing a JSON.
virtual std::string to_string () const override
 Converts the object into a string.
virtual expr2tc to_code2t (contextt &ctx, const std::string &class_name, const std::string &function_name) const override
 The IREP2 form of the body, for symbolt::set_value(const expr2tc &).
Public Member Functions inherited from jimple_method_body
virtual exprt to_exprt (contextt &, const std::string &, const std::string &) const
Public Member Functions inherited from jimple_ast
void dump () const
 Prints the contents into the the stdout.

Public Attributes

std::vector< std::shared_ptr< jimple_method_field > > members
Public Attributes inherited from jimple_ast
int line_location = -1
 instruction location

Additional Inherited Members

Static Protected Member Functions inherited from jimple_ast
static symbolt create_jimple_symbolt (const type2tc &t, const std::string &module, const std::string &name, const std::string &id, const std::string function_name="")
 creates a symbol with the default characteristics
static symbolt get_temp_symbol (const type2tc &t, const std::string &class_name, const std::string &function_name)
 Create a temporary variable to be used.
static symbolt get_allocation_function ()
 Get the allocation function symbol.
static symbolt get_lengthof_function ()
 Get the esbmc_get_object_size symbol.
static std::string get_method_name (std::string class_name, std::string function_name)
 Get the unique method name.
static std::string get_symbol_name (std::string class_name, std::string function_name, std::string symbol)
 Get the symbol name id.
static locationt get_location (const std::string &module, const std::string function_name="")
 initialize a location for the symbol

Detailed Description

A Jimple method definition.

Something such as: public void foo() { }

Member Enumeration Documentation

◆ statement

Enumerator
Assignment 
Identity 
StaticInvoke 
SpecialInvoke 
VirtualInvoke 
Return 
Label 
Goto 
If 
Declaration 
Throw 
Location 

Member Function Documentation

◆ from_json()

void jimple_full_method_body::from_json ( const json & )
overridevirtual

Initializes the current instance by parsing a JSON.

Parameters
jsonThe json object relative to the structure

Implements jimple_ast.

◆ to_code2t()

expr2tc jimple_full_method_body::to_code2t ( contextt & ctx,
const std::string & class_name,
const std::string & function_name ) const
overridevirtual

The IREP2 form of the body, for symbolt::set_value(const expr2tc &).

K.1 of docs/roadmap/scope-jimple-irep2.md. The default migrates whatever to_exprt built, so a subclass that has not been converted yet keeps working; each override that lands removes one migration rather than adding one, which is why this migration runs from the seam downwards.

Reimplemented from jimple_method_body.

◆ to_string()

std::string jimple_full_method_body::to_string ( ) const
overridevirtual

Converts the object into a string.

Returns
a human readable string of the object

Implements jimple_ast.

Member Data Documentation

◆ members

std::vector<std::shared_ptr<jimple_method_field> > jimple_full_method_body::members

The documentation for this class was generated from the following files: