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