More GraphML witness format issues
The witness format based on GraphML has several issues coming mainly from the fact that its semantics is defined over CFA, but the relation of a program and CFA is unclear (see !65 (merged)). Some issues can be fixed by !64 (merged). But there are still some issues where the solution is not clear.
- The ambiguity of witnesses can be dramatically reduced if each witness edge is bounded to some line of the source code (e.g. using
startline
andendline
). Which line should be associated withreturnFromFunction
? The line withreturn
or the line to which to which the control returns (i.e., the line with function call)? - Assume that there is a witness edge specifying only
startline
to ben
and assumptionx == 3
. Should this state-space guard be applied at the beginning of the line or after the first execution step correspnding to the line? I prefer the first possibility, but it seems that the paper Verification Witnesses applies it only after the first CFA edge corresponding to linen
is performed (f I understand it correctly).