restrict_function_pointers.cpp File Reference

#include "restrict_function_pointers.h"
#include <ansi-c/expr2c.h>
#include <json/json_parser.h>
#include <util/cmdline.h>
#include <util/options.h>
#include <util/pointer_expr.h>
#include <util/string_utils.h>
#include "goto_model.h"
#include "remove_function_pointers.h"
#include <algorithm>
#include <fstream>

Include dependency graph for restrict_function_pointers.cpp:

Go to the source code of this file.

Functions
void	restrict_function_pointers (message_handlert &message_handler, goto_modelt &goto_model, const optionst &options)
	Apply function pointer restrictions to a goto_model. More...
void	parse_function_pointer_restriction_options_from_cmdline (const cmdlinet &cmdline, optionst &options)
static std::string	resolve_pointer_name (const std::string &candidate, const goto_modelt &goto_model)
	Parse candidate to distinguish whether it refers to a function pointer symbol directly (as produced by label_function_pointer_call_sites), or a source location via its statement label. More...

Function Documentation

parse_function_pointer_restriction_options_from_cmdline()

void parse_function_pointer_restriction_options_from_cmdline	(	const cmdlinet &	cmdline,
		optionst &	options
	)

Definition at line 201 of file restrict_function_pointers.cpp.

resolve_pointer_name()

static std::string resolve_pointer_name ( const std::string &  candidate, const goto_modelt &  goto_model  )

static

Parse candidate to distinguish whether it refers to a function pointer symbol directly (as produced by label_function_pointer_call_sites), or a source location via its statement label.

In the latter case, resolve the name to the underlying function pointer symbol.

Definition at line 311 of file restrict_function_pointers.cpp.

restrict_function_pointers()

void restrict_function_pointers	(	message_handlert &	message_handler,
		goto_modelt &	goto_model,
		const optionst &	options
	)

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 171 of file restrict_function_pointers.cpp.