Go to the documentation of this file.
17 #ifndef CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
18 #define CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
20 #include <unordered_map>
21 #include <unordered_set>
29 #define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer"
30 #define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
31 "function-pointer-restrictions-file"
32 #define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \
33 "restrict-function-pointer-by-name"
35 #define OPT_RESTRICT_FUNCTION_POINTER \
36 "(" RESTRICT_FUNCTION_POINTER_OPT \
38 "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
40 "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):"
42 #define HELP_RESTRICT_FUNCTION_POINTER \
43 "--" RESTRICT_FUNCTION_POINTER_OPT \
44 " <pointer_name>/<target[,targets]*>\n" \
45 " restrict a function pointer to a set of possible targets\n" \
46 " targets must all exist in the symbol table with a matching " \
48 " works for globals and function parameters right now\n" \
49 "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
51 " add function pointer restrictions from file"
64 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
79 const std::string &filename,
92 std::string
what()
const override;
107 const std::list<std::string> &filenames,
111 const std::list<std::string> &restriction_opts);
114 const std::list<std::string> &restriction_opts,
115 const std::string &option);
118 const std::string &restriction_opt,
119 const std::string &option);
139 const std::list<std::string> &restriction_name_opts,
155 #endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
static function_pointer_restrictionst read_from_file(const std::string &filename, message_handlert &message_handler)
std::string what() const override
A human readable description of what went wrong.
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.
const restrictionst restrictions
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.
static restrictionst parse_function_pointer_restrictions_from_file(const std::list< std::string > &filenames, message_handlert &message_handler)
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > restrictionst
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)
A goto function, consisting of function type (see type), function body (see body),...
restrictionst::value_type restrictiont
nonstd::optional< T > optionalt
static restrictionst parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts)
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
std::string correct_format
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
static void typecheck_function_pointer_restrictions(const goto_modelt &goto_model, const restrictionst &restrictions)
void write_to_file(const std::string &filename) const
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 function_pointer_restrictionst from_json(const jsont &json)
instructionst::const_iterator const_targett
Base class for exceptions thrown in the cprover project.