[klee-dev] About KLEE Error

[Frank Busse]

Hi Mohit,


On Tue, 8 Jun 2021 10:00:50 +0530 (IST)
kmohit <kmohit at cdac.in> 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