[klee-dev] ERROR 21: Can not open input file: .adl**

[Cristian Cadar]

The POSIX runtime model creates file names 'A', 'B', 'C', etc.  You can 
easily extend the model to support other file names, but this is not 
part of the mainline.

You can read more about --sym-files in this tutorial: 
https://klee.github.io/tutorials/using-symbolic/

Cristian

On 28/05/2020 18:33, Nani Hutagaol wrote:
> Hi all,
> 
> I'm try to run a program that have to read a file. On the readfile 
> function, there's a piece of code like this,,
> ....................
> strcpy(adlfilename, filename);
> strcat(adlfilename, ".adl");
> if ((f = fopen(adlfilename, "r")) == NULL) {
> printf("%s %s", ErrorMessages[21], adlfilename);
> return 21;
> };
> ................
> 
> On shortf explanation, it need an input file with type is .adl,
> 
> On my execution, I run with command:
> klee --only-output-states-covering-new --optimize --libc=uclibc 
>   --max-time=60s --posix-runtime ./program.bc  --sym-args 0 1 2 
> --sym-files 1 10 --sym-stdin 10 --sym-stdout,
> 
> It just need around 2 seconds to stop the execution, because it end with 
> error like this,
> 
> ERROR 21: Can not open input file: .adl** ERROR 21: Can not open input 
> file: /.adl** ERROR 21: Can not open input file: .adl** ERROR 21: Can 
> not open input file: //.adl** ERROR 21: Can not open input file: / 
> .adl** ERROR 21: Can not open input file: /.adl** ERROR 21: Can not open 
> input file: .adl** ERROR 21: Can not open input file: / .adl** ERROR 21: 
> Can not open input file: .adl** ERROR 21: Can not open input file: 
> ///.adl** ERROR 21: Can not open input file: / /.adl** ERROR 21: Can not 
> open input file: // .adl**
> 
> I'm so very confused about that, because I can't move to the next process,
> Btw isn't --sym-files option aims to form symbolic file to be used as 
> input file into the program? So, why it return error can't open input 
> file although I use this option?
> 
> -- 
> Warm Regards
> _Nani Renova Hutagaol_
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>