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 <[email protected]
<mailto:[email protected]>> 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
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
