[HW7] Is "CROWN_REPLAY" correct?

[frogfrog2]

#ifdef CROWN
    SYM_int(...); ...
#ifndef CROWN_REPLAY
    printf("test\n");
    SYM_assume(...); ...
#endif
#else
    ...
#endif

I added the above code into tcas-mod-crown.c file. After using crownc and run_crown, I'm trying to run "crown_replay ./tcas-mod-crown_replay -d test-dir". However, "test" is printed for each test case, even though I'm using crown_replay. Am I doing something wrong? Any help would be appreciated!

[yheechan]

Observation

From the last slide of lec32-crown_tutorial-v3.pdf, it seems crownc should build <target>_replay binary file with -DCROWN_REPLAY. However, when building our concolic testing code with crownc, through the command line output, it can be seen that <target>_replay binary file is actually not built with -DCROWN_REPLAY option.

Quesiton: Is there any other flags we have to add as an option to crownc to make SYM_assume(..) codes ineffective through CROWN_REPLAY variable?

This is what the standard output results (specifically about <target>_replay binary) when building concolic testing code with crownc:

gcc -o tcas-mod-crown_replay tcas-mod-crown.c -I/usr/lib/CROWN_tc_generator/bin/../include -L/usr/lib/CROWN_tc_generator/bin/../lib -lcrown-replay --coverage -Wno-attributes -lpthread

As seen in the output results, <target>_replay binary is actually not built with -DCROWN_REPLAY flag.

My current TEMPORARY solution

After building your concolic testing code with crown, temporary solution can be manually executing the command to build your <target>_replay binary with -DCROWN_REPLAY flag on.

gcc -o tcas-mod-crown_replay tcas-mod-crown.c -I/usr/lib/CROWN_tc_generator/bin/../include -L/usr/lib/CROWN_tc_generator/bin/../lib -lcrown-replay --coverage -Wno-attributes -lpthread -DCROWN_REPLAY

This prevented printf("test\n"); to be executed (as of your example @frogfrog2 ).

[3-24]

I patched crownc to support CROWN_REPLAY flag. Thank you for reporting this.