Incorrect handling of switch-local variables

[lu-w]

Hey all,

CBMC does not seem to handle values of "switch-local" variables correctly, i.e. variables that were defined in the local scope of a switch-statement. In this example, x is such a variable:

extern void __VERIFIER_error();
void main() {
	switch (0) {
		int x;
		default:
			x = 0;
			if (x) __VERIFIER_error();
	}
}

CBMC returns VERIFICATION FAILED when run on this program. Indeed, x is of an indeterminate value at its declaration, but set to 0 directly afterwards in the default case. Hence, the error location should not be reachable and the program determined safe.

Upon inspection it seems like CBMC does not propagate the constraint of x=0 correctly and still assumes a non-deterministic value after its assignment - CBMC was able to produce a counterexample for x=262144.

CBMC version: 5.10
Operating system: Linux
Exact command line resulting in the issue: cbmc bug.c
What behaviour did you expect: CBMC returns VERIFICATION SUCCESSFUL
What happened instead: CBMC returns VERIFICATION FAILED

[martin-cs]

Thanks for reporting this. It does look like a front-end bug. My guess is that the DECL instruction is in the wrong place, so symex gets confused. Maybe one of the C front-end maintainers can have a look at this.

[lu-w]

Hey Martin, thanks for the reply! Is there any news on the issue?
This may seem like a rather constructed problem, but was actually discovered on code that was outputted by the static analysis tool Frama-C. Thus, we are currently not able to run CBMC on Frama-C exports that contain such switch-local variables.

[blizzard4591]

@martin-cs We are currently working on a comparison study which includes CBMC and this bug is blocking us from benchmarking CBMC on the same code as the other tools. Can you give an estimate on when this might be fixed?

[tautschnig]

@blizzard4591 I'll take a look.

[tautschnig]

Since eaa7d93 CBMC actually yields the correct result for the example, but I'll add a PR adding at least a regression test, and possibly also adjusting where we place the declaration that's generated for int x;.