From 490354ba299b955bfd7465fd29fd3a89e790cfdc Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 22 Nov 2023 11:59:01 -0800 Subject: [PATCH] added missing error strings and array entries --- src/frontend/yices/yices_parser.c | 9 ++++++++- src/parser_utils/term_stack_error.c | 3 +++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/frontend/yices/yices_parser.c b/src/frontend/yices/yices_parser.c index f3b6980d5..d324fe09e 100644 --- a/src/frontend/yices/yices_parser.c +++ b/src/frontend/yices/yices_parser.c @@ -123,32 +123,39 @@ static error_code_t const tstack_error2yices_error[NUM_TSTACK_ERRORS] = { NO_ERROR, // TSTACK_OP_NOT_IMPLEMENTED UNDEFINED_TERM_NAME, // TSTACK_UNDEF_TERM UNDEFINED_TYPE_NAME, // TSTACK_UNDEF_TYPE + NO_ERROR, // TSTACK_UNDEF_MACRO // TODO find proper code INVALID_RATIONAL_FORMAT, // TSTACK_RATIONAL_FORMAT INVALID_FLOAT_FORMAT, // TSTACK_FLOAT_FORMAT INVALID_BVBIN_FORMAT, // TSTACK_BVBIN_FORMAT INVALID_BVHEX_FORMAT, // TSTACK_BVHEX_FORMAT REDEFINED_TYPE_NAME, // TSTACK_TYPENAME_REDEF REDEFINED_TERM_NAME, // TSTACK_TERMNAME_REDEF + NO_ERROR, // TSTACK_MACRO_REDEF // TODO find proper code DUPLICATE_NAME_IN_SCALAR, // TSTACK_DUPLICATE_SCALAR_NAME DUPLICATE_VAR_NAME, // TSTACK_DUPLICATE_VAR_NAME + NO_ERROR, // TSTACK_DUPLICATE_TYPE_VAR_NAME // TODO find proper code NO_ERROR, // TSTACK_INVALID_OP WRONG_NUMBER_OF_ARGUMENTS, // TSTACK_INVALID_FRAME INTEGER_OVERFLOW, // TSTACK_INTEGER_OVERFLOW NONNEG_INT_REQUIRED, // TSTACK_NEGATIVE_EXPONENT INTEGER_REQUIRED, // TSTACK_NOT_AN_INTEGER + NO_ERROR, // TSTACK_NOT_A_STRING // TODO find proper code SYMBOL_REQUIRED, // TSTACK_NOT_A_SYMBOL RATIONAL_REQUIRED, // TSTACK_NOT_A_RATIONAL TYPE_REQUIRED, // TSTACK_NOT_A_TYPE ARITH_ERROR, // TSTACK_ARITH_ERROR DIVISION_BY_ZERO, // TSTACK_DIVIDE_BY_ZERO NON_CONSTANT_DIVISOR, // TSTACK_NON_CONSTANT_DIVISOR - NEGATIVE_BVSIZE, // TSTACK_NEGATIVE_BVSIZE + NEGATIVE_BVSIZE, // TSTACK_NONPOSITIVE_BVSIZE INCOMPATIBLE_BVSIZES, // TSTACK_INCOMPATIBLE_BVSIZES INVALID_BVCONSTANT, // TSTACK_INVALID_BVCONSTANT BVARITH_ERROR, // TSTACK_BVARITH_ERROR BVARITH_ERROR, // TSTACK_BVLOGIC_ERROR TYPE_MISMATCH_IN_DEF, // TSTACK_TYPE_ERROR_IN_DEFTERM NO_ERROR, // TSTACK_STRINGS_ARE_NOT_TERMS + NO_ERROR, // TSTACK_VARIABLES_VALUES_NOT_MATCHING, // TODO find proper code + NO_ERROR, // TSTACK_NOT_A_CONSTANT, // TODO find proper code + NO_ERROR, // TSTACK_NOT_A_VARIABLE, // TODO find proper code NO_ERROR, // TSTACK_YICES_ERROR }; diff --git a/src/parser_utils/term_stack_error.c b/src/parser_utils/term_stack_error.c index 92b1193c4..e7877b81b 100644 --- a/src/parser_utils/term_stack_error.c +++ b/src/parser_utils/term_stack_error.c @@ -78,6 +78,9 @@ static const char * const code2string[NUM_TSTACK_ERRORS] = { "error in bitvector operation", "incompatible types in define", "strings are not terms", + "variable values are not matching", + "not a constant", + "not a variable", "yices error", };