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