CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Types | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
string_abstractiont Class Reference

Replace all uses of char * by a struct that carries that string, and also the underlying allocation and the C string length. More...

#include <string_abstraction.h>

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

Public Member Functions

  string_abstractiont (goto_modelt &goto_model, message_handlert &_message_handler)
  Apply string abstraction to goto_model.
 
void  apply ()
 

Protected Types

enum class   whatt { IS_ZERO , LENGTH , SIZE }
 
typedef ::std::map< typet, typet >  abstraction_types_mapt
 
typedef std::unordered_map< irep_idt, irep_idt >  localst
 

Protected Member Functions

void  apply (goto_programt &dest)
 
void  replace_string_macros (exprt &expr, bool lhs, const source_locationt &)
 
void  move_lhs_arithmetic (exprt &lhs, exprt &rhs)
 
bool  is_char_type (const typet &type) const
 
bool  is_ptr_string_struct (const typet &type) const
 
goto_programt::targett  abstract (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett  abstract_assign (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett  abstract_pointer_assign (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett  abstract_char_assign (goto_programt &dest, goto_programt::targett it)
 
goto_programt::targett  char_assign (goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
 
void  abstract_function_call (goto_programt::targett it)
 
goto_programt::targett  value_assignments (goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
 
goto_programt::targett  value_assignments_if (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
 
goto_programt::targett  value_assignments_string_struct (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
 
exprt  build (const exprt &pointer, whatt what, bool write, const source_locationt &)
 
bool  build (const exprt &object, exprt &dest, bool write)
 
bool  build_wrap (const exprt &object, exprt &dest, bool write)
 
bool  build_if (const if_exprt &o_if, exprt &dest, bool write)
 
bool  build_array (const array_exprt &object, exprt &dest, bool write)
 
bool  build_symbol (const symbol_exprt &sym, exprt &dest)
 
bool  build_symbol_constant (const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
 
exprt  build_unknown (whatt what, bool write)
 
exprt  build_unknown (const typet &type, bool write)
 
const typet &  build_abstraction_type (const typet &type)
 
const typet &  build_abstraction_type_rec (const typet &type, const abstraction_types_mapt &known)
 
bool  build_pointer (const exprt &object, exprt &dest, bool write)
 
void  build_new_symbol (const symbolt &symbol, const irep_idt &identifier, const typet &type)
 
exprt  member (const exprt &a, whatt what)
 
void  abstract (goto_programt &dest)
 
void  add_str_parameters (symbolt &fct_symbol, goto_functiont::parameter_identifierst &parameter_identifiers)
 
code_typet::parametert  add_parameter (const symbolt &fct_symbol, const typet &type, const irep_idt &identifier)
 
void  make_decl_and_def (goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
 
exprt  make_val_or_dummy_rec (goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
 
symbol_exprt  add_dummy_symbol_and_value (goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const irep_idt &component_name, const typet &type, const typet &source_type)
 
void  declare_define_locals (goto_programt &dest)
 

Static Protected Member Functions

static bool  has_string_macros (const exprt &expr)
 
static typet  build_type (whatt what)
 

Protected Attributes

std::string  sym_suffix
 
goto_modelt &  goto_model
 
namespacet  ns
 
unsigned  temporary_counter
 
message_handlert &  message_handler
 
abstraction_types_mapt  abstraction_types_map
 
typet  string_struct
 
goto_programt  initialization
 
localst  locals
 
localst  parameter_map
 

Detailed Description

Replace all uses of char * by a struct that carries that string, and also the underlying allocation and the C string length.

This will become useful (with some modifications) for supporting strings in the C frontend, as the string solver expects a struct that bundles the string length and the underlying character array.

Definition at line 32 of file string_abstraction.h.

Member Typedef Documentation

◆  abstraction_types_mapt

typedef ::std::map< typet, typet > string_abstractiont::abstraction_types_mapt
protected

Definition at line 51 of file string_abstraction.h.

◆  localst

typedef std::unordered_map<irep_idt, irep_idt> string_abstractiont::localst
protected

Definition at line 139 of file string_abstraction.h.

Member Enumeration Documentation

◆  whatt

enum class string_abstractiont::whatt
strongprotected
Enumerator
IS_ZERO 
LENGTH 
SIZE 

Definition at line 108 of file string_abstraction.h.

Constructor & Destructor Documentation

◆  string_abstractiont()

string_abstractiont::string_abstractiont ( goto_modelt &  goto_model,
message_handlert &  _message_handler 
)

Apply string abstraction to goto_model.

If any abstractions are to be applied, the affected goto_functions and any affected symbols will be modified.

Definition at line 79 of file string_abstraction.cpp.

Member Function Documentation

◆  abstract() [1/2]

void string_abstractiont::abstract ( goto_programt &  dest )
protected

Definition at line 251 of file string_abstraction.cpp.

◆  abstract() [2/2]

goto_programt::targett string_abstractiont::abstract ( goto_programt &  dest,
goto_programt::targett  it 
)
protected

Definition at line 462 of file string_abstraction.cpp.

◆  abstract_assign()

goto_programt::targett string_abstractiont::abstract_assign ( goto_programt &  dest,
goto_programt::targett  it 
)
protected

Definition at line 512 of file string_abstraction.cpp.

◆  abstract_char_assign()

goto_programt::targett string_abstractiont::abstract_char_assign ( goto_programt &  dest,
goto_programt::targett  it 
)
protected

Definition at line 1186 of file string_abstraction.cpp.

◆  abstract_function_call()

void string_abstractiont::abstract_function_call ( goto_programt::targett  it )
protected

Definition at line 540 of file string_abstraction.cpp.

◆  abstract_pointer_assign()

goto_programt::targett string_abstractiont::abstract_pointer_assign ( goto_programt &  dest,
goto_programt::targett  it 
)
protected

Definition at line 1147 of file string_abstraction.cpp.

◆  add_dummy_symbol_and_value()

symbol_exprt string_abstractiont::add_dummy_symbol_and_value ( goto_programt &  dest,
goto_programt::targett  ref_instr,
const symbolt &  symbol,
const irep_idt &  component_name,
const typet &  type,
const typet &  source_type 
)
protected

Definition at line 397 of file string_abstraction.cpp.

◆  add_parameter()

code_typet::parametert string_abstractiont::add_parameter ( const symbolt &  fct_symbol,
const typet &  type,
const irep_idt &  identifier 
)
protected

Definition at line 219 of file string_abstraction.cpp.

◆  add_str_parameters()

void string_abstractiont::add_str_parameters ( symbolt &  fct_symbol,
goto_functiont::parameter_identifierst &  parameter_identifiers 
)
protected

Definition at line 192 of file string_abstraction.cpp.

◆  apply() [1/2]

void string_abstractiont::apply ( )

Definition at line 130 of file string_abstraction.cpp.

◆  apply() [2/2]

void string_abstractiont::apply ( goto_programt &  dest )
protected

Definition at line 182 of file string_abstraction.cpp.

◆  build() [1/2]

bool string_abstractiont::build ( const exprt &  object,
exprt &  dest,
bool  write 
)
protected

Definition at line 784 of file string_abstraction.cpp.

◆  build() [2/2]

exprt string_abstractiont::build ( const exprt &  pointer,
whatt  what,
bool  write,
const source_locationt &  source_location 
)
protected

Definition at line 634 of file string_abstraction.cpp.

◆  build_abstraction_type()

const typet & string_abstractiont::build_abstraction_type ( const typet &  type )
protected

Definition at line 677 of file string_abstraction.cpp.

◆  build_abstraction_type_rec()

const typet & string_abstractiont::build_abstraction_type_rec ( const typet &  type,
const abstraction_types_mapt &  known 
)
protected

Definition at line 695 of file string_abstraction.cpp.

◆  build_array()

bool string_abstractiont::build_array ( const array_exprt &  object,
exprt &  dest,
bool  write 
)
protected

Definition at line 893 of file string_abstraction.cpp.

◆  build_if()

bool string_abstractiont::build_if ( const if_exprt &  o_if,
exprt &  dest,
bool  write 
)
protected

Definition at line 865 of file string_abstraction.cpp.

◆  build_new_symbol()

void string_abstractiont::build_new_symbol ( const symbolt &  symbol,
const irep_idt &  identifier,
const typet &  type 
)
protected

Definition at line 1043 of file string_abstraction.cpp.

◆  build_pointer()

bool string_abstractiont::build_pointer ( const exprt &  object,
exprt &  dest,
bool  write 
)
protected

Definition at line 919 of file string_abstraction.cpp.

◆  build_symbol()

bool string_abstractiont::build_symbol ( const symbol_exprt &  sym,
exprt &  dest 
)
protected

Definition at line 1003 of file string_abstraction.cpp.

◆  build_symbol_constant()

bool string_abstractiont::build_symbol_constant ( const mp_integer &  zero_length,
const mp_integer &  buf_size,
exprt &  dest 
)
protected

Definition at line 1079 of file string_abstraction.cpp.

◆  build_type()

typet string_abstractiont::build_type ( whatt  what )
staticprotected

Definition at line 114 of file string_abstraction.cpp.

◆  build_unknown() [1/2]

exprt string_abstractiont::build_unknown ( const typet &  type,
bool  write 
)
protected

Definition at line 976 of file string_abstraction.cpp.

◆  build_unknown() [2/2]

exprt string_abstractiont::build_unknown ( whatt  what,
bool  write 
)
protected

Definition at line 952 of file string_abstraction.cpp.

◆  build_wrap()

bool string_abstractiont::build_wrap ( const exprt &  object,
exprt &  dest,
bool  write 
)
protected

Definition at line 29 of file string_abstraction.cpp.

◆  char_assign()

goto_programt::targett string_abstractiont::char_assign ( goto_programt &  dest,
goto_programt::targett  target,
const exprt &  new_lhs,
const exprt &  lhs,
const exprt &  rhs 
)
protected

Definition at line 1247 of file string_abstraction.cpp.

◆  declare_define_locals()

void string_abstractiont::declare_define_locals ( goto_programt &  dest )
protected

Definition at line 266 of file string_abstraction.cpp.

◆  has_string_macros()

bool string_abstractiont::has_string_macros ( const exprt &  expr )
staticprotected

Definition at line 587 of file string_abstraction.cpp.

◆  is_char_type()

bool string_abstractiont::is_char_type ( const typet &  type ) const
inlineprotected

Definition at line 65 of file string_abstraction.h.

◆  is_ptr_string_struct()

bool string_abstractiont::is_ptr_string_struct ( const typet &  type ) const
protected

Definition at line 61 of file string_abstraction.cpp.

◆  make_decl_and_def()

void string_abstractiont::make_decl_and_def ( goto_programt &  dest,
goto_programt::targett  ref_instr,
const irep_idt &  identifier,
const irep_idt &  source_sym 
)
protected

Definition at line 301 of file string_abstraction.cpp.

◆  make_val_or_dummy_rec()

exprt string_abstractiont::make_val_or_dummy_rec ( goto_programt &  dest,
goto_programt::targett  ref_instr,
const symbolt &  symbol,
const typet &  source_type 
)
protected

Definition at line 330 of file string_abstraction.cpp.

◆  member()

exprt string_abstractiont::member ( const exprt &  a,
whatt  what 
)
protected

Definition at line 1392 of file string_abstraction.cpp.

◆  move_lhs_arithmetic()

void string_abstractiont::move_lhs_arithmetic ( exprt &  lhs,
exprt &  rhs 
)
protected

Definition at line 1121 of file string_abstraction.cpp.

◆  replace_string_macros()

void string_abstractiont::replace_string_macros ( exprt &  expr,
bool  lhs,
const source_locationt &  source_location 
)
protected

Definition at line 603 of file string_abstraction.cpp.

◆  value_assignments()

goto_programt::targett string_abstractiont::value_assignments ( goto_programt &  dest,
goto_programt::targett  it,
const exprt &  lhs,
const exprt &  rhs 
)
protected

Definition at line 1277 of file string_abstraction.cpp.

◆  value_assignments_if()

goto_programt::targett string_abstractiont::value_assignments_if ( goto_programt &  dest,
goto_programt::targett  target,
const exprt &  lhs,
const if_exprt &  rhs 
)
protected

Definition at line 1324 of file string_abstraction.cpp.

◆  value_assignments_string_struct()

goto_programt::targett string_abstractiont::value_assignments_string_struct ( goto_programt &  dest,
goto_programt::targett  target,
const exprt &  lhs,
const exprt &  rhs 
)
protected

Definition at line 1355 of file string_abstraction.cpp.

Member Data Documentation

◆  abstraction_types_map

abstraction_types_mapt string_abstractiont::abstraction_types_map
protected

Definition at line 52 of file string_abstraction.h.

◆  goto_model

goto_modelt& string_abstractiont::goto_model
protected

Definition at line 46 of file string_abstraction.h.

◆  initialization

goto_programt string_abstractiont::initialization
protected

Definition at line 137 of file string_abstraction.h.

◆  locals

localst string_abstractiont::locals
protected

Definition at line 140 of file string_abstraction.h.

◆  message_handler

message_handlert& string_abstractiont::message_handler
protected

Definition at line 49 of file string_abstraction.h.

◆  ns

namespacet string_abstractiont::ns
protected

Definition at line 47 of file string_abstraction.h.

◆  parameter_map

localst string_abstractiont::parameter_map
protected

Definition at line 141 of file string_abstraction.h.

◆  string_struct

typet string_abstractiont::string_struct
protected

Definition at line 136 of file string_abstraction.h.

◆  sym_suffix

std::string string_abstractiont::sym_suffix
protected

Definition at line 45 of file string_abstraction.h.

◆  temporary_counter

unsigned string_abstractiont::temporary_counter
protected

Definition at line 48 of file string_abstraction.h.

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

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