Flow Insensitive Static Analysis. More...
#include <queue>#include <map>#include <iosfwd>#include <unordered_set>#include <goto-programs/goto_functions.h>
Include dependency graph for flow_insensitive_analysis.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | flow_insensitive_abstract_domain_baset |
| class | flow_insensitive_analysis_baset |
| class | flow_insensitive_analysist< T > |
Detailed Description
Flow Insensitive Static Analysis.
A framework for flow-insensitive analyses. Maintains a single global abstract value (an instance of flow_insensitive_abstract_domain_baset, "the domain,") which instructions are invited to transform in turn.
Note this is unsound if used naively, because it follows the control-flow graph and terminates when an instruction makes no change to the domain and that instruction's successors have already been visited. Therefore a domain that relies upon every reachable instruction being re-visited upon the domain being updated must ensure that itself, for example by maintaining a map from locations to the latest version of the domain witnessed.
Definition in file flow_insensitive_analysis.h.
