Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

added missing error strings and array entries #479

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

added missing error strings and array entries #479

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
490354b
added missing error strings and array entries
Nov 22, 2023
ec8c9d6
Merge branch 'master' into fix-some-printing
ahmed-irfan Nov 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion src/frontend/yices/yices_parser.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
};

Expand Down
3 changes: 3 additions & 0 deletions src/parser_utils/term_stack_error.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
};

Expand Down