CBMC
Loading...
Searching...
No Matches
Public Member Functions | List of all members
cleanert Class Reference

Class that allows to clean expressions of side effects and to generate havoc_slice expressions. More...

#include <utils.h>

+ Inheritance diagram for cleanert:
[フレーム]
[legend]
+ Collaboration diagram for cleanert:
[フレーム]
[legend]

Public Member Functions

  cleanert (symbol_table_baset &_symbol_table, message_handlert &_message_handler)
 
std::list< irep_idt >  clean (exprt &guard, goto_programt &dest, const irep_idt &mode)
 
void  do_havoc_slice (const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 
- Public Member Functions inherited from goto_convertt
void  goto_convert (const codet &code, goto_programt &dest, const irep_idt &mode)
 
  goto_convertt (symbol_table_baset &_symbol_table, message_handlert &_message_handler)
 
virtual  ~goto_convertt ()
 
void  set_prefix (const std::string &prefix)
 
- Public Member Functions inherited from messaget
virtual void  set_message_handler (message_handlert &_message_handler)
 
message_handlert &  get_message_handler ()
 
  messaget (const messaget &other)
 
messaget &  operator= (const messaget &other)
 
  messaget (message_handlert &_message_handler)
 
virtual  ~messaget ()
 
mstreamt &  get_mstream (unsigned message_level) const
 
mstreamt &  error () const
 
mstreamt &  warning () const
 
mstreamt &  result () const
 
mstreamt &  status () const
 
mstreamt &  statistics () const
 
mstreamt &  progress () const
 
mstreamt &  debug () const
 
void  conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
  Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream.
 

Additional Inherited Members

- Public Types inherited from messaget
enum   message_levelt {
  M_ERROR =1 , M_WARNING =2 , M_RESULT =4 , M_STATUS =6 ,
  M_STATISTICS =8 , M_PROGRESS =9 , M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned  eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
  Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
 
static commandt  command (unsigned c)
  Create an ECMA-48 SGR (Select Graphic Rendition) command.
 
- Static Public Attributes inherited from messaget
static eomt  eom
 
static const commandt  reset
  return to default formatting, as defined by the terminal
 
static const commandt  red
  render text with red foreground color
 
static const commandt  green
  render text with green foreground color
 
static const commandt  yellow
  render text with yellow foreground color
 
static const commandt  blue
  render text with blue foreground color
 
static const commandt  magenta
  render text with magenta foreground color
 
static const commandt  cyan
  render text with cyan foreground color
 
static const commandt  bright_red
  render text with bright red foreground color
 
static const commandt  bright_green
  render text with bright green foreground color
 
static const commandt  bright_yellow
  render text with bright yellow foreground color
 
static const commandt  bright_blue
  render text with bright blue foreground color
 
static const commandt  bright_magenta
  render text with bright magenta foreground color
 
static const commandt  bright_cyan
  render text with bright cyan foreground color
 
static const commandt  bold
  render text with bold font
 
static const commandt  faint
  render text with faint font
 
static const commandt  italic
  render italic text
 
static const commandt  underline
  render underlined text
 
static const commandt  quote_begin
  Start quoted text.
 
static const commandt  quote_end
  End quoted text.
 
- Protected Types inherited from goto_convertt
typedef std::list< std::pair< goto_programt::targett, goto_programt::instructiont > >  declaration_hop_instrumentationt
 
typedef std::map< irep_idt, std::pair< goto_programt::targett, node_indext > >  labelst
 
typedef std::list< std::pair< goto_programt::targett, node_indext > >  gotost
 
typedef std::list< goto_programt::targett >  computed_gotost
 
typedef exprt::operandst  caset
 
typedef std::list< std::pair< goto_programt::targett, caset > >  casest
 
typedef std::map< goto_programt::targett, casest::iterator, goto_programt::target_less_than >  cases_mapt
 
- Protected Member Functions inherited from goto_convertt
void  goto_convert_rec (const codet &code, goto_programt &dest, const irep_idt &mode)
 
symbolt &  new_tmp_symbol (const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
 
symbol_exprt  make_compound_literal (const exprt &expr, goto_programt &dest, const irep_idt &mode)
 
clean_expr_resultt  clean_expr (exprt &expr, const irep_idt &mode, bool result_is_used=true)
 
clean_expr_resultt  clean_expr_address_of (exprt &expr, const irep_idt &mode)
 
irep_idt  make_temp_symbol (exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
 
void  rewrite_boolean (exprt &dest)
  re-write boolean operators into ?:
 
clean_expr_resultt  remove_side_effect (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
 
clean_expr_resultt  remove_assignment (side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
 
clean_expr_resultt  remove_pre (side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)
 
clean_expr_resultt  remove_post (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt  remove_function_call (side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt  remove_cpp_new (side_effect_exprt &expr, bool result_is_used)
 
clean_expr_resultt  remove_cpp_delete (side_effect_exprt &expr)
 
clean_expr_resultt  remove_malloc (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt  remove_temporary_object (side_effect_exprt &expr)
 
clean_expr_resultt  remove_statement_expression (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
 
clean_expr_resultt  remove_gcc_conditional_expression (exprt &expr, const irep_idt &mode)
 
clean_expr_resultt  remove_overflow (side_effect_expr_overflowt &expr, bool result_is_used, const irep_idt &mode)
 
virtual void  do_cpp_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
 
void  do_java_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
 
void  do_java_new_array (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
 
void  cpp_new_initializer (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
  builds a goto program for object initialization after new
 
virtual void  do_function_call (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 
virtual void  do_function_call_if (const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 
virtual void  do_function_call_symbol (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
  add function calls to function queue for later processing
 
virtual void  do_function_call_symbol (const symbolt &)
 
virtual void  do_function_call_other (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  convert_block (const code_blockt &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_frontend_decl (const code_frontend_declt &, goto_programt &, const irep_idt &mode)
 
void  convert_decl_type (const codet &code, goto_programt &dest)
 
void  convert_expression (const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_assign (const code_assignt &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_cpp_delete (const codet &code, goto_programt &dest)
 
void  convert_loop_contracts (const codet &code, goto_programt::targett loop)
 
void  convert_for (const code_fort &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_while (const code_whilet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_dowhile (const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_assume (const code_assumet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_assert (const code_assertt &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_switch (const code_switcht &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_break (const code_breakt &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_return (const code_frontend_returnt &, goto_programt &dest, const irep_idt &mode)
 
void  convert_continue (const code_continuet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_ifthenelse (const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_goto (const code_gotot &code, goto_programt &dest)
 
void  convert_gcc_computed_goto (const codet &code, goto_programt &dest)
 
void  convert_skip (const codet &code, goto_programt &dest)
 
void  convert_label (const code_labelt &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_gcc_local_label (const codet &code, goto_programt &dest)
 
void  convert_switch_case (const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_gcc_switch_case_range (const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode)
 
void  convert_function_call (const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_start_thread (const codet &code, goto_programt &dest)
 
void  convert_end_thread (const codet &code, goto_programt &dest)
 
void  convert_atomic_begin (const codet &code, goto_programt &dest)
 
void  convert_atomic_end (const codet &code, goto_programt &dest)
 
void  convert_msc_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_msc_try_except (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_msc_leave (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_CPROVER_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_CPROVER_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_CPROVER_throw (const codet &code, goto_programt &dest, const irep_idt &mode)
 
void  convert_asm (const code_asmt &code, goto_programt &dest)
 
void  convert (const codet &code, goto_programt &dest, const irep_idt &mode)
  converts 'code' and appends the result to 'dest'
 
void  copy (const codet &code, goto_program_instruction_typet type, goto_programt &dest)
 
symbol_exprt  exception_flag (const irep_idt &mode)
 
void  unwind_destructor_stack (const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_point={})
  Unwinds the destructor stack and creates destructors for each node between destructor_start_point and destructor_end_point (including the start, excluding the end).
 
declaration_hop_instrumentationt  build_declaration_hops (goto_programt &dest, std::unordered_map< irep_idt, symbolt, irep_id_hash > &label_flags, const build_declaration_hops_inputst &inputs)
 
void  finish_gotos (goto_programt &dest, const irep_idt &mode)
 
void  finish_computed_gotos (goto_programt &dest)
 
void  optimize_guarded_gotos (goto_programt &dest)
  Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a branch target.
 
exprt  case_guard (const exprt &value, const caset &case_op)
 
void  generate_ifthenelse (const exprt &cond, const source_locationt &, goto_programt &true_case, const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
  if(guard) true_case; else false_case;
 
void  generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
  if(guard) goto target_true; else goto target_false;
 
void  generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, const source_locationt &, goto_programt &dest, const irep_idt &mode)
 
void  generate_thread_block (const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
  Generates the necessary goto-instructions to represent a thread-block.
 
irep_idt  get_string_constant (const exprt &expr)
 
bool  get_string_constant (const exprt &expr, irep_idt &)
 
exprt  get_constant (const exprt &expr)
 
void  do_atomic_begin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_atomic_end (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_create_thread (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_array_equal (const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_array_op (const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_printf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_scanf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_input (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_output (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_prob_coin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_prob_uniform (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 
void  do_havoc_slice (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
 
void  do_alloca (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
  alloca allocates memory that is freed when leaving the function (and not the block, as regular destructors would do).
 
exprt  get_array_argument (const exprt &src)
 
- Static Protected Member Functions inherited from goto_convertt
static bool  needs_cleaning (const exprt &expr)
  Returns 'true' for expressions that may change the program state.
 
static bool  assignment_lhs_needs_temporary (const exprt &lhs)
 
static void  replace_new_object (const exprt &object, exprt &dest)
 
static void  collect_operands (const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
 
- Protected Attributes inherited from goto_convertt
symbol_table_baset &  symbol_table
 
namespacet  ns
 
std::string  tmp_symbol_prefix
 
lifetimet  lifetime = lifetimet::STATIC_GLOBAL
 
struct goto_convertt::targetst  targets
 
- Protected Attributes inherited from messaget
message_handlert *  message_handler
 
mstreamt  mstream
 

Detailed Description

Class that allows to clean expressions of side effects and to generate havoc_slice expressions.

Definition at line 34 of file utils.h.

Constructor & Destructor Documentation

◆  cleanert()

cleanert::cleanert ( symbol_table_baset &  _symbol_table,
message_handlert &  _message_handler 
)
inline

Definition at line 37 of file utils.h.

Member Function Documentation

◆  clean()

std::list< irep_idt > cleanert::clean ( exprt &  guard,
goto_programt &  dest,
const irep_idt &  mode 
)
inline

Definition at line 45 of file utils.h.

◆  do_havoc_slice()

void cleanert::do_havoc_slice ( const symbol_exprt &  function,
const exprt::operandst &  arguments,
goto_programt &  dest,
const irep_idt &  mode 
)
inline

Definition at line 52 of file utils.h.

The documentation for this class was generated from the following file:
  • /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/utils.h

AltStyle によって変換されたページ (->オリジナル) /