cprover
|
#include "restrict_function_pointers.h"
#include <ansi-c/expr2c.h>
#include <json/json_parser.h>
#include <util/expr_iterator.h>
#include <util/string_utils.h>
#include <algorithm>
#include <fstream>
#include <functional>
#include <iostream>
Go to the source code of this file.
Functions | |
void | restrict_function_pointers (goto_modelt &goto_model, const function_pointer_restrictionst &restrictions) |
Apply function pointer restrictions to a goto_model. More... | |
void | parse_function_pointer_restriction_options_from_cmdline (const cmdlinet &cmdline, optionst &options) |
void parse_function_pointer_restriction_options_from_cmdline | ( | const cmdlinet & | cmdline, |
optionst & | options | ||
) |
Definition at line 229 of file restrict_function_pointers.cpp.
void restrict_function_pointers | ( | goto_modelt & | goto_model, |
const function_pointer_restrictionst & | restrictions | ||
) |
Apply function pointer restrictions to a goto_model.
Each restriction is a mapping from a pointer name to a set of possible targets. Replace calls of these "restricted" pointers with a branch on the value of the function pointer, comparing it to the set of possible targets. This also adds an assertion that the pointer actually has one of the listed values.
Note: This requires label_function_pointer_call_sites to be run before
Definition at line 215 of file restrict_function_pointers.cpp.