Skip to content

Track variables which are in scope

Marian Lingsch requested to merge track-variables-in-scope into trunk

Currently when exporting witnesses it happens that the invariants contain variables which are not in scope. To mitigate this, we add information to the CFANode's about which variables are currently in scope.

Since witnesses in version 2.0 are currently only defined for C programs we also only track the variables which are in scope for those programs. The optional typing should make it clear that this information will not always be available.

This branch currently only tackles the problem for the C parser of Eclipse. Other use cases are currently not considered. In particular post-processing of the CFA is ignored, since we are are only interested in the variables which are in scope in the original C program i.e. which can be exported in the invariants. If variables are added or deleted in post-processing this should have no effect on which variables can be exported.

Merge request reports