CBMC
dfcc_utilst Struct Reference

#include <dfcc_utils.h>

Static Public Member Functions

static bool function_symbol_exists (const goto_modelt &, const irep_idt &function_id)
 Returns true iff the given symbol exists and satisfies requirements. More...
 
static bool function_symbol_with_body_exists (const goto_modelt &, const irep_idt &function_id)
 
static symboltget_function_symbol (symbol_table_baset &, const irep_idt &function_id)
 Returns the symbolt for function_id. More...
 
static symbol_exprt create_symbol (symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
 Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table, and returns a symbol expression for the created symbol. More...
 
static const symboltcreate_static_symbol (symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
 Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol table, returns the created symbol. More...
 
static const symboltcreate_new_parameter_symbol (symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
 Creates a new parameter symbol for the given function_id. More...
 
static void add_parameter (goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
 Adds the given symbol as parameter to the function symbol's code_type. More...
 
static const symboltadd_parameter (goto_modelt &, const irep_idt &function_id, const std::string &base_name, const typet &type)
 Adds a parameter with given base_name and type to the given function_id. More...
 
static const symboltclone_and_rename_function (goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
 Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given function_id. More...
 
static void wrap_function (goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
 Given a function to wrap foo and a new name wrapped_foo More...
 
static const exprt make_null_check_expr (const exprt &ptr)
 Returns the expression expr == NULL. More...
 
static exprt make_sizeof_expr (const exprt &expr, const namespacet &)
 Returns the expression sizeof(expr). More...
 
static void inline_function (goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
 Inlines the given function, aborts on recursive calls during inlining. More...
 
static void inline_function (goto_modelt &goto_model, const irep_idt &function_id, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
 Inlines the given function, and returns function symbols that caused warnings. More...
 
static void inline_program (goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
 Inlines the given program, and returns function symbols that caused warnings. More...
 

Detailed Description

Definition at line 27 of file dfcc_utils.h.

Member Function Documentation

◆ add_parameter() [1/2]

const symbolt & dfcc_utilst::add_parameter ( goto_modelt goto_model,
const irep_idt function_id,
const std::string &  base_name,
const typet type 
)
static

Adds a parameter with given base_name and type to the given function_id.

Both the symbol and the goto_function are updated.

Definition at line 170 of file dfcc_utils.cpp.

◆ add_parameter() [2/2]

void dfcc_utilst::add_parameter ( goto_modelt goto_model,
const symbolt symbol,
const irep_idt function_id 
)
static

Adds the given symbol as parameter to the function symbol's code_type.

Also adds the corresponding parameter to its goto_function if it exists in the function map of the goto model.

Definition at line 156 of file dfcc_utils.cpp.

◆ clone_and_rename_function()

const symbolt & dfcc_utilst::clone_and_rename_function ( goto_modelt goto_model,
const irep_idt function_id,
const irep_idt new_function_id,
std::optional< typet new_return_type = {} 
)
static

Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given function_id.

The cloned function symbol has new_function_id as name The cloned parameters symbols have new_function_id::name as name Returns the new function symbol

Definition at line 300 of file dfcc_utils.cpp.

◆ create_new_parameter_symbol()

const symbolt & dfcc_utilst::create_new_parameter_symbol ( symbol_table_baset symbol_table,
const irep_idt function_id,
const std::string &  base_name,
const typet type 
)
static

Creates a new parameter symbol for the given function_id.

Definition at line 124 of file dfcc_utils.cpp.

◆ create_static_symbol()

const symbolt & dfcc_utilst::create_static_symbol ( symbol_table_baset symbol_table,
const typet type,
const std::string &  prefix,
const std::string &  base_name,
const source_locationt source_location,
const irep_idt mode,
const irep_idt module,
const exprt initial_value,
const bool  no_nondet_initialization = true 
)
static

Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol table, returns the created symbol.

If a symbol of the same name already exists the name will be decorated with a unique suffix. By default the symbol is be protected against nondet initialisation by tagging the its value field with a ID_C_no_nondet_initialization attribute as understood by nondet_static. This is because the static instrumentation variables are meant to keep their initial values for the instrumentation to work as intended. To allow nondet-initialisation of the symbol, just set no_nondet_initialization to false when calling the method.

Definition at line 103 of file dfcc_utils.cpp.

◆ create_symbol()

symbol_exprt dfcc_utilst::create_symbol ( symbol_table_baset symbol_table,
const typet type,
const irep_idt function_id,
const std::string &  base_name,
const source_locationt source_location 
)
static

Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table, and returns a symbol expression for the created symbol.

If a symbol of the same name already exists the name will be decorated with a unique suffix.

Definition at line 81 of file dfcc_utils.cpp.

◆ function_symbol_exists()

bool dfcc_utilst::function_symbol_exists ( const goto_modelt goto_model,
const irep_idt function_id 
)
static

Returns true iff the given symbol exists and satisfies requirements.

Definition at line 58 of file dfcc_utils.cpp.

◆ function_symbol_with_body_exists()

bool dfcc_utilst::function_symbol_with_body_exists ( const goto_modelt goto_model,
const irep_idt function_id 
)
static

Definition at line 65 of file dfcc_utils.cpp.

◆ get_function_symbol()

symbolt & dfcc_utilst::get_function_symbol ( symbol_table_baset symbol_table,
const irep_idt function_id 
)
static

Returns the symbolt for function_id.

Definition at line 72 of file dfcc_utils.cpp.

◆ inline_function() [1/2]

void dfcc_utilst::inline_function ( goto_modelt goto_model,
const irep_idt function_id,
message_handlert message_handler 
)
static

Inlines the given function, aborts on recursive calls during inlining.

Definition at line 443 of file dfcc_utils.cpp.

◆ inline_function() [2/2]

void dfcc_utilst::inline_function ( goto_modelt goto_model,
const irep_idt function_id,
std::set< irep_idt > &  no_body,
std::set< irep_idt > &  recursive_call,
std::set< irep_idt > &  missing_function,
std::set< irep_idt > &  not_enough_arguments,
message_handlert message_handler 
)
static

Inlines the given function, and returns function symbols that caused warnings.

Definition at line 460 of file dfcc_utils.cpp.

◆ inline_program()

void dfcc_utilst::inline_program ( goto_modelt goto_model,
goto_programt goto_program,
std::set< irep_idt > &  no_body,
std::set< irep_idt > &  recursive_call,
std::set< irep_idt > &  missing_function,
std::set< irep_idt > &  not_enough_arguments,
message_handlert message_handler 
)
static

Inlines the given program, and returns function symbols that caused warnings.

Definition at line 487 of file dfcc_utils.cpp.

◆ make_null_check_expr()

const exprt dfcc_utilst::make_null_check_expr ( const exprt ptr)
static

Returns the expression expr == NULL.

Definition at line 406 of file dfcc_utils.cpp.

◆ make_sizeof_expr()

exprt dfcc_utilst::make_sizeof_expr ( const exprt expr,
const namespacet ns 
)
static

Returns the expression sizeof(expr).

Definition at line 411 of file dfcc_utils.cpp.

◆ wrap_function()

void dfcc_utilst::wrap_function ( goto_modelt goto_model,
const irep_idt function_id,
const irep_idt wrapped_function_id 
)
static

Given a function to wrap foo and a new name wrapped_foo

ret_t foo(x_t foo::x, y_t foo::y) { foo_body; }

This method creates a new entry in the symbol_table for wrapped_foo and moves the body of the original function, foo_body, under wrapped_foo in function_map.

The parameter symbols of wrapped_foo remain the same as in foo:

ret_t wrapped_foo(x_t foo::x, y_t foo::y) { foo_body; }

The parameters of the original foo get renamed to make sure they are distinct from that of wrapped_foo, and a new empty body is generated for foo:

ret_t foo(x_t foo::x_wrapped, y_t foo::y_wrapped) { };

Any other goto_function calling foo still calls foo which has become a wrapper for wrapped_foo.

By generating a new body for foo, one can implement contract checking logic, contract replacement logic, etc.

Definition at line 324 of file dfcc_utils.cpp.


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