KLEE isn't great with completely symbolic link lists. The pointer could point to **anything** so in order to be complete KLEE must consider every object allocated in memory. This does not scale very well.
On 3 October 2013 18:06, Saikat Dutta <[email protected]> wrote: > Thanks. > But what about linked lists? If there exists a next pointer in a structure, > will it be taken care of by klee?Or do i need to fix the length of linked > list and declare every instance of that structure symbolically?I m a bit > confused. > > > On Thu, Oct 3, 2013 at 9:04 PM, Daniel Liew <[email protected]> > wrote: >> >> KLEE models memory at the bytes level so you can things like this... >> >> include <stdio.h> >> >> int main(int argc, char** argv) >> { >> typedef struct >> { >> int a; >> int b; >> } A; >> >> A instance; >> >> klee_make_symbolic(&instance, sizeof(A)); >> >> if ( instance.a > 0 ) >> printf("instance.a >0\n"); >> else >> printf("instance.a <=0\n"); >> >> } >> >> As for "Normally big application have..." that totally depends on what >> sort of programs you are talking about. KLEE has built-in support for >> declaring symbolic command line arguments and symbolic files as >> command line arguments for convenience. You can get info on the is by >> running >> >> $ klee --posix-runtime <program>.bc --help >> >> usage: (klee_init_env) [options] [program arguments] >> -sym-arg <N> - Replace by a symbolic argument with length N >> -sym-args <MIN> <MAX> <N> - Replace by at least MIN arguments and at >> most >> MAX arguments, each with maximum length N >> -sym-files <NUM> <N> - Make stdin and up to NUM symbolic files, >> each >> with maximum size N. >> -sym-stdout - Make stdout symbolic. >> -max-fail <N> - Allow up to <N> injected failures >> -fd-fail - Shortcut for '-max-fail 1' >> >> See the Coreutils webpage >> (http://ccadar.github.io/klee/TestingCoreutils.html) for an example of >> how to use these >> >> On 3 October 2013 15:46, Saikat Dutta <[email protected]> >> wrote: >> > Hi, >> > Normally big application have structures and linked lists or arrays of >> > such >> > structures as inputs to functions. Is there an easy way to symbolically >> > declare them using klee? Or does one have to declare each of their >> > component >> > primitive variables? >> > Thanks. >> > -Saikat > > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
