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
