search for: smtlib

...eader name in --help } class llvm::cl::DefaultCategory { virtual const char* getName() { return "General";} virtual const char* getHelpDescription() { return "";} } then clients in their own code could simply implement their own categories by sub-classing e.g. class klee::SMTLIBOptionsCategory : public llvm::cl::OptionCategory { virtual const char* getName() { return "SMTLIB";} virtual const char* getHelpDescription() { return "These options control the behaviour of the SMTLIB printer";} } and now when a client declares an option we could have an a...

...pport for: memcpy, memset, memmove, strlen, strcpy, strncpy, strcat, strncat, strchr, memchr, strcmp, strncmp, memcmp, toupper, tolower, malloc, calloc, free, exit, abort - New options: --max-builtins-iterations, --max-memcpy-iterations, --memcpy=<method> - New, additional output format: SMTLIB (versions 1 and 2) - Support for many GCC/LLVM built-in functions (e.g., __builtin_parity()) - Improved counterexample traces - LLBMC is now based on LLVM 3.1 - New version of STP (revision 1666) - Support for backend solver "MiniSat and propagators" in STP - Option --friendly-proto...

SMT solvers seem more general-purpose than we need. We just need an ILP solver of some kind (Omega, PIP, TaPAS, ...) for almost all uses I can think of. Do you want to do more powerful symbolic analysis for some purpose? --Vikram Associate Professor, Computer Science University of Illinois at Urbana-Champaign http://llvm.org/~vadve On Mar 27, 2009, at 12:08 PM, John Regehr wrote: >

On Wed, 25 Mar 2009, Vikram S. Adve wrote: > We do have a static array bounds checking algorithm based on the Omega > integer programming library, but it is not hugely effective. I think > this can be strengthened a *lot*. I should add that I would be interested in helping with hooking a good decision procedure into LLVM. This will be useful far beyond array bounds check