[klee-dev] A question about specifying symbolic files

[li peng]

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
-------------- next part --------------
HTML attachment scrubbed and removed