cprover
Loading...
Searching...
No Matches
restrict_function_pointers.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Restrict function pointers
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
16
17#ifndef CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
18#define CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
19
20#include <unordered_map>
21#include <unordered_set>
22
24#include <util/irep.h>
25#include <util/optional.h>
26
27#include "goto_program.h"
28
29class cmdlinet;
30class goto_functiont;
31class goto_modelt;
32class jsont;
34class optionst;
35
36#define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer"
37#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
38 "function-pointer-restrictions-file"
39#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \
40 "restrict-function-pointer-by-name"
41
42#define OPT_RESTRICT_FUNCTION_POINTER \
43 "(" RESTRICT_FUNCTION_POINTER_OPT \
44 "):" \
45 "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
46 "):" \
47 "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):"
48
49#define HELP_RESTRICT_FUNCTION_POINTER \
50 " {y--" RESTRICT_FUNCTION_POINTER_OPT \
51 "} " \
52 "{upointer_name}/{utarget[,targets]*} \t " \
53 "restrict a function pointer to a set of possible targets; targets must " \
54 "all exist in the symbol table with a matching type; works for globals " \
55 "and function parameters right now\n" \
56 " {y--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \
57 "} {ufile_name} \t " \
58 "add function pointer restrictions from file {ufile_name}\n" \
59 " {y--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \
60 "} " \
61 "{usymbol_name}/{utarget[targets]*} \t " \
62 "restrict a function pointer where {usymbol_name} is the unmangled " \
63 "name, before labelling function pointers\n"
64
66 const cmdlinet &cmdline,
67 optionst &options);
68
70{
71public:
73 std::string reason,
74 std::string correct_format = "");
75
76 std::string what() const override;
77
78 std::string correct_format;
79};
80
82{
83public:
85 std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
86 using restrictiont = restrictionst::value_type;
87
89
92 const optionst &options,
93 const goto_modelt &goto_model,
94 message_handlert &message_handler);
95
96 jsont to_json() const;
98 from_json(const jsont &json, const goto_modelt &goto_model);
99
101 const std::string &filename,
102 const goto_modelt &goto_model,
103 message_handlert &message_handler);
104
105 void write_to_file(const std::string &filename) const;
106
107protected:
109 const goto_modelt &goto_model,
111
113 restrictionst lhs,
114 const restrictionst &rhs);
115
117 const std::list<std::string> &filenames,
118 const goto_modelt &goto_model,
119 message_handlert &message_handler);
120
122 const std::list<std::string> &restriction_opts,
123 const goto_modelt &goto_model);
124
126 const std::list<std::string> &restriction_opts,
127 const std::string &option,
128 const goto_modelt &goto_model);
129
131 const std::string &restriction_opt,
132 const std::string &option,
133 const goto_modelt &goto_model);
134
136 const goto_functiont &goto_function,
137 const function_pointer_restrictionst::restrictionst &by_name_restrictions,
138 const goto_programt::const_targett &location);
139
153 const std::list<std::string> &restriction_name_opts,
154 const goto_modelt &goto_model);
155};
156
166 message_handlert &message_handler,
167 goto_modelt &goto_model,
168 const optionst &options);
169
170#endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
std::string reason
The reason this exception was generated.
Definition c_errors.h:83
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.
static restrictionst parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts, const goto_modelt &goto_model)
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(const std::list< std::string > &restriction_opts, const std::string &option, const goto_modelt &goto_model)
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option, 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)
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)
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > restrictionst
static restrictionst parse_function_pointer_restrictions_from_file(const std::list< std::string > &filenames, const goto_modelt &goto_model, message_handlert &message_handler)
void write_to_file(const std::string &filename) const
static void typecheck_function_pointer_restrictions(const goto_modelt &goto_model, const restrictionst &restrictions)
static function_pointer_restrictionst from_json(const jsont &json, const goto_modelt &goto_model)
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
instructionst::const_iterator const_targett
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
std::string what() const override
A human readable description of what went wrong.
Definition json.h:27
Concrete Goto Program.
nonstd::optional< T > optionalt
Definition optional.h:35
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
void restrict_function_pointers(message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
Apply function pointer restrictions to a goto_model.