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 optionalt< 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 85 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 89 of file restrict_function_pointers.h.

◆ restrictiont

using function_pointer_restrictionst::restrictiont = restrictionst::value_type

Definition at line 90 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 529 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 468 of file restrict_function_pointers.cpp.

◆ get_by_name_restriction()

optionalt< 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 425 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 627 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 222 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 362 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 244 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 273 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 282 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 572 of file restrict_function_pointers.cpp.

◆ to_json()

jsont function_pointer_restrictionst::to_json ( ) const

Definition at line 589 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 109 of file restrict_function_pointers.cpp.

◆ write_to_file()

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

Definition at line 608 of file restrict_function_pointers.cpp.

Member Data Documentation

◆ restrictions

const restrictionst function_pointer_restrictionst::restrictions

Definition at line 92 of file restrict_function_pointers.h.

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