From e036a5bd9bf20106e174c793ea9e23f17775ce6c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 May 2024 18:06:18 -0700 Subject: [PATCH] add parameter validation to ternary and 4-ary functions for API #7219 Signed-off-by: Nikolaj Bjorner --- src/api/api_util.h | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/api/api_util.h b/src/api/api_util.h index 7b16229f4..e02ac6fee 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -147,6 +147,9 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) { \ Z3_TRY; \ RESET_ERROR_CODE(); \ EXTRA_CODE; \ + CHECK_IS_EXPR(n1, nullptr); \ + CHECK_IS_EXPR(n2, nullptr); \ + CHECK_IS_EXPR(n3, nullptr); \ expr * args[3] = { to_expr(n1), to_expr(n2), to_expr(n3) }; \ ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 3, args); \ mk_c(c)->save_ast_trail(a); \ @@ -164,6 +167,10 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) { \ Z3_TRY; \ RESET_ERROR_CODE(); \ EXTRA_CODE; \ + CHECK_IS_EXPR(n1, nullptr); \ + CHECK_IS_EXPR(n2, nullptr); \ + CHECK_IS_EXPR(n3, nullptr); \ + CHECK_IS_EXPR(n4, nullptr); \ expr * args[4] = { to_expr(n1), to_expr(n2), to_expr(n3), to_expr(n4) }; \ ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 4, args); \ mk_c(c)->save_ast_trail(a); \