remove_calls_no_bodyt Class Reference

#include <remove_calls_no_body.h>

Public Member Functions
void	operator() (goto_programt &goto_program, const goto_functionst &goto_functions, message_handlert &)
	Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value. More...
void	operator() (goto_functionst &goto_functions, message_handlert &)
	Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value. More...

Protected Member Functions
bool	is_opaque_function_call (const goto_programt::const_targett target, const goto_functionst &goto_functions)
	Check if instruction is a call to an opaque function through an ordinary (non-function pointer) call. More...
void	remove_call_no_body (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
	Remove a single call. More...

Detailed Description

Definition at line 20 of file remove_calls_no_body.h.

Member Function Documentation

is_opaque_function_call()

bool remove_calls_no_bodyt::is_opaque_function_call ( const goto_programt::const_targett  target, const goto_functionst &  goto_functions  )

protected

Check if instruction is a call to an opaque function through an ordinary (non-function pointer) call.

Parameters

target	iterator pointing to the instruction to check
goto_functions	all goto function to look up call target

Definition at line 66 of file remove_calls_no_body.cpp.

operator()() [1/2]

void remove_calls_no_bodyt::operator()	(	goto_functionst &	goto_functions,
		message_handlert &	message_handler
	)

Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value.

Parameters

goto_functions	goto functions to operate on
message_handler	message handler

Definition at line 128 of file remove_calls_no_body.cpp.

operator()() [2/2]

void remove_calls_no_bodyt::operator()	(	goto_programt &	goto_program,
		const goto_functionst &	goto_functions,
		message_handlert &	message_handler
	)

Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value.

Parameters

goto_program	goto program to operate on
goto_functions	all goto functions; for looking up functions which the goto program may call
message_handler	message handler

Definition at line 99 of file remove_calls_no_body.cpp.

remove_call_no_body()

void remove_calls_no_bodyt::remove_call_no_body ( goto_programt &  goto_program, goto_programt::targett  target, const exprt &  lhs, const exprt::operandst &  arguments  )

protected

Remove a single call.

Parameters

goto_program	goto program to modify
target	iterator pointing to the call
lhs	lhs of the call to which the return value is assigned
arguments	arguments of the call

Definition at line 25 of file remove_calls_no_body.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-programs/remove_calls_no_body.h
• /home/runner/work/cbmc/cbmc/src/goto-programs/remove_calls_no_body.cpp