Re: [klee-dev] Klee & pointers
Hi Cristian, Thank you very much for the prompt reply. Regards, Igor -Original Message- From: klee-dev-boun...@imperial.ac.uk On Behalf Of Cristian Cadar Sent: Wednesday, August 12, 2020 17:19 To: klee-dev@imperial.ac.uk Subject: Re: [klee-dev] Klee & pointers 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 > > 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(, 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 > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev - 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 klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Klee & pointers
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 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(, 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 klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Klee & pointers
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 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(, 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 klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev