Hi, Yes, you cannot directly mark a single field as symbolic. Simply declare an auxiliary variable of the right type, mark it as symbolic, and then memcpy it into the desired field.
You can also look at this thread for more details: http://keeda.stanford.edu/pipermail/klee-dev/2011-July/000682.html Cristian On 04/06/2012 08:45 AM, Ryan Govostes wrote: > I would expect the following to work: > > %<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%< > > struct > { > char fieldA[256]; > char fieldB[256]; > } thing; > > klee_make_symbolic(thing.fieldB, sizeof(thing.fieldB), "fieldB"); > > %<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%<%< > > However, this fails with > > KLEE: ERROR: memory error: invalid pointer: make_symbolic > > It seems like I can make the entire struct symbolic, but not a single member. > Is this accurate? What is the reason behind this limitation? > > Thanks, > Ryan Govostes > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
