Incorrect behavior for global variables

[namasikanam]

As global variables can cause the inpurity of the functions, that is functions will possibly have side effect, current piVC cannot handle them correctly. For example, the partial correctness of the following code will be verified.

int x;

@pre true
@post rv > 0
int fun() {
	x := 1;
	return x;
}

@pre true
@post rv < 0
int fun1() {
	x := -1;
	fun();
	return x;
}

I have no idea how to fix this bug, It seems a inherent flaw of the algorithm.

[jankofron]

As far as I know, global variables should be used just for annotations (pre- and post-conditions), not as a real code variables. The system just ignores them, and you should not use them in the code. As you wrote, this is an inherent property of the approach, not a bug.