Hi Emil,
Lines are truncated to go over a kcachegrind bug; to avoid this problem,
just pass -no-truncate-source-lines to KLEE.
I'm not sure why FilePerm.c fails on your machine, it might be a fragile
test. But I noticed that you run the test with uclibc enabled, while
the default configuration is to run w/o uclibc. Have you changed some
of the default options?
Cristian
On 22/08/14 12:30, Emil Rakadjiev wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
