tests: add multiple pre- and post-conditions to pre_post_condition

immunant · Mar 3, 2025 · 931ae8b · 931ae8b
1 parent dd59186
commit 931ae8b
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 0 deletions.
diff --git 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
@@ -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)) {