Hi Mohit,
On Tue, 8 Jun 2021 10:00:50 +0530 (IST) kmohit <[email protected]> wrote: > I want to generate model error through KLEE . For that , I > wrote source code using malloc for encoutering model error. model.err is only generated for huge symbolic sizes, e.g.: -- #include "klee/klee.h" #include <stdlib.h> int main(void) { size_t size; klee_make_symbolic(&size, sizeof(size_t), "size"); char * p = malloc(size); } -- Kind regards, Frank _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
