diff --git a/tests/pre_post_condition/main.c b/tests/pre_post_condition/main.c index b8ecff0ab..5e7b6d1dd 100644 --- a/tests/pre_post_condition/main.c +++ b/tests/pre_post_condition/main.c @@ -13,6 +13,15 @@ Test(pre_condition, not_a_positive, .exit_code = 10) { f1(-1, &b); } +Test(pre_condition, not_b_non_null, .exit_code = 11) { + f1(1, NULL); +} + +Test(pre_condition, not_b_eq_0, .exit_code = 13) { + b = 1; + f1(1, &b); +} + Test(post_condition, not_b_eq_10, .exit_code = 21) { b = 0; f1(1, &b); diff --git a/tests/pre_post_condition/src.c b/tests/pre_post_condition/src.c index 19d810fcb..f59076ba4 100644 --- a/tests/pre_post_condition/src.c +++ b/tests/pre_post_condition/src.c @@ -18,6 +18,30 @@ void a_positive(int a, int *b) { } } +IA2_PRE_CONDITION(f1) +void b_non_null(int a, int *b) { + if (!b) { + exit(11); + } +} + +IA2_PRE_CONDITION(f1) +void b_eq_0(int a, int *b) { + if (!b) { + return; + } + if (!(*b == 0)) { + exit(13); + } +} + +IA2_POST_CONDITION(f1) +void a_eq_b(int a, int *b) { + if (!(a == *b)) { + exit(20); + } +} + IA2_POST_CONDITION(f1) void b_eq_10(int a, int *b) { if (!(*b == 10)) {