Hi Igor,
For this example, I don't think it makes sense to make the pointer
itself symbolic. You could instead replace the klee_make_symbolic call
with klee_make_symbolic(a, sizeof(*a), "a"); to make the malloc'ed
memory symbolic.
If you're interested in symbolic pointers more generally, I would
recommend this paper, which contains in the beginning a discussion of
the different memory models used in symbolic execution (as well as
proposing a new model):
https://srg.doc.ic.ac.uk/publications/19-segmem-esecfse.html
Best,
Cristian
On 09/08/2020 14:45, Breger, Igor (Mobileye) wrote:
Hi all,
I am trying to generate function coverage tests. From the tutorial and
mail-archive I could not understand how I can define pointer as
symbolic and also the data it point to.
In the follow example, if I make a pointer symbolic, most of the tests
KLEE generate are invalid ( 6 of 7 ) . The only valid test is with NULL
values.
I would appreciate any help.
Best Regards,
Igor
#include "klee/klee.h"
#include <stdlib.h>
int get_sign(int *a) {
if ( a == NULL)
return 2;
int x = *a;
if (x == 0)
return 0;
if (x < 0)
return -1;
else
return 1;
}
int main() {
int *a = (int*)malloc(sizeof(int));
klee_make_symbolic(&a, sizeof(a), "a");
return get_sign(a);
}
---------------------------------------------------------------------
Intel Israel (74) Limited
This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.
_______________________________________________
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
