Hello KLEE developers, I am trying to understand how KLEE emulates environment variables. In particular, how do functions like getopt_long get executed with KLEE, when we give --sym-arg as an argument. getopt_long is found in unistd.h, and is available in uclibc. For a coreutils file like groups.c where the following line is encountered:
while ((optc = getopt_long (argc, argv, "", longopts, NULL)) != -1) how would KLEE generate different inputs? for simplicity, consider the case where we use --sym-arg 1 10 as a command line argument which leads to argv[1] becoming a symbolic buffer of size 10, if my understanding is correct, when getopt_long is called, one of the two things can happen: 1) argv[1] is declared as a symbolic buffer, we explore all paths of getopt_long code in uclibc library, so all different if's / elses in getopt_long code will get forked and execute to give different optc values. 2) getopt_long is skipped, optc variable is made symbolic, and the main function in groups.c treats optc as symbolic value. on any successive if/else condition in groups.c containing optc, a new state is forked with new value of optc. Is there a third (correct) way? Please advise. Thanks and Regards, Shehbaz Jaffer _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
