[klee-dev] make reading from file symbolic

[Daniel Liew]

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 <urrimus at hotmail.com> 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
>
-------------- next part --------------
HTML attachment scrubbed and removed