[klee-dev] Fwd: create ponter/array access bounds expressions with klee

[Eric Lu]

Hi, Paul
Thanks for your reply.

What I want to generate a expression for pointers to express the memory
space. I.E.

    int *ptr;
    int a[N], b[(a+1)*N];
    for( i = 0; i < N; i++){
      ptr++;
      array[i] += i + 2;
      ptr++;
      b[a*i+1] = i;
   }

   We get the access region expression for each variable:
   1)  ptr: (start_address: ptr, upbound:2*N, lowerbound: 0 )
   2) a: ( &a[0], N, 0);
  3) b:  (&b[1], a*N, 1);

Can klee do this? I have look through the mail list, there seems no subject
related to this case.


On Fri, Jun 14, 2013 at 4:46 PM, Paul Marinescu <
paul.marinescu at imperial.ac.uk> wrote:

> Hi,
> KLEE does generate symbolic expressions to check for out-of-bounds memory
> access. If you are looking for something specific, you may get more answers
> if you explain it in a few sentences, rather than expect people to read the
> whole paper.
>
> Best,
> Paul
>
> On 14 Jun 2013, at 08:31, Eric Lu <eirc.lew at gmail.com> wrote:
>
> Hello,
>
>   I want to generate pointer/array access bounds expressions with KLEE in
> LLVM. I am new to symbolic execution and KLEE, and I am not sure if  some
> body have done this before?
>
>   What I need is something like symbolic execution in [1]， is it possible
> to implement [1] based KLEE?
>
>    Or are there some better ways to do this?  Any advice is welcome!
>
>
> [1]   Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed
> Memory Regions
>
>
> Thanks!
>
> Eric
>  _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed