cprover
function_pointer_restrictionst Class Reference

#include <restrict_function_pointers.h>

+ Collaboration diagram for function_pointer_restrictionst:

Classes

class  invalid_restriction_exceptiont
 

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)
 
static function_pointer_restrictionst read_from_file (const std::string &filename, 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, message_handlert &message_handler)
 
static restrictionst parse_function_pointer_restrictions_from_command_line (const std::list< std::string > &restriction_opts)
 
static restrictionst parse_function_pointer_restrictions (const std::list< std::string > &restriction_opts, const std::string &option)
 
static restrictiont parse_function_pointer_restriction (const std::string &restriction_opt, const std::string &option)
 
static optionalt< restrictiontget_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 67 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 70 of file restrict_function_pointers.h.

◆ restrictiont

using function_pointer_restrictionst::restrictiont = restrictionst::value_type

Definition at line 72 of file restrict_function_pointers.h.

Member Function Documentation

◆ from_json()

function_pointer_restrictionst function_pointer_restrictionst::from_json ( const jsont json)
static

Definition at line 496 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 439 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 396 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 589 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 260 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 
)
staticprotected

Definition at line 336 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 
)
staticprotected

Definition at line 282 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)
staticprotected

Definition at line 309 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,
message_handlert message_handler 
)
staticprotected

Definition at line 318 of file restrict_function_pointers.cpp.

◆ read_from_file()

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

Definition at line 535 of file restrict_function_pointers.cpp.

◆ to_json()

jsont function_pointer_restrictionst::to_json ( ) const

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

◆ write_to_file()

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

Definition at line 570 of file restrict_function_pointers.cpp.

Member Data Documentation

◆ restrictions

const restrictionst function_pointer_restrictionst::restrictions

Definition at line 74 of file restrict_function_pointers.h.


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