[klee-dev] FilePerm.c test fails

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev