CBMC
Public Member Functions | Public Attributes | Protected Member Functions | Protected Attributes | List of all members
contracts_wranglert Class Reference

#include <contracts_wrangler.h>

+ Collaboration diagram for contracts_wranglert:

Public Member Functions

 contracts_wranglert (goto_modelt &goto_model, const std::string &file_name, message_handlert &message_handler)
 

Public Attributes

namespacet ns
 

Protected Member Functions

void configure_functions (const jsont &)
 
void mangle (const loop_contracts_clauset &loop_contracts, const irep_idt &function_id)
 Mangle loop_contracts in the function with function_id More...
 
void add_builtin_pointer_function_symbol (std::string function_name, const std::size_t num_of_args)
 Add builtin function symbol with function_name into symbol table. More...
 

Protected Attributes

goto_modelt & goto_model
 
symbol_tablet & symbol_table
 
goto_functionst & goto_functions
 
message_handlert & message_handler
 
functionst functions
 

Detailed Description

Definition at line 60 of file contracts_wrangler.h.

Constructor & Destructor Documentation

◆ contracts_wranglert()

contracts_wranglert::contracts_wranglert ( goto_modelt &  goto_model,
const std::string &  file_name,
message_handlert &  message_handler 
)

Definition at line 29 of file contracts_wrangler.cpp.

Member Function Documentation

◆ add_builtin_pointer_function_symbol()

void contracts_wranglert::add_builtin_pointer_function_symbol ( std::string  function_name,
const std::size_t  num_of_args 
)
protected

Add builtin function symbol with function_name into symbol table.

Parameters
function_nameName of the function to add.
num_of_argsNumber of arguments of the added symbol.

Definition at line 80 of file contracts_wrangler.cpp.

◆ configure_functions()

void contracts_wranglert::configure_functions ( const jsont &  config)
protected

Definition at line 273 of file contracts_wrangler.cpp.

◆ mangle()

void contracts_wranglert::mangle ( const loop_contracts_clauset &  loop_contracts,
const irep_idt &  function_id 
)
protected

Mangle loop_contracts in the function with function_id

Parameters
loop_contractsThe contracts mangled in the function.
function_idThe function containing the loop we mangle to.

Definition at line 100 of file contracts_wrangler.cpp.

Member Data Documentation

◆ functions

functionst contracts_wranglert::functions
protected

Definition at line 77 of file contracts_wrangler.h.

◆ goto_functions

goto_functionst& contracts_wranglert::goto_functions
protected

Definition at line 73 of file contracts_wrangler.h.

◆ goto_model

goto_modelt& contracts_wranglert::goto_model
protected

Definition at line 71 of file contracts_wrangler.h.

◆ message_handler

message_handlert& contracts_wranglert::message_handler
protected

Definition at line 75 of file contracts_wrangler.h.

◆ ns

namespacet contracts_wranglert::ns

Definition at line 68 of file contracts_wrangler.h.

◆ symbol_table

symbol_tablet& contracts_wranglert::symbol_table
protected

Definition at line 72 of file contracts_wrangler.h.

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