Hi,
Thanks for answered my question.
But is it possible to find the same error in Klee without using the Klee api's
(Klee_make_symbolic) which you are using in that example, instead of Klee api if
we make Klee symbolic via command line argument ( --sym-stdin). I am not getting
the same error (ptr.err). So could you help me out with any example or any
explanations. Here, the code
#include<stdlib.h>
int global[3];
int main()
{
free(global);
}
Thank you in advance...
Regards,
Mohit
On May 28, 2021 at 7:03 PM Frank Busse <f.bu...@imperial.ac.uk> wrote:
> Hi,
>
>
> On Fri, 28 May 2021 17:37:22 +0530 (IST)
> kmohit <kmo...@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
>
> _______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
For assimilation and dissemination of knowledge, visit cakes.cdac.in
------------------------------------------------------------------------------------------------------------
[ 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.
------------------------------------------------------------------------------------------------------------
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
