[klee-dev] symbolic aggregate data structures?

[Cristian Cadar]

Hi Mark, the three approaches should be roughly equivalent (although 
there are some small differences), but in the unlikely event that you 
notice any significant performance differences, please let us know.

Cristian

On 31/03/14 17:18, Mark R. Tuttle wrote:
> Thanks, that's great.  I'm also seeking assurance, I guess, that I'm not
> missing semantic or performance distinctions of significance among
>
>    int a[2];
>    klee_make_symbolic(&a,sizeof(a),"a");
>
> and
>
>    int a[2];
>    a[0] = klee_int("a0");
>    a[1] = klee_int("a1");
>
> and
>
>    int a[2];
>    for (int i=0; i<2; i++) { a[i] = klee_int("a"); }
>
> Thanks,
> Mark
>
>
>
> On Mon, Mar 31, 2014 at 11:22 AM, Cristian Cadar <c.cadar at imperial.ac.uk
> <mailto:c.cadar at imperial.ac.uk>> wrote:
>
>     This is a presentation issue, so the best solution would be to
>     extend the ktest-tool (a small program written in Python) to output
>     data in the desired format.  I would be happy to consider such a patch.
>
>     Best,
>     Cristian
>
>
>     On 31/03/14 02:57, Mark R. Tuttle wrote:
>
>         What is the "right" way to assign symbolic values to aggregate data
>         structures like arrays?
>
>         If I run klee on
>
>         main() {
>             int a[2];
>             klee_make_symbolic(&a,sizeof(__a),"a");
>             return 0;
>         }
>
>         then "ktest-tool --write-ints" displays the array in a rather
>         user-unfriendly way:
>
>         num objects: 1
>         object    0: name: 'a'
>         object    0: size: 8
>         object    0: data: '\x00\x00\x00\x00\x00\x00\x00\__x00'
>
>         If I run klee on
>
>         main(){
>             int a[2];
>             klee_make_symbolic(&a[0],__sizeof(a[0]),"a0");
>             klee_make_symbolic(&a[1],__sizeof(a[1]),"a1");
>             return 0;
>         }
>
>         then klee seems to complain that I'm calling klee_make_symbolic
>         with a
>         pointer into an array and a size that is not the size of the array:
>
>         KLEE: ERROR:
>         /nfs/site/home/mrtuttle/shr/__uefi/ddt/q1/demo2.c:3: wrong
>         size given to klee_make_symbolic[_name]
>
>         If I run klee on
>
>         main(){
>             int a[2];
>             a[0] = klee_int("a0");
>             a[1] = klee_int("a1");
>             return 0;
>         }
>
>         then "ktest-tool --write-ints" displays the array fairly nicely,
>
>         num objects: 2
>         object    0: name: 'a0'
>         object    0: size: 4
>         object    0: data: 0
>         object    1: name: 'a1'
>         object    1: size: 4
>         object    1: data: 0
>
>         This seems the best solution.  But is there a way to extend this to
>         integers of size other than four bytes, to characters, character
>         strings
>         (so that strings print as strings), etc?
>
>         Thanks,
>         Mark
>
>
>
>         _________________________________________________
>         klee-dev mailing list
>         klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>         https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>         <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>     _________________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
>     <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>