On Fri, Sep 25, 2009 at 7:27 PM, Suhabe Bugrara <suhabe at stanford.edu> wrote:
> Okay, I think the problem is that KLEE doesn't treat the first
> argument as symbolic because it's usually the name of the program, so
> the argv[0][0] expression refers to a concrete value.
Right. We certainly could, it just didn't occur to us at the time, or
it isn't very interesting to spend search time on. See the code around
final_argv = ...
in klee_init_env.c.
Adding a klee_init_env option to support this would be reasonable though.
- Daniel
> Suhabe
>
>
> On Fri, Sep 25, 2009 at 3:17 PM, Suhabe Bugrara <suhabe at stanford.edu>
> wrote:
>> Hello,
>>
>> I'm running KLEE on the following program:
>>
>> int main(int argc, char* argv[]) {
>> ? ? ? ?if (argc >= 1) {
>> ? ? ? ? ? ? ? ?printf("zero ");
>>
>> ? ? ? ? ? ? ? ?if (argv[0][0] == 'c') {
>> ? ? ? ? ? ? ? ? ? ? ? ?printf("one ");
>> ? ? ? ? ? ? ? ?}
>> ? ? ? ? ? ? ? ?else {
>> ? ? ? ? ? ? ? ? ? ? ? ?printf("two ");
>> ? ? ? ? ? ? ? ?}
>> ? ? ? ?}
>> ? ? ? ?else {
>> ? ? ? ? ? ? ? ?printf("three ");
>> ? ? ? ?}
>>
>> ? ? ? ?return 0;
>> }
>>
>> using the following command:
>>
>> klee --libc=klee --posix-runtime --init-env test.bc --sym-args 0 1 15
>>
>> I expected the output to be "zero one two three", but actual output is
>> "zero two". It looks like it's not forking at each of the branches.
>> Any ideas on where I'm going wrong?
>>
>> Thanks.
>>
>> Suhabe
>>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
