cbmc/dfcc__utils_8h_source.html

/*******************************************************************\


Module: Dynamic frame condition checking for function contracts


Author: Remi Delmas, delmasrd@amazon.com

Date: August 2022


\*******************************************************************/


#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H

#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H


#include <util/message.h>

#include <util/namespace.h>

#include <util/std_expr.h>


#include <set>


class goto_modelt;

class goto_programt;

class message_handlert;

class symbolt;


struct dfcc_utilst

{

  static bool

  function_symbol_exists(const goto_modelt &, const irep_idt &function_id);

  static bool function_symbol_with_body_exists(

    const goto_modelt &,

    const irep_idt &function_id);


  static symbolt &

  get_function_symbol(symbol_table_baset &, const irep_idt &function_id);


  static symbol_exprt create_symbol(

    symbol_table_baset &,

    const typet &type,

    const irep_idt &function_id,

    const std::string &base_name,

    const source_locationt &source_location);


  static const symbolt &create_static_symbol(

    symbol_table_baset &,

    const typet &type,

    const std::string &prefix,

    const std::string &base_name,

    const source_locationt &source_location,

    const irep_idt &mode,

    const irep_idt &module,

    const exprt &initial_value,

    const bool no_nondet_initialization = true);


#if defined(__GNUC__) && __GNUC__ >= 14

  [[gnu::no_dangling]]

#endif

  static const symbolt &

  create_new_parameter_symbol(

    symbol_table_baset &,

    const irep_idt &function_id,

    const std::string &base_name,

    const typet &type);


  static void add_parameter(

    goto_modelt &,

    const symbolt &symbol,

    const irep_idt &function_id);


  static const symbolt &add_parameter(

    goto_modelt &,

    const irep_idt &function_id,

    const std::string &base_name,

    const typet &type);


#if defined(__GNUC__) && __GNUC__ >= 14

  [[gnu::no_dangling]]

#endif

  static const symbolt &

  clone_and_rename_function(

    goto_modelt &goto_model,

    const irep_idt &function_id,

    const irep_idt &new_function_id,

    std::optional<typet> new_return_type);


  static void wrap_function(

    goto_modelt &goto_model,

    const irep_idt &function_id,

    const irep_idt &wrapped_function_id);


  static const exprt make_null_check_expr(const exprt &ptr);


  static exprt make_sizeof_expr(const exprt &expr, const namespacet &);


  static void inline_function(

    goto_modelt &goto_model,

    const irep_idt &function_id,

    message_handlert &message_handler);


  static void inline_function(

    goto_modelt &goto_model,

    const irep_idt &function_id,

    std::set<irep_idt> &no_body,

    std::set<irep_idt> &recursive_call,

    std::set<irep_idt> &missing_function,

    std::set<irep_idt> &not_enough_arguments,

    message_handlert &message_handler);


  static void inline_program(

    goto_modelt &goto_model,

    goto_programt &goto_program,

    std::set<irep_idt> &no_body,

    std::set<irep_idt> &recursive_call,

    std::set<irep_idt> &missing_function,

    std::set<irep_idt> &not_enough_arguments,

    message_handlert &message_handler);

};

struct dfcc_utilst {…};


#endif

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

ait::ait
ait()
Definition ai.h:565

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38

exprt
Base class for all expressions.
Definition expr.h:56

goto_modelt
Definition goto_model.h:27

goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:73

message_handlert
Definition message.h:27

namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91

source_locationt
Definition source_location.h:20

symbol_exprt
Expression to hold a symbol (variable)
Definition std_expr.h:131

symbol_table_baset
The symbol table base class interface.
Definition symbol_table_base.h:23

symbolt
Symbol table entry.
Definition symbol.h:28

typet
The type of an expression, extends irept.
Definition type.h:29

namespace.h

message.h

std_expr.h
API to expression classes.

dfcc_utilst
Definition dfcc_utils.h:28

dfcc_utilst::get_function_symbol
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Definition dfcc_utils.cpp:72

dfcc_utilst::inline_function
static void inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
Inlines the given function, aborts on recursive calls during inlining.
Definition dfcc_utils.cpp:443

dfcc_utilst::function_symbol_with_body_exists
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
Definition dfcc_utils.cpp:65

dfcc_utilst::make_null_check_expr
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
Definition dfcc_utils.cpp:406

dfcc_utilst::function_symbol_exists
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
Definition dfcc_utils.cpp:58

dfcc_utilst::make_sizeof_expr
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
Definition dfcc_utils.cpp:411

dfcc_utilst::create_new_parameter_symbol
static const symbolt & create_new_parameter_symbol(symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
Creates a new parameter symbol for the given function_id.
Definition dfcc_utils.cpp:124

dfcc_utilst::wrap_function
static void wrap_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
Given a function to wrap foo and a new name wrapped_foo
Definition dfcc_utils.cpp:324

dfcc_utilst::create_static_symbol
static const symbolt & create_static_symbol(symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol ...
Definition dfcc_utils.cpp:103

dfcc_utilst::clone_and_rename_function
static const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given ...
Definition dfcc_utils.cpp:300

dfcc_utilst::add_parameter
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
Definition dfcc_utils.cpp:156

dfcc_utilst::inline_program
static void inline_program(goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
Inlines the given program, and returns function symbols that caused warnings.
Definition dfcc_utils.cpp:487

dfcc_utilst::create_symbol
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
Definition dfcc_utils.cpp:81