[klee-dev] About KLEE Error

Frank Busse f.busse at imperial.ac.uk
Wed Jul 7 13:41:54 BST 2021


Hi,


On Wed, 7 Jul 2021 17:31:37 +0530 (IST)
kmohit <kmohit at cdac.in> wrote:

> Can you give me more details for Model.err.
> This example that you gave is not very obvious to me.If I recall
> size_t takes only 8 bytes.How does that lead to a huge symbolic size?

The error is not raised by klee_make_symbolic but by malloc. As size is
unconstrained, KLEE might allocate up to 18446744073709551615 bytes.
I'd consider that huge.


Kind regards,

Frank



More information about the klee-dev mailing list