Hi Dan. I have markable progress, but klee does not work still.
I am using now klee -libc=uclibc -posix-runtime schedule.o --sym-files 0 10 but, accourding to the tutorial (http://www.cs.purdue.edu/homes/kim1051/cs490/proj3/description.html), i can use klee -libc=uclibc -posix-runtime schedule.o A --sym-files 1 10 and to use file, whose name is in args[1], instead of stdin. But lets check first case. I setted klee_warning_once("w1") before fscanf(stdin, ...) call and klee_warning_once("w2") after fscanf(stdin, ...) call. As the result i have following output: klee -libc=uclibc -posix-runtime schedule.o --sym-files 0 10 KLEE: NOTE: Using model: /home/urmas/forensic/thirdparty-install/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory = "klee-out-55" KLEE: WARNING: undefined reference to function: __isoc99_fscanf KLEE: WARNING: undefined reference to function: fwrite KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 53277392) KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: WARNING ONCE: __user_main: w1 KLEE: WARNING ONCE: calling external: __isoc99_fscanf(53164400, 53153200, 53453008) And execution halts at the fscanf statement again. I think i installed uclibc correctly, as it were necessary to do in http://klee.llvm.org/GetStarted.html but if problem can be in uclibc installation i can try to reinstall it, but i am not sure. The problem is in the same statement as before. Urmas Repinski. Date: Fri, 19 Apr 2013 10:49:34 +0100 Subject: Re: [klee-dev] make reading from file symbolic From: [email protected] To: [email protected] CC: [email protected] Hi Urmas, Are you running the posix runtime (--posix-runtime)? Without the POSIX runtime the following does not work.. $ klee thing.o --help KLEE: output directory = "klee-out-12" KLEE: done: total instructions = 37 KLEE: done: completed paths = 3 where as with the POSIX runtime... $ klee --posix-runtime thing.o --help KLEE: NOTE: Using model: /data/dev/KLEE/klee/bin/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory = "klee-out-13" KLEE: WARNING: undefined reference to function: __xstat64 KLEE: ERROR: /data/dev/KLEE/klee/src/runtime/POSIX/klee_init_env.c:24: klee_init_env usage: (klee_init_env) [options] [program arguments] -sym-arg <N> - Replace by a symbolic argument with length N -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at most MAX arguments, each with maximum length N -sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, each with maximum size N. -sym-stdout - Make stdout symbolic. -max-fail <N> - Allow up to <N> injected failures -fd-fail - Shortcut for '-max-fail 1' KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 100 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 It might be the case that the -sym-arg family of options does not work without POSIX run time being enabled (although I'm not sure). Regards, Dan Liew. On 19 April 2013 07:06, Urmas Repinski <[email protected]> wrote: Hello. I have some program, named schedule.c, that i want symbolically evaluate using klee, to generate inputs. Inside the program i have some fscanf(stdin, "%d", &command) comes, and with "%f" argument also. I want to make this command variable symbolic, no difference to generate symbolic input file for it, ot to make it as usual variable and to generate inputs. When i compile the code with llvm-gcc, then compilation is success and .o file is generated. But when i execute .o file using klee - klee schedule.o I get : KLEE: WARNING: undefined reference to function: __isoc99_fscanf KLEE: WARNING: undefined reference to variable: stdin KLEE: WARNING ONCE: calling external: __isoc99_fscanf(140528011303360, 51367536, 51252160) and no inputs is generated, execution stops. Obviously necessary to replace the reading from stdin by --sym-files parameters, but if i add klee schedule.o --sym-files 0 20 0 - means that no addition files needed, stdin only, and 20 some arbitrary number, size of data. When i hit Ctrl+C then 5 inputs are generated, but not in this variables what i want. Please suggest any possible parameters combination, i think to avoid warnings necessary to remove fscanf from original code, but in this case klee will not know what variables to make symbolic..... Urmas Repinski
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
