CBMC
three_way_merge_abstract_interpreter.cpp 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 dependency graph for three_way_merge_abstract_interpreter.cpp:

Go to the source code of this file.

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.cpp.