[klee-dev] A question about specifying symbolic files

[Daniel Schwartz]

Hi Peng,

You need to give the symbolic file a "name", that will then be given
symbolic value.
Try "klee --posix-runtime --libc=uclibc xxx.bc A --sym-files 1 1024".

You should be able to print argv[1] and see that it's "A".


Best,
Daniel Schwartz

On Sat, Sep 30, 2017 at 1:16 AM, li peng <poppeter1982 at gmail.com> wrote:

> Hi All
>
> I have question about how to set a symbolic file in POSIX runtime.
>
> Suppose I have the following snippet of code:
>
> #include <stdio.h>
>
> #include <stdlib.h>
>
> #include <string.h>
>
>
> int main(int argc, char** argv) {
>
>   char* filename = argv[1];
>
>   char *buf = (char*)malloc(2);
>
>
>   FILE* fd = fopen(filename, "r");
>
>   if (fd != NULL) {
>
>     char *line = NULL;
>
>     size_t len = 0;
>
>     ssize_t read;
>
>
>     while ((read = getline(&line, &len, fd)) != -1) {
>
>       char buffer[1024];
>
>       strcpy(buffer, line);
>
>       buffer[strcspn(buffer, "\r\n")] = 0;
>
>
>       if (strcmp(buffer, "abc") == 0) {
>
>         printf(">>> buffer is abc \n");
>
>         free(buf);
>
>       } else {
>
>         if (strcmp(buffer, "abcd") == 0) {
>
>           // OOB here
>
>           printf(">>> buffer is abcd \n");
>
>           buf[3] = 'c';
>
>         }
>
>       }
>
>     }
>
>   }
>
>   fclose(fd);
>
>   return 0;
>
> }
>
> Regarding this program, can you please show how to specify the symbolic
> file as the first argument? I tried the command "klee --posix-runtime
> --libc=uclibc xxx.bc --sym-files 1 1024", but it does not work.
>
> Answers are highly appreciated!
>
> Thanks
>
> Peng
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed