Hi,

On Wed, 7 Jul 2021 17:31:37 +0530 (IST)
kmohit <[email protected]> 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

_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to