CBMC
Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Static Protected Member Functions | List of all members
function_pointer_restrictionst Class Reference

#include <restrict_function_pointers.h>

+ Collaboration diagram for function_pointer_restrictionst:

Public Types

using restrictionst = std::unordered_map< irep_idt, std::unordered_set< irep_idt > >
 
using restrictiont = restrictionst::value_type
 

Public Member Functions

jsont to_json () const
 
void write_to_file (const std::string &filename) const
 

Static Public Member Functions

static function_pointer_restrictionst from_options (const optionst &options, const goto_modelt &goto_model, message_handlert &message_handler)
 Parse function pointer restrictions from command line. More...
 
static function_pointer_restrictionst from_json (const jsont &json, const goto_modelt &goto_model)
 
static function_pointer_restrictionst read_from_file (const std::string &filename, const goto_modelt &goto_model, message_handlert &message_handler)
 

Public Attributes

const restrictionst restrictions
 

Static Protected Member Functions

static void typecheck_function_pointer_restrictions (const goto_modelt &goto_model, const restrictionst &restrictions)
 
static restrictionst merge_function_pointer_restrictions (restrictionst lhs, const restrictionst &rhs)
 
static restrictionst parse_function_pointer_restrictions_from_file (const std::list< std::string > &filenames, const goto_modelt &goto_model, message_handlert &message_handler)
 
static restrictionst parse_function_pointer_restrictions_from_command_line (const std::list< std::string > &restriction_opts, const goto_modelt &goto_model)
 
static restrictionst parse_function_pointer_restrictions (const std::list< std::string > &restriction_opts, const std::string &option, const goto_modelt &goto_model)
 
static restrictiont parse_function_pointer_restriction (const std::string &restriction_opt, const std::string &option, const goto_modelt &goto_model)
 
static std::optional< restrictiont > get_by_name_restriction (const goto_functiont &goto_function, const function_pointer_restrictionst::restrictionst &by_name_restrictions, const goto_programt::const_targett &location)
 
static restrictionst get_function_pointer_by_name_restrictions (const std::list< std::string > &restriction_name_opts, const goto_modelt &goto_model)
 Get function pointer restrictions from restrictions with named pointers. More...
 

Detailed Description

Definition at line 80 of file restrict_function_pointers.h.

Member Typedef Documentation

◆ restrictionst

using function_pointer_restrictionst::restrictionst = std::unordered_map<irep_idt, std::unordered_set<irep_idt> >

Definition at line 83 of file restrict_function_pointers.h.

◆ restrictiont

using function_pointer_restrictionst::restrictiont = restrictionst::value_type

Definition at line 85 of file restrict_function_pointers.h.

Member Function Documentation

◆ from_json()

function_pointer_restrictionst function_pointer_restrictionst::from_json ( const jsont &  json,
const goto_modelt &  goto_model 
)
static

Definition at line 535 of file restrict_function_pointers.cpp.

◆ from_options()

function_pointer_restrictionst function_pointer_restrictionst::from_options ( const optionst &  options,
const goto_modelt &  goto_model,
message_handlert &  message_handler 
)
static

Parse function pointer restrictions from command line.

Definition at line 474 of file restrict_function_pointers.cpp.

◆ get_by_name_restriction()

std::optional< function_pointer_restrictionst::restrictiont > function_pointer_restrictionst::get_by_name_restriction ( const goto_functiont &  goto_function,
const function_pointer_restrictionst::restrictionst &  by_name_restrictions,
const goto_programt::const_targett &  location 
)
staticprotected

Definition at line 431 of file restrict_function_pointers.cpp.

◆ get_function_pointer_by_name_restrictions()

function_pointer_restrictionst::restrictionst function_pointer_restrictionst::get_function_pointer_by_name_restrictions ( const std::list< std::string > &  restriction_name_opts,
const goto_modelt &  goto_model 
)
staticprotected

Get function pointer restrictions from restrictions with named pointers.

This takes a list of restrictions, with each restriction consisting of a function pointer name, and the list of target functions. That is, each input restriction is of the form <fp-name>/<target>(,<target>)*. The method then returns a restrictionst object constructed from the given list of restrictions

Parameters
restriction_name_optsrestrictions
goto_modelgoto model with labelled function pointer calls
Returns
function pointer restrictions in the internal format that is understood by other methods in this class

Definition at line 633 of file restrict_function_pointers.cpp.

◆ merge_function_pointer_restrictions()

function_pointer_restrictionst::restrictionst function_pointer_restrictionst::merge_function_pointer_restrictions ( function_pointer_restrictionst::restrictionst  lhs,
const restrictionst &  rhs 
)
staticprotected

Definition at line 228 of file restrict_function_pointers.cpp.

◆ parse_function_pointer_restriction()

function_pointer_restrictionst::restrictiont function_pointer_restrictionst::parse_function_pointer_restriction ( const std::string &  restriction_opt,
const std::string &  option,
const goto_modelt &  goto_model 
)
staticprotected

Definition at line 368 of file restrict_function_pointers.cpp.

◆ parse_function_pointer_restrictions()

function_pointer_restrictionst::restrictionst function_pointer_restrictionst::parse_function_pointer_restrictions ( const std::list< std::string > &  restriction_opts,
const std::string &  option,
const goto_modelt &  goto_model 
)
staticprotected

Definition at line 250 of file restrict_function_pointers.cpp.

◆ parse_function_pointer_restrictions_from_command_line()

function_pointer_restrictionst::restrictionst function_pointer_restrictionst::parse_function_pointer_restrictions_from_command_line ( const std::list< std::string > &  restriction_opts,
const goto_modelt &  goto_model 
)
staticprotected

Definition at line 278 of file restrict_function_pointers.cpp.

◆ parse_function_pointer_restrictions_from_file()

function_pointer_restrictionst::restrictionst function_pointer_restrictionst::parse_function_pointer_restrictions_from_file ( const std::list< std::string > &  filenames,
const goto_modelt &  goto_model,
message_handlert &  message_handler 
)
staticprotected

Definition at line 288 of file restrict_function_pointers.cpp.

◆ read_from_file()

function_pointer_restrictionst function_pointer_restrictionst::read_from_file ( const std::string &  filename,
const goto_modelt &  goto_model,
message_handlert &  message_handler 
)
static

Definition at line 578 of file restrict_function_pointers.cpp.

◆ to_json()

jsont function_pointer_restrictionst::to_json ( ) const

Definition at line 595 of file restrict_function_pointers.cpp.

◆ typecheck_function_pointer_restrictions()

void function_pointer_restrictionst::typecheck_function_pointer_restrictions ( const goto_modelt &  goto_model,
const restrictionst &  restrictions 
)
staticprotected

Definition at line 111 of file restrict_function_pointers.cpp.

◆ write_to_file()

void function_pointer_restrictionst::write_to_file ( const std::string &  filename) const

Definition at line 614 of file restrict_function_pointers.cpp.

Member Data Documentation

◆ restrictions

const restrictionst function_pointer_restrictionst::restrictions

Definition at line 87 of file restrict_function_pointers.h.

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