CBMC
three_way_merge_abstract_interpreter.h File Reference

An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call. More...

#include <analyses/ai.h>
+ Include dependency graph for three_way_merge_abstract_interpreter.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  ai_three_way_merget
 

Detailed Description

An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivity domain's three-way-merge operation on returning from a function call.

This gives some of the precision of context-sensitive analysis but at a fraction of the cost. The really key thing is that it distinguishes between variables that are modified in the function (or things called from it) and those that appear modified because they have different values at different call sites. This is especially important for preserving the value of (unmodified) global variables.

Definition in file three_way_merge_abstract_interpreter.h.