cprover
restrict_function_pointers.cpp File Reference
#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>
+ Include dependency graph for restrict_function_pointers.cpp:

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)
 

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

◆ restrict_function_pointers()

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.