dfcc_utils.h

Go to the documentation of this file.

/*******************************************************************\
 
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);
 
  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);
 
  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);
};
 
#endif