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/expr_iterator.h>
16 #include <util/pointer_expr.h>
17 #include <util/string_utils.h>
18 
19 #include <algorithm>
20 #include <fstream>
21 #include <functional>
22 #include <iostream>
23 
24 namespace
25 {
26 source_locationt make_function_pointer_restriction_assertion_source_location(
27  source_locationt source_location,
29 {
30  std::stringstream comment;
31 
32  comment << "dereferenced function pointer at " << restriction.first
33  << " must be ";
34 
35  if(restriction.second.size() == 1)
36  {
37  comment << *restriction.second.begin();
38  }
39  else
40  {
41  comment << "one of [";
42 
44  comment, restriction.second.begin(), restriction.second.end(), ", ");
45 
46  comment << ']';
47  }
48 
49  source_location.set_comment(comment.str());
50  source_location.set_property_class(ID_assertion);
51 
52  return source_location;
53 }
54 
55 template <typename Handler, typename GotoFunctionT>
56 void for_each_function_call(GotoFunctionT &&goto_function, Handler handler)
57 {
58  using targett = decltype(goto_function.body.instructions.begin());
60  goto_function,
61  [](targett target) { return target->is_function_call(); },
62  handler);
63 }
64 
65 void restrict_function_pointer(
66  goto_functiont &goto_function,
67  goto_modelt &goto_model,
68  const function_pointer_restrictionst &restrictions,
69  const goto_programt::targett &location)
70 {
71  PRECONDITION(location->is_function_call());
72 
73  // for each function call, we check if it is using a symbol we have
74  // restrictions for, and if so branch on its value and insert concrete calls
75  // to the restriction functions
76 
77  // Check if this is calling a function pointer, and if so if it is one
78  // we have a restriction for
79  const auto &original_function_call = location->get_function_call();
80 
81  if(!can_cast_expr<dereference_exprt>(original_function_call.function()))
82  return;
83 
84  // because we run the label function pointer calls transformation pass before
85  // this stage a dereference can only dereference a symbol expression
86  auto const &called_function_pointer =
87  to_dereference_expr(original_function_call.function()).pointer();
88  PRECONDITION(can_cast_expr<symbol_exprt>(called_function_pointer));
89  auto const &pointer_symbol = to_symbol_expr(called_function_pointer);
90  auto const restriction_iterator =
91  restrictions.restrictions.find(pointer_symbol.get_identifier());
92 
93  if(restriction_iterator == restrictions.restrictions.end())
94  return;
95 
96  auto const &restriction = *restriction_iterator;
97 
98  // this is intentionally a copy because we're about to change the
99  // instruction this iterator points to
100  // if we can, we will replace uses of it by a case distinction over
101  // given functions the function pointer can point to
102  auto const original_function_call_instruction = *location;
103 
104  *location = goto_programt::make_assertion(
105  false_exprt{},
106  make_function_pointer_restriction_assertion_source_location(
107  original_function_call_instruction.source_location, restriction));
108 
109  auto const assume_false_location = goto_function.body.insert_after(
110  location,
112  false_exprt{}, original_function_call_instruction.source_location));
113 
114  // this is mutable because we'll update this at the end of each
115  // loop iteration to always point at the start of the branch
116  // we created
117  auto else_location = location;
118 
119  auto const end_if_location = goto_function.body.insert_after(
120  assume_false_location, goto_programt::make_skip());
121 
122  for(auto const &restriction_target : restriction.second)
123  {
124  auto new_instruction = original_function_call_instruction;
125  // can't use get_function_call because that'll return a const ref
126  const symbol_exprt &function_pointer_target_symbol_expr =
127  goto_model.symbol_table.lookup_ref(restriction_target).symbol_expr();
128  to_code_function_call(new_instruction.code_nonconst()).function() =
129  function_pointer_target_symbol_expr;
130  auto const goto_end_if_location = goto_function.body.insert_before(
131  else_location,
133  end_if_location, original_function_call_instruction.source_location));
134  auto const replaced_instruction_location =
135  goto_function.body.insert_before(goto_end_if_location, new_instruction);
136  else_location = goto_function.body.insert_before(
137  replaced_instruction_location,
139  else_location,
140  notequal_exprt{pointer_symbol,
141  address_of_exprt{function_pointer_target_symbol_expr}}));
142  }
143 }
144 } // namespace
145 
147  invalid_restriction_exceptiont(std::string reason, std::string correct_format)
148  : reason(std::move(reason)), correct_format(std::move(correct_format))
149 {
150 }
151 
152 std::string
154 {
155  std::string res;
156 
157  res += "Invalid restriction";
158  res += "\nReason: " + reason;
159 
160  if(!correct_format.empty())
161  {
162  res += "\nFormat: " + correct_format;
163  }
164 
165  return res;
166 }
167 
169  const goto_modelt &goto_model,
171 {
172  for(auto const &restriction : restrictions)
173  {
174  auto const function_pointer_sym =
175  goto_model.symbol_table.lookup(restriction.first);
176  if(function_pointer_sym == nullptr)
177  {
178  throw invalid_restriction_exceptiont{id2string(restriction.first) +
179  " not found in the symbol table"};
180  }
181  auto const &function_pointer_type = function_pointer_sym->type;
182  if(function_pointer_type.id() != ID_pointer)
183  {
184  throw invalid_restriction_exceptiont{"not a function pointer: " +
185  id2string(restriction.first)};
186  }
187  auto const &function_type =
188  to_pointer_type(function_pointer_type).subtype();
189  if(function_type.id() != ID_code)
190  {
191  throw invalid_restriction_exceptiont{"not a function pointer: " +
192  id2string(restriction.first)};
193  }
194  auto const &ns = namespacet{goto_model.symbol_table};
195  for(auto const &function_pointer_target : restriction.second)
196  {
197  auto const function_pointer_target_sym =
198  goto_model.symbol_table.lookup(function_pointer_target);
199  if(function_pointer_target_sym == nullptr)
200  {
202  "symbol not found: " + id2string(function_pointer_target)};
203  }
204  auto const &function_pointer_target_type =
205  function_pointer_target_sym->type;
206  if(function_type != function_pointer_target_type)
207  {
209  "type mismatch: `" + id2string(restriction.first) + "' points to `" +
210  type2c(function_type, ns) + "', but restriction `" +
211  id2string(function_pointer_target) + "' has type `" +
212  type2c(function_pointer_target_type, ns) + "'"};
213  }
214  }
215  }
216 }
217 
219  goto_modelt &goto_model,
221 {
222  for(auto &function_item : goto_model.goto_functions.function_map)
223  {
224  goto_functiont &goto_function = function_item.second;
225 
226  for_each_function_call(goto_function, [&](const goto_programt::targett it) {
227  restrict_function_pointer(goto_function, goto_model, restrictions, it);
228  });
229  }
230 }
231 
233  const cmdlinet &cmdline,
234  optionst &options)
235 {
237  {
238  options.set_option(
241  }
242 
244  {
245  options.set_option(
248  }
249 
251  {
252  options.set_option(
255  }
256 }
257 
262 {
263  auto &result = lhs;
264 
265  for(auto const &restriction : rhs)
266  {
267  auto emplace_result = result.emplace(restriction.first, restriction.second);
268  if(!emplace_result.second)
269  {
270  for(auto const &target : restriction.second)
271  {
272  emplace_result.first->second.insert(target);
273  }
274  }
275  }
276 
277  return result;
278 }
279 
282  const std::list<std::string> &restriction_opts,
283  const std::string &option)
284 {
285  auto function_pointer_restrictions =
287 
288  for(const std::string &restriction_opt : restriction_opts)
289  {
290  const auto restriction =
291  parse_function_pointer_restriction(restriction_opt, option);
292 
293  const bool inserted = function_pointer_restrictions
294  .emplace(restriction.first, restriction.second)
295  .second;
296 
297  if(!inserted)
298  {
300  "function pointer restriction for `" + id2string(restriction.first) +
301  "' was specified twice"};
302  }
303  }
304 
305  return function_pointer_restrictions;
306 }
307 
310  const std::list<std::string> &restriction_opts)
311 {
313  restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT);
314 }
315 
318  const std::list<std::string> &filenames,
319  message_handlert &message_handler)
320 {
321  auto merged_restrictions = function_pointer_restrictionst::restrictionst{};
322 
323  for(auto const &filename : filenames)
324  {
325  auto const restrictions = read_from_file(filename, message_handler);
326 
327  merged_restrictions = merge_function_pointer_restrictions(
328  std::move(merged_restrictions), restrictions.restrictions);
329  }
330 
331  return merged_restrictions;
332 }
333 
336  const std::string &restriction_opt,
337  const std::string &option)
338 {
339  // the format for restrictions is <pointer_name>/<target[,more_targets]*>
340  // exactly one pointer and at least one target
341  auto const pointer_name_end = restriction_opt.find('/');
342  auto const restriction_format_message =
343  "the format for restrictions is "
344  "<pointer_name>/<target[,more_targets]*>";
345 
346  if(pointer_name_end == std::string::npos)
347  {
348  throw invalid_restriction_exceptiont{"couldn't find '/' in `" +
349  restriction_opt + "'",
350  restriction_format_message};
351  }
352 
353  if(pointer_name_end == restriction_opt.size())
354  {
356  "couldn't find names of targets after '/' in `" + restriction_opt + "'",
357  restriction_format_message};
358  }
359 
360  if(pointer_name_end == 0)
361  {
363  "couldn't find target name before '/' in `" + restriction_opt + "'"};
364  }
365 
366  auto const pointer_name = restriction_opt.substr(0, pointer_name_end);
367  auto const target_names_substring =
368  restriction_opt.substr(pointer_name_end + 1);
369  auto const target_name_strings = split_string(target_names_substring, ',');
370 
371  if(target_name_strings.size() == 1 && target_name_strings[0].empty())
372  {
374  "missing target list for function pointer restriction " + pointer_name,
375  restriction_format_message};
376  }
377 
378  std::unordered_set<irep_idt> target_names;
379  target_names.insert(target_name_strings.begin(), target_name_strings.end());
380 
381  for(auto const &target_name : target_names)
382  {
383  if(target_name == ID_empty_string)
384  {
386  "leading or trailing comma in restrictions for `" + pointer_name + "'",
387  restriction_format_message);
388  }
389  }
390 
391  return std::make_pair(pointer_name, target_names);
392 }
393 
396  const goto_functiont &goto_function,
397  const function_pointer_restrictionst::restrictionst &by_name_restrictions,
398  const goto_programt::const_targett &location)
399 {
400  PRECONDITION(location->is_function_call());
401 
402  const exprt &function = location->get_function_call().function();
403 
404  if(!can_cast_expr<dereference_exprt>(function))
405  return {};
406 
407  // the function pointer is guaranteed to be a symbol expression, as the
408  // label_function_pointer_call_sites() pass (which must be run before the
409  // function pointer restriction) replaces calls via complex pointer
410  // expressions by calls to a function pointer variable
411  auto const &function_pointer_call_site =
412  to_symbol_expr(to_dereference_expr(function).pointer());
413 
414  const goto_programt::const_targett it = std::prev(location);
415 
416  const code_assignt &assign = it->get_assign();
417 
418  INVARIANT(
419  to_symbol_expr(assign.lhs()).get_identifier() ==
420  function_pointer_call_site.get_identifier(),
421  "called function pointer must have been assigned at the previous location");
422 
423  if(!can_cast_expr<symbol_exprt>(assign.rhs()))
424  return {};
425 
426  const auto &rhs = to_symbol_expr(assign.rhs());
427 
428  const auto restriction = by_name_restrictions.find(rhs.get_identifier());
429 
430  if(restriction != by_name_restrictions.end())
431  {
433  std::make_pair(
434  function_pointer_call_site.get_identifier(), restriction->second));
435  }
436 
437  return {};
438 }
439 
441  const optionst &options,
442  const goto_modelt &goto_model,
443  message_handlert &message_handler)
444 {
445  auto const restriction_opts =
447 
448  restrictionst commandline_restrictions;
449  try
450  {
451  commandline_restrictions =
454  goto_model, commandline_restrictions);
455  }
456  catch(const invalid_restriction_exceptiont &e)
457  {
460  }
461 
462  restrictionst file_restrictions;
463  try
464  {
465  auto const restriction_file_opts =
468  restriction_file_opts, message_handler);
469  typecheck_function_pointer_restrictions(goto_model, file_restrictions);
470  }
471  catch(const invalid_restriction_exceptiont &e)
472  {
473  throw deserialization_exceptiont{e.what()};
474  }
475 
476  restrictionst name_restrictions;
477  try
478  {
479  auto const restriction_name_opts =
481  name_restrictions = get_function_pointer_by_name_restrictions(
482  restriction_name_opts, goto_model);
483  typecheck_function_pointer_restrictions(goto_model, name_restrictions);
484  }
485  catch(const invalid_restriction_exceptiont &e)
486  {
489  }
490 
492  commandline_restrictions,
493  merge_function_pointer_restrictions(file_restrictions, name_restrictions))};
494 }
495 
498 {
500 
501  if(!json.is_object())
502  {
503  throw deserialization_exceptiont{"top level item is not an object"};
504  }
505 
506  for(auto const &restriction : to_json_object(json))
507  {
508  restrictions.emplace(irep_idt{restriction.first}, [&] {
509  if(!restriction.second.is_array())
510  {
511  throw deserialization_exceptiont{"Value of " + restriction.first +
512  " is not an array"};
513  }
514  auto possible_targets = std::unordered_set<irep_idt>{};
515  auto const &array = to_json_array(restriction.second);
517  array.begin(),
518  array.end(),
519  std::inserter(possible_targets, possible_targets.end()),
520  [&](const jsont &array_element) {
521  if(!array_element.is_string())
522  {
523  throw deserialization_exceptiont{
524  "Value of " + restriction.first +
525  "contains a non-string array element"};
526  }
527  return irep_idt{to_json_string(array_element).value};
528  });
529  return possible_targets;
530  }());
531  }
532 
534 }
535 
537  const std::string &filename,
538  message_handlert &message_handler)
539 {
540  auto inFile = std::ifstream{filename};
541  jsont json;
542 
543  if(parse_json(inFile, filename, message_handler, json))
544  {
546  "failed to read function pointer restrictions from " + filename};
547  }
548 
549  return from_json(json);
550 }
551 
553 {
554  auto function_pointer_restrictions_json = jsont{};
555  auto &restrictions_json_object =
556  function_pointer_restrictions_json.make_object();
557 
558  for(auto const &restriction : restrictions)
559  {
560  auto &targets_array =
561  restrictions_json_object[id2string(restriction.first)].make_array();
562  for(auto const &target : restriction.second)
563  {
564  targets_array.push_back(json_stringt{target});
565  }
566  }
567 
568  return function_pointer_restrictions_json;
569 }
570 
572  const std::string &filename) const
573 {
574  auto function_pointer_restrictions_json = to_json();
575 
576  auto outFile = std::ofstream{filename};
577 
578  if(!outFile)
579  {
580  throw system_exceptiont{"cannot open " + filename +
581  " for writing function pointer restrictions"};
582  }
583 
584  function_pointer_restrictions_json.output(outFile);
585  // Ensure output file ends with a newline character.
586  outFile << '\n';
587 }
588 
591  const std::list<std::string> &restriction_name_opts,
592  const goto_modelt &goto_model)
593 {
594  function_pointer_restrictionst::restrictionst by_name_restrictions =
596  restriction_name_opts, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT);
597 
599  for(auto const &goto_function : goto_model.goto_functions.function_map)
600  {
601  for_each_function_call(
602  goto_function.second, [&](const goto_programt::const_targett it) {
603  const auto restriction = get_by_name_restriction(
604  goto_function.second, by_name_restrictions, it);
605 
606  if(restriction)
607  {
608  restrictions.insert(*restriction);
609  }
610  });
611  }
612 
613  return restrictions;
614 }
function_pointer_restrictionst::invalid_restriction_exceptiont::reason
std::string reason
Definition: restrict_function_pointers.h:97
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:29
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:536
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT
Definition: restrict_function_pointers.h:32
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:442
optionst
Definition: options.h:23
string_utils.h
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
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:157
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:1157
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:218
function_pointer_restrictionst::to_json
jsont to_json() const
Definition: restrict_function_pointers.cpp:552
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
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:27
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:153
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:440
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:982
notequal_exprt
Disequality.
Definition: std_expr.h:1197
function_pointer_restrictionst::restrictions
const restrictionst restrictions
Definition: restrict_function_pointers.h:70
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:590
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:623
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:232
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:877
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:317
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:259
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:835
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:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
can_cast_expr< dereference_exprt >
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:426
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
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:67
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:395
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:1326
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
function_pointer_restrictionst::restrictiont
restrictionst::value_type restrictiont
Definition: restrict_function_pointers.h:68
function_pointer_restrictionst
Definition: restrict_function_pointers.h:64
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:309
source_locationt
Definition: source_location.h:20
function_pointer_restrictionst::invalid_restriction_exceptiont::invalid_restriction_exceptiont
invalid_restriction_exceptiont(std::string reason, std::string correct_format="")
Definition: restrict_function_pointers.cpp:147
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
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:98
RESTRICT_FUNCTION_POINTER_OPT
#define RESTRICT_FUNCTION_POINTER_OPT
Definition: restrict_function_pointers.h:29
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
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:168
function_pointer_restrictionst::write_to_file
void write_to_file(const std::string &filename) const
Definition: restrict_function_pointers.cpp:571
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:281
RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT
Definition: restrict_function_pointers.h:30
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:335
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:639
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:497
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
function_pointer_restrictionst::invalid_restriction_exceptiont
Definition: restrict_function_pointers.h:89
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:889
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
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:238
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:563
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
json_stringt
Definition: json.h:270
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:136