[klee-dev] About KLEE Error

[kmohit]

Hi,
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?


Thank you and kind regards,
Mohit kumar


On June 17, 2021 at 1:13 AM Frank Busse <f.busse at imperial.ac.uk> wrote:
> 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
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
------------------------------------------------------------------------------------------------------------
[ C-DAC is on Social-Media too. Kindly follow us at:
Facebook: https://www.facebook.com/CDACINDIA & Twitter: @cdacindia ]

This e-mail is for the sole use of the intended recipient(s) and may
contain confidential and privileged information. If you are not the
intended recipient, please contact the sender by reply e-mail and destroy
all copies and the original message. Any unauthorized review, use,
disclosure, dissemination, forwarding, printing or copying of this email
is strictly prohibited and appropriate legal action will be taken.
------------------------------------------------------------------------------------------------------------

-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.jpg
Type: image/jpeg
Size: 7789 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20210707/b58b9205/attachment.jpg>