klee since llvm version 2.8 does not generate enough test case for islower example

[llvmbot]

Bugzilla Link	10436
Resolution	FIXED
Resolved on	Apr 08, 2012 07:02
Version	unspecified
OS	All
Reporter	LLVM Bugzilla Contributor
CC	@ccadar

Extended Description

Building klee with newer versions of llvm (since 2.8) produces wrong results.
Not enough paths are evaluated.

What are the reesons,
looking at islower.c it should be indeed 3 generated test cases.
Or is llvm making some special optimizations which i don't see?

Generated output wither newer version:
Started: 2011-07-22 09:32:54
BEGIN searcher description
DFSSearcher
END searcher description
Finished: 2011-07-22 09:32:54
Elapsed: 00:00:00
KLEE: done: explored paths = 2
KLEE: done: avg. constructs per query = 7
KLEE: done: total queries = 3
KLEE: done: valid queries = 0
KLEE: done: invalid queries = 3
KLEE: done: query cex = 3

KLEE: done: total instructions = 26
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

Code with older
Started: 2011-07-22 01:10:22
BEGIN searcher description
DFSSearcher
END searcher description
Finished: 2011-07-22 01:10:22
Elapsed: 00:00:00
KLEE: done: explored paths = 3
KLEE: done: avg. constructs per query = 6
KLEE: done: total queries = 3
KLEE: done: valid queries = 0
KLEE: done: invalid queries = 3
KLEE: done: query cex = 3

KLEE: done: total instructions = 52
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

[llvmbot]

It is not a bug.
The llvm optimization pass simplify cfg simplifies the example (just 4 instead of 5 BB in my_islower) and therefore needs less test cases.

Maybe in that case, the web site should be updated.

This optimization can't be disabled with -disable-opt.

[ccadar]

Closing old bug reports. The example in Tutorial 1 was changed, to make it
more reproducible across LLVM versions.