Requesting example of running symcc with symbolic input file

[AndrewQuijano]

I was hoping to get familiar with using symcc, but with files. I see the option to set an environment variable to have an input file. However, when I built this executable locally, I am not getting any results. What am I doing wrong such that I am not getting more results? How would I get this working with the concolic script?

Here is the code

`#include

include

include <sys/types.h>

include <sys/uio.h>

include

include

int main(int argc, char **argv) { if (argc < 2) { fprintf(stderr, "usage: %s inputfile\n", argv[0]); return 1; } int fd = open(argv[1], O_RDONLY); char buf[64] = {}; int r = read(fd, buf, 64); if (r < 5) { fprintf(stderr, "Need at least five characters of input\n"); return 1; } buf[63] = '\0'; if (buf[0] == 'h' && buf[1] == 'e' && buf[2] == 'l' && buf[3] == 'l' && buf[4] == 'o') { printf("Bug!!\n"); return 1; } else { printf("%s\n", buf); return 0; } }`

[AndrewQuijano]

Actually, realized it seems my issue was the length does not change, so I created a file called testing.txt with content hella

[AndrewQuijano]

[AndrewQuijano]

find ./results/ -type f -print -exec hexdump -C {} \;

Then I would use ../util/pure_concolic_execution.sh -i ./input/ -o ./output/ ./test_file @@ to have my program run with concolic execution, the @@ is since I am using input files to the executable.

[sebastianpoeplau]

That's correct, SymCC doesn't change the length of your input. With C and C++ strings you can often work around this limitation by creating a relatively large input file and relying on SymCC to put a null character in the right place to terminate the string early. (In that sense, SymCC can shorten the input...)