cprover
Loading...
Searching...
No Matches
value_set_analysis_fivrns.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Analysis (Flow Insensitive, Validity Regions)
4
5Author: Daniel Kroening, kroening@kroening.com,
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
15
17
19#include "value_sets.h"
20
22 public value_setst,
23 public flow_insensitive_analysist<value_set_domain_fivrnst>
24{
25public:
27
28 // constructor
30 const namespacet &_ns,
31 track_optionst _track_options=TRACK_ALL_POINTERS):
33 track_options(_track_options)
34 {
35 }
36
38
39 virtual void initialize(const goto_programt &goto_program);
40 virtual void initialize(const goto_functionst &goto_functions);
41
42 using baset::output;
43
44 void output(const irep_idt &function_id, locationt l, std::ostream &out)
45 {
46 state.value_set.set_from(function_id, l->location_number);
47 state.value_set.set_to(function_id, l->location_number);
48 state.output(ns, out);
49 }
50
51 void output(
52 const irep_idt &function_id,
53 const goto_programt &goto_program,
54 std::ostream &out)
55 {
56 forall_goto_program_instructions(it, goto_program)
57 {
58 out << "**** " << it->source_location << '\n';
59 output(function_id, it, out);
60 out << '\n';
61 goto_program.output_instruction(ns, function_id, out, *it);
62 out << '\n';
63 }
64 }
65
66protected:
68
69 bool check_type(const typet &type);
70 void get_globals(std::list<value_set_fivrnst::entryt> &dest);
71 void add_vars(const goto_functionst &goto_functions);
72 void add_vars(const goto_programt &goto_programa);
73
75 const symbolt &symbol,
76 std::list<value_set_fivrnst::entryt> &dest);
77
79 const irep_idt &identifier,
80 const std::string &suffix,
81 const typet &type,
82 std::list<value_set_fivrnst::entryt> &dest);
83
84public:
85 // interface value_sets
86 virtual void get_values(
87 const irep_idt &function_id,
88 locationt l,
89 const exprt &expr,
90 std::list<exprt> &dest)
91 {
96 state.value_set.from_target_index = l->location_number;
97 state.value_set.to_target_index = l->location_number;
98 state.value_set.get_value_set(expr, dest, ns);
99 }
100};
101
102#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FIVRNS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
number_type number(const key_type &a)
Definition: numbering.h:37
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
void get_globals(std::list< value_set_fivrnst::entryt > &dest)
virtual void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest)
flow_insensitive_analysist< value_set_domain_fivrnst > baset
void output(const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out)
void get_entries(const symbolt &symbol, std::list< value_set_fivrnst::entryt > &dest)
void add_vars(const goto_functionst &goto_functions)
void output(const irep_idt &function_id, locationt l, std::ostream &out)
value_set_analysis_fivrnst(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
void add_vars(const goto_programt &goto_programa)
virtual void initialize(const goto_functionst &goto_functions)
virtual void initialize(const goto_programt &goto_program)
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrnst::entryt > &dest)
bool check_type(const typet &type)
virtual void output(const namespacet &ns, std::ostream &out) const
static numberingt< irep_idt > function_numbering
void set_to(const irep_idt &function, unsigned inx)
void set_from(const irep_idt &function, unsigned inx)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
unsigned from_target_index
Flow Insensitive Static Analysis.
#define forall_goto_program_instructions(it, program)
Value Set Domain (Flow Insensitive, Validity Regions)
Value Set Propagation.