diff --git a/src/ae_assert_tests/NULL_1.c b/src/ae_assert_tests/NULL_1.c new file mode 100644 index 00000000..520dbbcc --- /dev/null +++ b/src/ae_assert_tests/NULL_1.c @@ -0,0 +1,9 @@ +#include "stdbool.h" +#include +extern void svf_assert(bool); + +int main() { + int *ptr = NULL; + svf_assert(ptr == NULL); + return 0; +} diff --git a/src/ae_assert_tests/NULL_2.c b/src/ae_assert_tests/NULL_2.c new file mode 100644 index 00000000..2a14153f --- /dev/null +++ b/src/ae_assert_tests/NULL_2.c @@ -0,0 +1,10 @@ +#include "stdbool.h" +#include +extern void svf_assert(bool); + +int main() { + int value = 10; + int *ptr = &value; + svf_assert(ptr != NULL); + return 0; +} diff --git a/src/ae_assert_tests/NULL_3.c b/src/ae_assert_tests/NULL_3.c new file mode 100644 index 00000000..c8b9893a --- /dev/null +++ b/src/ae_assert_tests/NULL_3.c @@ -0,0 +1,15 @@ +#include "stdbool.h" +#include +extern void svf_assert(bool); + +int main() { + int *ptr = NULL; + bool isNullDereference = false; + + if (ptr == NULL) { + isNullDereference = true; + } + + svf_assert(isNullDereference); + return 0; +} diff --git a/src/ae_assert_tests/NULL_4.c b/src/ae_assert_tests/NULL_4.c new file mode 100644 index 00000000..bf484113 --- /dev/null +++ b/src/ae_assert_tests/NULL_4.c @@ -0,0 +1,12 @@ +#include "stdbool.h" +#include +extern void svf_assert(bool); + +int main() { + int *a[3][3] = {NULL}; + + bool isNull = (a[0][0] == NULL); + svf_assert(isNull); + + return 0; +}