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
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.

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_name	Name of the function to add.
num_of_args	Number 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_contracts	The contracts mangled in the function.
function_id	The 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:

• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/contracts_wrangler.h
• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/contracts_wrangler.cpp