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

The contents of a Jimple method. More...

#include <jimple_method_body.h>

Inheritance diagram for jimple_method_field:
[legend]

Public Member Functions

virtual exprt to_exprt (contextt &, const std::string &, const std::string &) const
virtual expr2tc to_code2t (contextt &ctx, const std::string &class_name, const std::string &function_name, const locationt &loc) const
 The IREP2 form of this statement, located at loc.
Public Member Functions inherited from jimple_ast
void dump () const
 Prints the contents into the the stdout.
virtual void from_json (const json &)=0
 Initializes the current instance by parsing a JSON.
virtual std::string to_string () const =0
 Converts the object into a string.

Additional Inherited Members

Public Attributes inherited from jimple_ast
int line_location = -1
 instruction location
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

The contents of a Jimple method.

This can be statements or declarations

Member Function Documentation

◆ to_code2t()

virtual expr2tc jimple_method_field::to_code2t ( contextt & ctx,
const std::string & class_name,
const std::string & function_name,
const locationt & loc ) const
inlinevirtual

The IREP2 form of this statement, located at loc.

K.2 of docs/roadmap/scope-jimple-irep2.md. The location is a parameter rather than something the caller stamps afterwards: a code_*2t holds it in a non-reflected field, so it has to be set while the node is still a legacy exprt. As in jimple_method_body, the default migrates whatever to_exprt built, so each override that lands removes a migration instead of adding one.

Reimplemented in jimple_assignment, jimple_declaration, jimple_goto, jimple_if, jimple_invoke, and jimple_label.

◆ to_exprt()

virtual exprt jimple_method_field::to_exprt ( contextt & ,
const std::string & ,
const std::string &  ) const
inlinevirtual

Reimplemented in jimple_identity.


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