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

Base interface to hold jimple expressions. More...

#include <jimple_expr.h>

Inheritance diagram for jimple_expr:
[legend]

Public Member Functions

virtual exprt to_exprt (contextt &, const std::string &, const std::string &) const
virtual expr2tc to_expr2t (contextt &ctx, const std::string &class_name, const std::string &function_name) const
 The IREP2 form of this expression.
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.

Static Public Member Functions

static std::shared_ptr< jimple_expr > get_expression (const json &j)
 Recursively explores and initializes a jimple_expression.

Static Protected Member Functions

static expr2tc lower_invoke2t (contextt &ctx, const std::string &base_class, const std::string &method, const std::string &this_variable, const std::vector< std::shared_ptr< jimple_expr > > &parameters, const expr2tc &lhs, const std::string &class_name, const std::string &function_name)
 Lower an invoke to the block both invoke forms produce.
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

Additional Inherited Members

Public Attributes inherited from jimple_ast
int line_location = -1
 instruction location

Detailed Description

Base interface to hold jimple expressions.

Member Function Documentation

◆ get_expression()

std::shared_ptr< jimple_expr > jimple_expr::get_expression ( const json & j)
static

Recursively explores and initializes a jimple_expression.

Jimple expressions can be unary (e.g. cast) or binary (e.g. addition), however, the operands can be other expressions. For example, it is valid to do a cast over a math operation: (int) 1 + 1 in Jimple, this should be parsed as:

  • cast:
    • to: int
    • from:
      • binop: +
        • op1: 1
        • op2: 1

This function will do that

Parameters
j
Returns
std::shared_ptr<jimple_expr>

◆ lower_invoke2t()

expr2tc jimple_expr::lower_invoke2t ( contextt & ctx,
const std::string & base_class,
const std::string & method,
const std::string & this_variable,
const std::vector< std::shared_ptr< jimple_expr > > & parameters,
const expr2tc & lhs,
const std::string & class_name,
const std::string & function_name )
staticprotected

Lower an invoke to the block both invoke forms produce.

One assignment per bound argument into the callee's own @this/@parameterN symbol – the frontend's stand-in for the parameter binding that belongs at symex – followed by the call. this_variable is empty for a static invoke, and lhs is nil when the result is discarded.

◆ to_expr2t()

virtual expr2tc jimple_expr::to_expr2t ( contextt & ctx,
const std::string & class_name,
const std::string & function_name ) const
inlinevirtual

The IREP2 form of this expression.

The expression counterpart of jimple_method_field::to_code2t (K.4 of docs/roadmap/scope-jimple-irep2.md). A return type belongs to a virtual's signature, so the 27 to_exprt overrides cannot migrate one at a time; a parallel method can, with this default carrying whatever has not moved yet and shrinking as each override lands.

Reimplemented in jimple_binop, jimple_cast, jimple_constant, jimple_deref, jimple_expr_invoke, jimple_lengthof, jimple_newarray, jimple_nondet, jimple_static_member, jimple_symbol, jimple_virtual_invoke, and jimple_virtual_member.

◆ to_exprt()

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

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