[klee-dev] Errors Detected by KLEE-2.1

[Frank Busse]

Hi,


On Fri, 28 May 2021 17:37:22 +0530 (IST)
kmohit <kmohit at cdac.in> wrote:

>           I am trying to write a code of free invalid memory for x86
> architecture. And when I was analysis it with Klee, it identified
> exec.err irrespective of free.err.
> So, could you have any examples for free.err or assert.err that
> identified by Klee-2.1

free.err files are only created when you try to free globals or stack
allocations (alloca). Otherwise see:

--
#include <assert.h>
#include <stdlib.h>

int global[3];

int main(void) {
	int sym;
	klee_make_symbolic(&sym, sizeof(sym), "sym");

	switch(sym) {
		case 0:
			assert(sym); // assert.err
			break;
		case 1: {
			free(global); // free.err
			break;
		}
		default: {
			int *p = (int *)(unsigned long)sym; // ptr.err
			free(p);
		}
	}
--

I hope that answers your question.


Kind regards,

Frank