CBMC
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:

Public Member Functions

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

Protected Types

enum  whatt { whatt::IS_ZERO, whatt::LENGTH, whatt::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
 
void make_type (exprt &dest, const typet &type)
 
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 33 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 52 of file string_abstraction.h.

◆ localst

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

Definition at line 147 of file string_abstraction.h.

Member Enumeration Documentation

◆ whatt

enum string_abstractiont::whatt
strongprotected
Enumerator
IS_ZERO 
LENGTH 
SIZE 

Definition at line 116 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 252 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 473 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 523 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 1190 of file string_abstraction.cpp.

◆ abstract_function_call()

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

Definition at line 551 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 1149 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 406 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 220 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 193 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 183 of file string_abstraction.cpp.

◆ build() [1/2]

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

Definition at line 790 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 643 of file string_abstraction.cpp.

◆ build_abstraction_type()

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

Definition at line 686 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 704 of file string_abstraction.cpp.

◆ build_array()

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

Definition at line 899 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 871 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 1049 of file string_abstraction.cpp.

◆ build_pointer()

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

Definition at line 925 of file string_abstraction.cpp.

◆ build_symbol()

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

Definition at line 1009 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 1081 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 982 of file string_abstraction.cpp.

◆ build_unknown() [2/2]

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

Definition at line 958 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 1253 of file string_abstraction.cpp.

◆ declare_define_locals()

void string_abstractiont::declare_define_locals ( goto_programt &  dest)
protected

Definition at line 267 of file string_abstraction.cpp.

◆ has_string_macros()

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

Definition at line 598 of file string_abstraction.cpp.

◆ is_char_type()

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

Definition at line 66 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 302 of file string_abstraction.cpp.

◆ make_type()

void string_abstractiont::make_type ( exprt &  dest,
const typet &  type 
)
inlineprotected

Definition at line 77 of file string_abstraction.h.

◆ 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 333 of file string_abstraction.cpp.

◆ member()

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

Definition at line 1408 of file string_abstraction.cpp.

◆ move_lhs_arithmetic()

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

Definition at line 1123 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 612 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 1287 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 1334 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 1365 of file string_abstraction.cpp.

Member Data Documentation

◆ abstraction_types_map

abstraction_types_mapt string_abstractiont::abstraction_types_map
protected

Definition at line 53 of file string_abstraction.h.

◆ goto_model

goto_modelt& string_abstractiont::goto_model
protected

Definition at line 47 of file string_abstraction.h.

◆ initialization

goto_programt string_abstractiont::initialization
protected

Definition at line 145 of file string_abstraction.h.

◆ locals

localst string_abstractiont::locals
protected

Definition at line 148 of file string_abstraction.h.

◆ message_handler

message_handlert& string_abstractiont::message_handler
protected

Definition at line 50 of file string_abstraction.h.

◆ ns

namespacet string_abstractiont::ns
protected

Definition at line 48 of file string_abstraction.h.

◆ parameter_map

localst string_abstractiont::parameter_map
protected

Definition at line 149 of file string_abstraction.h.

◆ string_struct

typet string_abstractiont::string_struct
protected

Definition at line 144 of file string_abstraction.h.

◆ sym_suffix

std::string string_abstractiont::sym_suffix
protected

Definition at line 46 of file string_abstraction.h.

◆ temporary_counter

unsigned string_abstractiont::temporary_counter
protected

Definition at line 49 of file string_abstraction.h.

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