cprover
restrict_function_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Restrict function pointers
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
10 
11 #include <ansi-c/expr2c.h>
12 
13 #include <json/json_parser.h>
14 
15 #include <util/cmdline.h>
16 #include <util/options.h>
17 #include <util/pointer_expr.h>
18 #include <util/string_utils.h>
19 
20 #include "goto_model.h"
21 
22 #include <algorithm>
23 #include <fstream>
24 
25 namespace
26 {
27 source_locationt make_function_pointer_restriction_assertion_source_location(
28  source_locationt source_location,
30 {
31  std::stringstream comment;
32 
33  comment << "dereferenced function pointer at " << restriction.first
34  << " must be ";
35 
36  if(restriction.second.size() == 1)
37  {
38  comment << *restriction.second.begin();
39  }
40  else
41  {
42  comment << "one of [";
43 
45  comment, restriction.second.begin(), restriction.second.end(), ", ");
46 
47  comment << ']';
48  }
49 
50  source_location.set_comment(comment.str());
51  source_location.set_property_class(ID_assertion);
52 
53  return source_location;
54 }
55 
56 template <typename Handler, typename GotoFunctionT>
57 void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
58 {
59  using targett = decltype(goto_function.body.instructions.begin());
61  goto_function,
62  [](targett target) { return target->is_function_call(); },
63  handler);
64 }
65 
66 void restrict_function_pointer(
67  goto_functiont &goto_function,
68  goto_modelt &goto_model,
69  const function_pointer_restrictionst &restrictions,
70  const goto_programt::targett &location)
71 {
72  PRECONDITION(location->is_function_call());
73 
74  // for each function call, we check if it is using a symbol we have
75  // restrictions for, and if so branch on its value and insert concrete calls
76  // to the restriction functions
77 
78  // Check if this is calling a function pointer, and if so if it is one
79  // we have a restriction for
80  const auto &original_function_call = location->get_function_call();
81 
82  if(!can_cast_expr<dereference_exprt>(original_function_call.function()))
83  return;
84 
85  // because we run the label function pointer calls transformation pass before
86  // this stage a dereference can only dereference a symbol expression
87  auto const &called_function_pointer =
88  to_dereference_expr(original_function_call.function()).pointer();
89  PRECONDITION(can_cast_expr<symbol_exprt>(called_function_pointer));
90  auto const &pointer_symbol = to_symbol_expr(called_function_pointer);
91  auto const restriction_iterator =
92  restrictions.restrictions.find(pointer_symbol.get_identifier());
93 
94  if(restriction_iterator == restrictions.restrictions.end())
95  return;
96 
97  auto const &restriction = *restriction_iterator;
98 
99  // this is intentionally a copy because we're about to change the
100  // instruction this iterator points to
101  // if we can, we will replace uses of it by a case distinction over
102  // given functions the function pointer can point to
103  auto const original_function_call_instruction = *location;
104 
105  *location = goto_programt::make_assertion(
106  false_exprt{},
107  make_function_pointer_restriction_assertion_source_location(
108  original_function_call_instruction.source_location, restriction));
109 
110  auto const assume_false_location = goto_function.body.insert_after(
111  location,
113  false_exprt{}, original_function_call_instruction.source_location));
114 
115  // this is mutable because we'll update this at the end of each
116  // loop iteration to always point at the start of the branch
117  // we created
118  auto else_location = location;
119 
120  auto const end_if_location = goto_function.body.insert_after(
121  assume_false_location, goto_programt::make_skip());
122 
123  for(auto const &restriction_target : restriction.second)
124  {
125  auto new_instruction = original_function_call_instruction;
126  // can't use get_function_call because that'll return a const ref
127  const symbol_exprt &function_pointer_target_symbol_expr =
128  goto_model.symbol_table.lookup_ref(restriction_target).symbol_expr();
129  to_code_function_call(new_instruction.code_nonconst()).function() =
130  function_pointer_target_symbol_expr;
131  auto const goto_end_if_location = goto_function.body.insert_before(
132  else_location,
134  end_if_location, original_function_call_instruction.source_location));
135  auto const replaced_instruction_location =
136  goto_function.body.insert_before(goto_end_if_location, new_instruction);
137  else_location = goto_function.body.insert_before(
138  replaced_instruction_location,
140  else_location,
141  notequal_exprt{pointer_symbol,
142  address_of_exprt{function_pointer_target_symbol_expr}}));
143  }
144 }
145 } // namespace
146 
148  invalid_restriction_exceptiont(std::string reason, std::string correct_format)
149  : reason(std::move(reason)), correct_format(std::move(correct_format))
150 {
151 }
152 
153 std::string
155 {
156  std::string res;
157 
158  res += "Invalid restriction";
159  res += "\nReason: " + reason;
160 
161  if(!correct_format.empty())
162  {
163  res += "\nFormat: " + correct_format;
164  }
165 
166  return res;
167 }
168 
170  const goto_modelt &goto_model,
172 {
173  for(auto const &restriction : restrictions)
174  {
175  auto const function_pointer_sym =
176  goto_model.symbol_table.lookup(restriction.first);
177  if(function_pointer_sym == nullptr)
178  {
179  throw invalid_restriction_exceptiont{id2string(restriction.first) +
180  " not found in the symbol table"};
181  }
182  auto const &function_pointer_type = function_pointer_sym->type;
183  if(function_pointer_type.id() != ID_pointer)
184  {
185  throw invalid_restriction_exceptiont{"not a function pointer: " +
186  id2string(restriction.first)};
187  }
188  auto const &function_type =
189  to_pointer_type(function_pointer_type).subtype();
190  if(function_type.id() != ID_code)
191  {
192  throw invalid_restriction_exceptiont{"not a function pointer: " +
193  id2string(restriction.first)};
194  }
195  auto const &ns = namespacet{goto_model.symbol_table};
196  for(auto const &function_pointer_target : restriction.second)
197  {
198  auto const function_pointer_target_sym =
199  goto_model.symbol_table.lookup(function_pointer_target);
200  if(function_pointer_target_sym == nullptr)
201  {
203  "symbol not found: " + id2string(function_pointer_target)};
204  }
205  auto const &function_pointer_target_type =
206  function_pointer_target_sym->type;
207  if(function_type != function_pointer_target_type)
208  {
210  "type mismatch: `" + id2string(restriction.first) + "' points to `" +
211  type2c(function_type, ns) + "', but restriction `" +
212  id2string(function_pointer_target) + "' has type `" +
213  type2c(function_pointer_target_type, ns) + "'"};
214  }
215  }
216  }
217 }
218 
220  goto_modelt &goto_model,
222 {
223  for(auto &function_item : goto_model.goto_functions.function_map)
224  {
225  goto_functiont &goto_function = function_item.second;
226 
227  for_each_function_call(goto_function, [&](const goto_programt::targett it) {
228  restrict_function_pointer(goto_function, goto_model, restrictions, it);
229  });
230  }
231 }
232 
234  const cmdlinet &cmdline,
235  optionst &options)
236 {
238  {
239  options.set_option(
242  }
243 
245  {
246  options.set_option(
249  }
250 
252  {
253  options.set_option(
256  }
257 }
258 
263 {
264  auto &result = lhs;
265 
266  for(auto const &restriction : rhs)
267  {
268  auto emplace_result = result.emplace(restriction.first, restriction.second);
269  if(!emplace_result.second)
270  {
271  for(auto const &target : restriction.second)
272  {
273  emplace_result.first->second.insert(target);
274  }
275  }
276  }
277 
278  return result;
279 }
280 
283  const std::list<std::string> &restriction_opts,
284  const std::string &option)
285 {
286  auto function_pointer_restrictions =
288 
289  for(const std::string &restriction_opt : restriction_opts)
290  {
291  const auto restriction =
292  parse_function_pointer_restriction(restriction_opt, option);
293 
294  const bool inserted = function_pointer_restrictions
295  .emplace(restriction.first, restriction.second)
296  .second;
297 
298  if(!inserted)
299  {
301  "function pointer restriction for `" + id2string(restriction.first) +
302  "' was specified twice"};
303  }
304  }
305 
306  return function_pointer_restrictions;
307 }
308 
311  const std::list<std::string> &restriction_opts)
312 {
314  restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT);
315 }
316 
319  const std::list<std::string> &filenames,
320  message_handlert &message_handler)
321 {
322  auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
323 
324  for(auto const &filename : filenames)
325  {
326  auto const restrictions = read_from_file(filename, message_handler);
327 
328  merged_restrictions = merge_function_pointer_restrictions(
329  std::move(merged_restrictions), restrictions.restrictions);
330  }
331 
332  return merged_restrictions;
333 }
334 
337  const std::string &restriction_opt,
338  const std::string &option)
339 {
340  // the format for restrictions is <pointer_name>/<target[,more_targets]*>
341  // exactly one pointer and at least one target
342  auto const pointer_name_end = restriction_opt.find('/');
343  auto const restriction_format_message =
344  "the format for restrictions is "
345  "<pointer_name>/<target[,more_targets]*>";
346 
347  if(pointer_name_end == std::string::npos)
348  {
349  throw invalid_restriction_exceptiont{"couldn't find '/' in `" +
350  restriction_opt + "'",
351  restriction_format_message};
352  }
353 
354  if(pointer_name_end == restriction_opt.size())
355  {
357  "couldn't find names of targets after '/' in `" + restriction_opt + "'",
358  restriction_format_message};
359  }
360 
361  if(pointer_name_end == 0)
362  {
364  "couldn't find target name before '/' in `" + restriction_opt + "'"};
365  }
366 
367  auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
368  auto const target_names_substring =
369  restriction_opt.substr(pointer_name_end + 1);
370  auto const target_name_strings = split_string(target_names_substring, ',');
371 
372  if(target_name_strings.size() == 1 && target_name_strings[0].empty())
373  {
375  "missing target list for function pointer restriction " + pointer_name,
376  restriction_format_message};
377  }
378 
379  std::unordered_set<irep_idt> target_names;
380  target_names.insert(target_name_strings.begin(), target_name_strings.end());
381 
382  for(auto const &target_name : target_names)
383  {
384  if(target_name == ID_empty_string)
385  {
387  "leading or trailing comma in restrictions for `" + pointer_name + "'",
388  restriction_format_message);
389  }
390  }
391 
392  return std::make_pair(pointer_name, target_names);
393 }
394 
397  const goto_functiont &goto_function,
398  const function_pointer_restrictionst::restrictionst &by_name_restrictions,
399  const goto_programt::const_targett &location)
400 {
401  PRECONDITION(location->is_function_call());
402 
403  const exprt &function = location->call_function();
404 
405  if(!can_cast_expr<dereference_exprt>(function))
406  return {};
407 
408  // the function pointer is guaranteed to be a symbol expression, as the
409  // label_function_pointer_call_sites() pass (which must be run before the
410  // function pointer restriction) replaces calls via complex pointer
411  // expressions by calls to a function pointer variable
412  auto const &function_pointer_call_site =
413  to_symbol_expr(to_dereference_expr(function).pointer());
414 
415  const goto_programt::const_targett it = std::prev(location);
416 
417  INVARIANT(
418  to_symbol_expr(it->assign_lhs()).get_identifier() ==
419  function_pointer_call_site.get_identifier(),
420  "called function pointer must have been assigned at the previous location");
421 
422  if(!can_cast_expr<symbol_exprt>(it->assign_rhs()))
423  return {};
424 
425  const auto &rhs = to_symbol_expr(it->assign_rhs());
426 
427  const auto restriction = by_name_restrictions.find(rhs.get_identifier());
428 
429  if(restriction != by_name_restrictions.end())
430  {
432  std::make_pair(
433  function_pointer_call_site.get_identifier(), restriction->second));
434  }
435 
436  return {};
437 }
438 
440  const optionst &options,
441  const goto_modelt &goto_model,
442  message_handlert &message_handler)
443 {
444  auto const restriction_opts =
446 
447  restrictionst commandline_restrictions;
448  try
449  {
450  commandline_restrictions =
453  goto_model, commandline_restrictions);
454  }
455  catch(const invalid_restriction_exceptiont &e)
456  {
459  }
460 
461  restrictionst file_restrictions;
462  try
463  {
464  auto const restriction_file_opts =
467  restriction_file_opts, message_handler);
468  typecheck_function_pointer_restrictions(goto_model, file_restrictions);
469  }
470  catch(const invalid_restriction_exceptiont &e)
471  {
472  throw deserialization_exceptiont{e.what()};
473  }
474 
475  restrictionst name_restrictions;
476  try
477  {
478  auto const restriction_name_opts =
480  name_restrictions = get_function_pointer_by_name_restrictions(
481  restriction_name_opts, goto_model);
482  typecheck_function_pointer_restrictions(goto_model, name_restrictions);
483  }
484  catch(const invalid_restriction_exceptiont &e)
485  {
488  }
489 
491  commandline_restrictions,
492  merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
493 }
494 
497 {
499 
500  if(!json.is_object())
501  {
502  throw deserialization_exceptiont{"top level item is not an object"};
503  }
504 
505  for(auto const &restriction : to_json_object(json))
506  {
507  restrictions.emplace(irep_idt{restriction.first}, [&] {
508  if(!restriction.second.is_array())
509  {
510  throw deserialization_exceptiont{"Value of " + restriction.first +
511  " is not an array"};
512  }
513  auto possible_targets = std::unordered_set<irep_idt>{};
514  auto const &array = to_json_array(restriction.second);
516  array.begin(),
517  array.end(),
518  std::inserter(possible_targets, possible_targets.end()),
519  [&](const jsont &array_element) {
520  if(!array_element.is_string())
521  {
522  throw deserialization_exceptiont{
523  "Value of " + restriction.first +
524  "contains a non-string array element"};
525  }
526  return irep_idt{to_json_string(array_element).value};
527  });
528  return possible_targets;
529  }());
530  }
531 
533 }
534 
536  const std::string &filename,
537  message_handlert &message_handler)
538 {
539  auto inFile = std::ifstream{filename};
540  jsont json;
541 
542  if(parse_json(inFile, filename, message_handler, json))
543  {
545  "failed to read function pointer restrictions from " + filename};
546  }
547 
548  return from_json(json);
549 }
550 
552 {
553  auto function_pointer_restrictions_json = jsont{};
554  auto &restrictions_json_object =
555  function_pointer_restrictions_json.make_object();
556 
557  for(auto const &restriction : restrictions)
558  {
559  auto &targets_array =
560  restrictions_json_object[id2string(restriction.first)].make_array();
561  for(auto const &target : restriction.second)
562  {
563  targets_array.push_back(json_stringt{target});
564  }
565  }
566 
567  return function_pointer_restrictions_json;
568 }
569 
571  const std::string &filename) const
572 {
573  auto function_pointer_restrictions_json = to_json();
574 
575  auto outFile = std::ofstream{filename};
576 
577  if(!outFile)
578  {
579  throw system_exceptiont{"cannot open " + filename +
580  " for writing function pointer restrictions"};
581  }
582 
583  function_pointer_restrictions_json.output(outFile);
584  // Ensure output file ends with a newline character.
585  outFile << '\n';
586 }
587 
590  const std::list<std::string> &restriction_name_opts,
591  const goto_modelt &goto_model)
592 {
593  function_pointer_restrictionst::restrictionst by_name_restrictions =
595  restriction_name_opts, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
596 
598  for(auto const &goto_function : goto_model.goto_functions.function_map)
599  {
600  for_each_function_call(
601  goto_function.second, [&](const goto_programt::const_targett it) {
602  const auto restriction = get_by_name_restriction(
603  goto_function.second, by_name_restrictions, it);
604 
605  if(restriction)
606  {
607  restrictions.insert(*restriction);
608  }
609  });
610  }
611 
612  return restrictions;
613 }
function_pointer_restrictionst::invalid_restriction_exceptiont::reason
std::string reason
Definition: restrict_function_pointers.h:101
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:26
can_cast_expr< symbol_exprt >
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:173
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
function_pointer_restrictionst::read_from_file
static function_pointer_restrictionst read_from_file(const std::string &filename, message_handlert &message_handler)
Definition: restrict_function_pointers.cpp:535
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:140
RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
Definition: restrict_function_pointers.h:39
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
optionst
Definition: options.h:23
string_utils.h
transform
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:159
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
for_each_instruction_if
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
Definition: goto_program.h:1232
restrict_function_pointers
void restrict_function_pointers(goto_modelt &goto_model, const function_pointer_restrictionst &restrictions)
Apply function pointer restrictions to a goto_model.
Definition: restrict_function_pointers.cpp:219
function_pointer_restrictionst::to_json
jsont to_json() const
Definition: restrict_function_pointers.cpp:551
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
options.h
Options.
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
jsont::make_object
json_objectt & make_object()
Definition: json.h:438
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
jsont
Definition: json.h:27
function_pointer_restrictionst::invalid_restriction_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: restrict_function_pointers.cpp:154
function_pointer_restrictionst::from_options
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.
Definition: restrict_function_pointers.cpp:439
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1056
notequal_exprt
Disequality.
Definition: std_expr.h:1283
function_pointer_restrictionst::restrictions
const restrictionst restrictions
Definition: restrict_function_pointers.h:74
json_parser.h
function_pointer_restrictionst::get_function_pointer_by_name_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.
Definition: restrict_function_pointers.cpp:589
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
type2c
std::string type2c(const typet &type, const namespacet &ns)
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:39
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:706
parse_function_pointer_restriction_options_from_cmdline
void parse_function_pointer_restriction_options_from_cmdline(const cmdlinet &cmdline, optionst &options)
Definition: restrict_function_pointers.cpp:233
cmdlinet
Definition: cmdline.h:21
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
function_pointer_restrictionst::parse_function_pointer_restrictions_from_file
static restrictionst parse_function_pointer_restrictions_from_file(const std::list< std::string > &filenames, message_handlert &message_handler)
Definition: restrict_function_pointers.cpp:318
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
restrict_function_pointers.h
Given goto functions and a list of function parameters or globals that are function pointers with lis...
function_pointer_restrictionst::merge_function_pointer_restrictions
static restrictionst merge_function_pointer_restrictions(restrictionst lhs, const restrictionst &rhs)
Definition: restrict_function_pointers.cpp:260
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
expr2c.h
join_strings
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:62
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:641
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
can_cast_expr< dereference_exprt >
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:668
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:61
function_pointer_restrictionst::restrictionst
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > restrictionst
Definition: restrict_function_pointers.h:71
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
function_pointer_restrictionst::get_by_name_restriction
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)
Definition: restrict_function_pointers.cpp:396
message_handlert
Definition: message.h:28
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
function_pointer_restrictionst::restrictiont
restrictionst::value_type restrictiont
Definition: restrict_function_pointers.h:72
function_pointer_restrictionst
Definition: restrict_function_pointers.h:68
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
function_pointer_restrictionst::parse_function_pointer_restrictions_from_command_line
static restrictionst parse_function_pointer_restrictions_from_command_line(const std::list< std::string > &restriction_opts)
Definition: restrict_function_pointers.cpp:310
source_locationt
Definition: source_location.h:19
function_pointer_restrictionst::invalid_restriction_exceptiont::invalid_restriction_exceptiont
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
Definition: restrict_function_pointers.cpp:148
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
function_pointer_restrictionst::invalid_restriction_exceptiont::correct_format
std::string correct_format
Definition: restrict_function_pointers.h:102
RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_OPT
Definition: restrict_function_pointers.h:36
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
cmdline.h
function_pointer_restrictionst::typecheck_function_pointer_restrictions
static void typecheck_function_pointer_restrictions(const goto_modelt &goto_model, const restrictionst &restrictions)
Definition: restrict_function_pointers.cpp:169
function_pointer_restrictionst::write_to_file
void write_to_file(const std::string &filename) const
Definition: restrict_function_pointers.cpp:570
function_pointer_restrictionst::parse_function_pointer_restrictions
static restrictionst parse_function_pointer_restrictions(const std::list< std::string > &restriction_opts, const std::string &option)
Definition: restrict_function_pointers.cpp:282
RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
Definition: restrict_function_pointers.h:37
function_pointer_restrictionst::parse_function_pointer_restriction
static restrictiont parse_function_pointer_restriction(const std::string &restriction_opt, const std::string &option)
Definition: restrict_function_pointers.cpp:336
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:722
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
function_pointer_restrictionst::from_json
static function_pointer_restrictionst from_json(const jsont &json)
Definition: restrict_function_pointers.cpp:496
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
function_pointer_restrictionst::invalid_restriction_exceptiont
Definition: restrict_function_pointers.h:93
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
parse_json
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
optionst::get_list_option
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
code_function_callt::function
exprt & function()
Definition: std_code.h:1248
json_stringt
Definition: json.h:270
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:135