Fixing global variables

[rasoolmaghareh]

@xuanlinhha please apply my comment and remove the spec-independence part. It seems to be irrelevant to this PR.

Also, one extra program fails on make check. Can you please check it:

********************
Testing: 0 .. 10.. 20.. 30.. 40.. 50..
FAIL: KLEE :: Feature/WithLibc.c (108 of 185)
******************** TEST 'KLEE :: Feature/WithLibc.c' FAILED ********************
Script:
--
/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang -I/home/sajjad/Tracer-X/klee/include /home/sajjad/Tracer-X/klee/test/Feature/WithLibc.c -emit-llvm -O0 -c -o /home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp2.bc
rm -rf /home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp.klee-out
/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee -solver-backend=z3 --output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp.klee-out --libc=klee /home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp2.bc > /home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp3.log
echo "good" > /home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp3.good
diff /home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp3.log /home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp3.good
--
Exit Code: -6

Command Output (stdout):
--
Command 0: "/home/sajjad/llvm-3.4.2/build/Release+Asserts/bin/clang" "-I/home/sajjad/Tracer-X/klee/include" "/home/sajjad/Tracer-X/klee/test/Feature/WithLibc.c" "-emit-llvm" "-O0" "-c" "-o" "/home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp2.bc"
Command 0 Result: 0
Command 0 Output:

Command 0 Stderr:
/home/sajjad/Tracer-X/klee/test/Feature/WithLibc.c:11:3: warning: implicit declaration of function 'klee_make_symbolic' is invalid in C99 [-Wimplicit-function-declaration]
  klee_make_symbolic(buf, sizeof buf);
  ^
/home/sajjad/Tracer-X/klee/test/Feature/WithLibc.c:14:7: warning: implicitly declaring library function 'strcmp' with type 'int (const char *, const char *)'
  if (strcmp(buf, s)==0) {
      ^
/home/sajjad/Tracer-X/klee/test/Feature/WithLibc.c:14:7: note: please include the header <string.h> or explicitly provide a declaration for 'strcmp'
/home/sajjad/Tracer-X/klee/test/Feature/WithLibc.c:16:7: warning: implicitly declaring library function 'printf' with type 'int (const char *, ...)'
      printf("good\n");
      ^
/home/sajjad/Tracer-X/klee/test/Feature/WithLibc.c:16:7: note: please include the header <stdio.h> or explicitly provide a declaration for 'printf'
3 warnings generated.

Command 1: "rm" "-rf" "/home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp.klee-out"
Command 1 Result: 0
Command 1 Output:

Command 1 Stderr:

Command 2: "/home/sajjad/Tracer-X/klee/Release+Asserts/bin/klee" "-solver-backend=z3" "--output-dir=/home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp.klee-out" "--libc=klee" "/home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp2.bc"
Command 2 Result: -6
Command 2 Output:
None

Command 2 Stderr:
KLEE: output directory is "/home/sajjad/Tracer-X/klee/test/Feature/Output/WithLibc.c.tmp.klee-out"
Using Z3 solver backend
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: printf
klee: Memory.cpp:511: klee::ref<klee::Expr> klee::ObjectState::read(unsigned int, klee::Expr::Width) const: Assertion `width == NumBytes * 8 && "Invalid width for read size!"' failed.
0  libLLVM-3.4.so  0x00007fb1b4839052 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  libLLVM-3.4.so  0x00007fb1b48387c4
2  libpthread.so.0 0x00007fb1b3f36390
3  libc.so.6       0x00007fb1b19f1428 gsignal + 56
4  libc.so.6       0x00007fb1b19f302a abort + 362
5  libc.so.6       0x00007fb1b19e9bd7
6  libc.so.6       0x00007fb1b19e9c82
7  klee            0x00000000004a81a6 klee::ObjectState::read(unsigned int, unsigned int) const + 486
8  klee            0x00000000004a8b1b klee::ObjectState::read(klee::ref<klee::Expr>, unsigned int) const + 251
9  klee            0x00000000004f016e klee::TxSubsumptionTableEntry::subsumed(klee::TimingSolver*, klee::ExecutionState&, double, bool, std::map<klee::ref<klee::TxAllocationContext>, klee::TxStore::MiddleStateStore, std::less<klee::ref<klee::TxAllocationContext> >, std::allocator<std::pair<klee::ref<klee::TxAllocationContext> const, klee::TxStore::MiddleStateStore> > >&, std::map<klee::ref<klee::TxVariable>, klee::ref<klee::TxStoreEntry>, std::less<klee::ref<klee::TxVariable> >, std::allocator<std::pair<klee::ref<klee::TxVariable> const, klee::ref<klee::TxStoreEntry> > > >&, std::map<klee::ref<klee::TxVariable>, klee::ref<klee::TxStoreEntry>, std::less<klee::ref<klee::TxVariable> >, std::allocator<std::pair<klee::ref<klee::TxVariable> const, klee::ref<klee::TxStoreEntry> > > >&, int) + 622
10 klee            0x00000000004f45cb klee::TxSubsumptionTable::check(klee::TimingSolver*, klee::ExecutionState&, double, int) + 859
11 klee            0x00000000004f48bf klee::TxTree::subsumptionCheck(klee::TimingSolver*, klee::ExecutionState&, double) + 223
12 klee            0x0000000000493812 klee::Executor::run(klee::ExecutionState&) + 5442
13 klee            0x0000000000494047 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1703
14 klee            0x0000000000464d5d main + 12765
15 libc.so.6       0x00007fb1b19dc830 __libc_start_main + 240
16 klee            0x000000000046d869 _start + 41

--

********************

[xuanlinhha]

The error from make check I don't know why, I am debugging But I see without the new fix, it already existed.

[xuanlinhha]

Can you check again @rasoolmaghareh ? It is fine on my side now.

[rasoolmaghareh]

@linh, I rechecked and both mack check and make on klee-examples\basic folder pass. I merging this into the master branch.

@sanghu1790 can you please later if this commit affects the scalability on your benchmarks?