|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
The contents of a Jimple method. More...
#include <jimple_method_body.h>
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 | |
The contents of a Jimple method.
This can be statements or declarations
|
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.
|
inlinevirtual |
Reimplemented in jimple_identity.