[klee-dev] FilePerm.c test fails

[Emil Rakadjiev]

I ran the tests on Ubuntu 12.04 (upstream STP doesn't build, so I used r940); the result is the same, FilePerm.c fails.

But while trying to find out the reason for the test failure, I tried analyzing the assembly.ll files and noticed that they are broken. At least one line is truncated, and not just in the FilePerm.c test files. Examples:

FilePerm.c test:
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt -analyze -view-cfg assembly.ll
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt:assembly.ll:76:1: error: expected end of struct constant

The contents of assembly.ll are:
...
74  @.str23 = private constant [18 x i8] c"ignoring (ENOENT)\00", align 1
75  @__exe_env = global %struct.exe_sym_env_t { [32 x %struct.exe_file_t] [%struct.exe_file_t { i32 0, i32 5, i64 0, %struct.exe_disk_file_t* null }, %struct.exe_file_t { i32 1, i32 9, i64 0, %struct.exe_disk_file_t* null }, %struct.exe_file_t { i32 2, i32 9
76  @.str24 = private constant [6 x i8] c"-stat\00", align 1
...
(the end of line 75 is missing)

---

FD_Fail2.c test:
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt -analyze -view-cfg assembly.ll
/home/er/workspace/llvm-2.9/Release+Asserts/bin/opt: assembly.ll:69:254: error: expected type

The contents of assembly.ll are:
...
68  @unknown.1225 = internal constant [14 x i8] c"Unknown error "
69  @_stdio_streams = internal global [3 x %struct.FILE] [%struct.FILE { i16 544, [2 x i8] zeroinitializer, i32 0, i8* null, i8* null, i8* null, i8* null, i8* null, i8* null, %struct.FILE* getelementptr inbounds ([3 x %struct.FILE]* @_stdio_streams, i64 0, i
70  @stdin = global %struct.FILE* getelementptr inbounds ([3 x %struct.FILE]* @_stdio_streams, i64 0, i64 0)
...
(the end of line 69 is missing)

----

This is probably unrelated to the FilePerm.c test failure, but it'd still be good to know why the lines are truncated.

Thank you,
Emil



PS: A minor correction to my previous email: I noticed that I posted the contents of FilePerm.c.tmp.log, after I manually added "-libc=uclibc" to the special RUN comment, thus there are less warnings. The log of the original, unmodified version is below. This doesn't make any difference in the test outcome, though.
KLEE: NOTE: Using model: /home/er/workspace/klee/build/debug/Debug+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/er/workspace/klee/build/debug/test/Runtime/POSIX/Output/klee-out-44"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: __fgetc_unlocked
KLEE: WARNING: undefined reference to function: __fputc_unlocked
KLEE: WARNING: undefined reference to function: endutent
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to function: getutent
KLEE: WARNING: undefined reference to function: realpath
KLEE: WARNING: undefined reference to function: setutent
KLEE: WARNING: undefined reference to function: stat64
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING: undefined reference to function: strcmp
KLEE: WARNING: undefined reference to function: utmpname
KLEE: WARNING ONCE: calling external: stat64(59728192, 59825904)
KLEE: WARNING ONCE: calling external: __errno_location()
KLEE: WARNING ONCE: calling external: fwrite(59701472, 1, 21, 140474038325696)
Cannot open file 'A'
File 'A' opened successfully

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