mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

add parameter validation to ternary and 4-ary functions for API #7219

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-11 18:06:18 -07:00
parent efc893263a
commit e036a5bd9b
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_util.h
View file

@ -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); \