cprover
Loading...
Searching...
No Matches
value_set_analysis_fi.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Propagation (flow insensitive)
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
13#define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
14
16
17#include "value_set_domain_fi.h"
18#include "value_sets.h"
19
21 public value_setst,
22 public flow_insensitive_analysist<value_set_domain_fit>
23{
24public:
26
27 // constructor
29 const namespacet &_ns,
30 track_optionst _track_options=TRACK_ALL_POINTERS):
32 track_options(_track_options)
33 {
34 }
35
37
38 void initialize(const goto_programt &goto_program) override;
39 void initialize(const goto_functionst &goto_functions) override;
40
41protected:
43
44 bool check_type(const typet &type);
45 void get_globals(std::list<value_set_fit::entryt> &dest);
46 void add_vars(const goto_functionst &goto_functions);
47 void add_vars(const goto_programt &goto_programa);
48
49 void get_entries(
50 const symbolt &symbol,
51 std::list<value_set_fit::entryt> &dest);
52
53 void get_entries_rec(
54 const irep_idt &identifier,
55 const std::string &suffix,
56 const typet &type,
57 std::list<value_set_fit::entryt> &dest);
58
59public:
60 // interface value_sets
61 std::vector<exprt> get_values(
62 const irep_idt &function_id,
63 locationt l,
64 const exprt &expr) override;
65};
66
67#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_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
goto_programt::const_targett locationt
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
bool check_type(const typet &type)
value_set_analysis_fit(const namespacet &_ns, track_optionst _track_options=TRACK_ALL_POINTERS)
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
void add_vars(const goto_functionst &goto_functions)
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
void get_globals(std::list< value_set_fit::entryt > &dest)
void initialize(const goto_programt &goto_program) override
flow_insensitive_analysist< value_set_domain_fit > baset
Flow Insensitive Static Analysis.
Value Set (Flow Insensitive)
Value Set Propagation.