NuSMV Developers Manual: NuSMV/code/nusmv/core/utils/ErrorMgr.h Source File

00001 /* ---------------------------------------------------------------------------
00002 
00003 
00004   This file is part of the ``utils'' package of NuSMV version 2.
00005   Copyright (C) 2011 by FBK-irst.
00006 
00007   NuSMV version 2 is free software; you can redistribute it and/or
00008   modify it under the terms of the GNU Lesser General Public
00009   License as published by the Free Software Foundation; either
00010   version 2 of the License, or (at your option) any later version.
00011 
00012   NuSMV version 2 is distributed in the hope that it will be useful,
00013   but WITHOUT ANY WARRANTY; without even the implied warranty of
00014   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00015   Lesser General Public License for more details.
00016 
00017   You should have received a copy of the GNU Lesser General Public
00018   License along with this library; if not, write to the Free Software
00019   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
00020 
00021   For more information on NuSMV see <http://nusmv.fbk.eu>
00022   or email to <nusmv-users@fbk.eu>.
00023   Please report bugs to <nusmv-users@fbk.eu>.
00024 
00025   To contact the NuSMV development board, email to <nusmv@fbk.eu>. 
00026 
00027 -----------------------------------------------------------------------------*/
00028 
00039 #ifndef __NUSMV_CORE_UTILS_ERROR_MGR_H__
00040 #define __NUSMV_CORE_UTILS_ERROR_MGR_H__
00041 
00042 #include "nusmv/core/utils/utils.h"
00043 #include "nusmv/core/cinit/NuSMVEnv.h"
00044 #include "nusmv/core/prop/Prop.h"
00045 #include "nusmv/core/utils/StreamMgr.h"
00046 #include "nusmv/core/opt/opt.h"
00047 #include "nusmv/core/node/NodeMgr.h"
00048 #include "nusmv/core/node/printers/MasterPrinter.h"
00049 #include "nusmv/core/utils/UStringMgr.h"
00050 
00057 typedef struct ErrorMgr_TAG*  ErrorMgr_ptr;
00058 
00059 
00060 typedef enum FailureKind_TAG {
00061   FAILURE_DIV_BY_ZERO,
00062   FAILURE_CASE_NOT_EXHAUSTIVE,
00063   FAILURE_ARRAY_OUT_OF_BOUNDS,
00064   FAILURE_UNSPECIFIED
00065 } FailureKind;
00066 
00073 #define ERROR_MGR(self) \
00074          ((ErrorMgr_ptr) self)
00075 
00081 #define ERROR_MGR_CHECK_INSTANCE(self) \
00082          (nusmv_assert(ERROR_MGR(self) != ERROR_MGR(NULL)))
00083 
00084 /*@-skipposixheaders@*/
00085 /*@-skipisoheaders@*/
00086 #include <setjmp.h>
00087 /*@=skipposixheaders@*/
00088 /*@=skipisoheaders@*/
00089 /* New versions of cygwin do not need special treatments */
00090 /* #ifdef __CYGWIN__  */
00091 /* #define JMPBUF jmp_buf */
00092 /* #define SETJMP(buf,val) setjmp(buf) */
00093 /* #define LONGJMP(buf,val) longjmp(buf, val) */
00094 /* #else */
00095 #if defined(__MINGW32__) || defined(_MSC_VER)
00096 
00102 #define JMPBUF jmp_buf
00103 
00109 #define SETJMP(buf,val) setjmp(buf)
00110 
00116 #define LONGJMP(buf,val) longjmp(buf, val)
00117 #else
00118 #define JMPBUF sigjmp_buf
00119 #define SETJMP(buf,val) sigsetjmp(buf, val)
00120 #define LONGJMP(buf,val) siglongjmp(buf, val)
00121 #endif
00122 /* #endif */
00123 
00124 /* warning take care not to do something like this:
00125 
00126   CATCH(errmgr) {
00127      cmd1....
00128      return 1;
00129   } FAIL(errmgr) {
00130      cmd2...
00131     return 0;
00132   }
00133 
00134   The right way to use it is:
00135 
00136   {
00137     type result;
00138 
00139     CATCH(errmgr) {
00140      cmd1....
00141      result = value;
00142     } FAIL(errmgr) {
00143      cmd2...
00144      result = 1;
00145     }
00146     return(result);
00147   }
00148   I.e. return inside CATCH/FAIL may cause damage of the stack
00149 */
00150 
00151 /* To exploit the CATCH/FAIL mechanism, you can use any ErrorMgr exit function */
00152 
00158 #define ErrorMgr_set_long_jmp(err)              \
00159   SETJMP(*(ErrorMgr_new_long_jmp(err)), 1)
00160 
00166 #define CATCH(err) if (ErrorMgr_set_long_jmp(err) == 0) {
00167 
00173 #define FAIL(err)  ErrorMgr_cancel_long_jmp(err); } else
00174 
00175 
00176 
00179 /*---------------------------------------------------------------------------*/
00180 /* Function prototypes                                                       */
00181 /*---------------------------------------------------------------------------*/
00182 
00197 ErrorMgr_ptr ErrorMgr_create(const NuSMVEnv_ptr env);
00198 
00207 void ErrorMgr_destroy(ErrorMgr_ptr self);
00208 
00215 StreamMgr_ptr
00216 ErrorMgr_get_stream_manager(const ErrorMgr_ptr self);
00217 
00224 UStringMgr_ptr
00225 ErrorMgr_get_string_manager(const ErrorMgr_ptr self);
00226 
00233 OptsHandler_ptr
00234 ErrorMgr_get_options_handler(const ErrorMgr_ptr self);
00235 
00242 node_ptr ErrorMgr_get_the_node(const ErrorMgr_ptr self);
00243 
00250 void ErrorMgr_set_the_node(ErrorMgr_ptr self, node_ptr node);
00251 
00262 JMPBUF*
00263 ErrorMgr_new_long_jmp(ErrorMgr_ptr self);
00264 
00277 void
00278 ErrorMgr_long_jmp(ErrorMgr_ptr self);
00279 
00288 void
00289 ErrorMgr_cancel_long_jmp(ErrorMgr_ptr self);
00290 
00300 void
00301 ErrorMgr_reset_long_jmp(ErrorMgr_ptr self);
00302 
00315 void
00316 ErrorMgr_start_parsing_err(ErrorMgr_ptr self);
00317 
00328 void
00329 ErrorMgr_finish_parsing_err (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
00330 
00342 void
00343 ErrorMgr_nusmv_exit (ErrorMgr_ptr self, int n) NUSMV_FUNCATTR_NORETURN;
00344 
00354 void
00355 ErrorMgr_rpterr (ErrorMgr_ptr self, const char* fmt, ...) NUSMV_FUNCATTR_NORETURN;
00356 
00367 void
00368 ErrorMgr_rpterr_node (ErrorMgr_ptr self, node_ptr node,
00369                            const char* fmt, ...) NUSMV_FUNCATTR_NORETURN;
00370 
00378 void ErrorMgr_error_msg(const ErrorMgr_ptr self,
00379                                const char* format, ...);
00380 
00389 void ErrorMgr_warning_msg(ErrorMgr_ptr self,
00390                                  const char * fmt, ...);
00391 
00398 boolean
00399 ErrorMgr_io_atom_is_empty(ErrorMgr_ptr self);
00400 
00407 void
00408 ErrorMgr_io_atom_push(ErrorMgr_ptr self, node_ptr s);
00409 
00416 void
00417 ErrorMgr_io_atom_pop(ErrorMgr_ptr self);
00418 
00425 node_ptr
00426 ErrorMgr_io_atom_head(ErrorMgr_ptr self);
00427 
00434 void
00435 ErrorMgr_print_io_atom_stack(ErrorMgr_ptr self);
00436 
00446 void
00447 ErrorMgr_internal_error (ErrorMgr_ptr self,
00448                               const char * fmt, ...) NUSMV_FUNCATTR_NORETURN;
00449 
00456 void
00457 ErrorMgr_error_multiple_substitution (ErrorMgr_ptr self,
00458                                            node_ptr nodep) NUSMV_FUNCATTR_NORETURN;
00459 
00466 void
00467 ErrorMgr_report_failure_node (ErrorMgr_ptr self, node_ptr n) NUSMV_FUNCATTR_NORETURN;
00468 
00475 void
00476 ErrorMgr_warning_failure_node(ErrorMgr_ptr self, node_ptr n);
00477 
00484 void ErrorMgr_warning_case_not_exhaustive(ErrorMgr_ptr self,
00485                                                  node_ptr failure);
00486 
00493 void
00494 ErrorMgr_warning_possible_div_by_zero(ErrorMgr_ptr self,
00495                                       node_ptr failure);
00496 
00503 void
00504 ErrorMgr_warning_possible_array_out_of_bounds(ErrorMgr_ptr self,
00505                                               node_ptr failure);
00506 
00513 void
00514 ErrorMgr_error_array_out_of_bounds (ErrorMgr_ptr self,
00515                                          int index, int low, int high) NUSMV_FUNCATTR_NORETURN;
00516 
00523 void
00524 ErrorMgr_error_lhs_of_index_is_not_array (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
00525 
00532 void
00533 ErrorMgr_error_div_by_zero (ErrorMgr_ptr self, node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00534 
00541 void
00542 ErrorMgr_error_div_by_nonconst (ErrorMgr_ptr self, node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00543 
00544 
00551 void ErrorMgr_error_mod_by_nonword (ErrorMgr_ptr self, node_ptr expr);
00552 
00559 void
00560 ErrorMgr_type_error (ErrorMgr_ptr self, node_ptr n) NUSMV_FUNCATTR_NORETURN;
00561 
00568 void
00569 ErrorMgr_range_error (ErrorMgr_ptr self, node_ptr n, node_ptr var) NUSMV_FUNCATTR_NORETURN;
00570 
00577 void
00578 ErrorMgr_range_warning(ErrorMgr_ptr self, node_ptr n, node_ptr var);
00579 
00586 void
00587 ErrorMgr_error_multiple_assignment (ErrorMgr_ptr self, node_ptr t1) NUSMV_FUNCATTR_NORETURN;
00588 
00595 void
00596 ErrorMgr_error_empty_range (ErrorMgr_ptr self, node_ptr name, int dim1, int dim2) NUSMV_FUNCATTR_NORETURN;
00597 
00604 void
00605 ErrorMgr_error_not_word_wsizeof (ErrorMgr_ptr self, node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00606 
00613 void
00614 ErrorMgr_error_not_constant_extend_width (ErrorMgr_ptr self,
00615                                                const node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00616 
00623 void
00624 ErrorMgr_error_not_constant_resize_width (ErrorMgr_ptr self,
00625                                                const node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00626 
00633 void
00634 ErrorMgr_error_not_constant_wtoint (ErrorMgr_ptr self, const node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00635 
00642 void
00643 ErrorMgr_error_not_constant_width_of_word_type (ErrorMgr_ptr self,
00644                                                      node_ptr name) NUSMV_FUNCATTR_NORETURN;
00645 
00652 void
00653 ErrorMgr_error_not_constant_width_of_word_array_type (ErrorMgr_ptr self,
00654                                                            node_ptr name) NUSMV_FUNCATTR_NORETURN;
00655 
00662 void
00663 ErrorMgr_error_not_constant_width_of_array_type (ErrorMgr_ptr self,
00664                                                       node_ptr name) NUSMV_FUNCATTR_NORETURN;
00665 
00672 void
00673 ErrorMgr_error_wrong_word_operand (ErrorMgr_ptr self,
00674                                         const char* msg, node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00675 
00682 void
00683 ErrorMgr_error_assign_both (ErrorMgr_ptr self, node_ptr v, node_ptr v1,
00684                                  int lineno, int lineno2) NUSMV_FUNCATTR_NORETURN;
00685 
00692 void
00693 ErrorMgr_error_unknown_var_in_order_file (ErrorMgr_ptr self, node_ptr n) NUSMV_FUNCATTR_NORETURN;
00694 
00701 void
00702 ErrorMgr_warning_variable_not_declared(ErrorMgr_ptr self, node_ptr vname);
00703 
00710 void
00711 ErrorMgr_warning_missing_variable(ErrorMgr_ptr self, node_ptr vname);
00712 
00719 void
00720 ErrorMgr_warning_missing_variables(ErrorMgr_ptr self,
00721                                    NodeList_ptr vars_list);
00722 
00729 void
00730 ErrorMgr_warning_non_ag_only_spec(ErrorMgr_ptr self, Prop_ptr prop);
00731 
00738 void
00739 ErrorMgr_warning_ag_only_without_reachables(ErrorMgr_ptr self);
00740 
00747 void
00748 ErrorMgr_warning_fsm_init_empty(ErrorMgr_ptr self);
00749 
00756 void
00757 ErrorMgr_warning_fsm_invar_empty(ErrorMgr_ptr self);
00758 
00765 void
00766 ErrorMgr_warning_fsm_fairness_empty(ErrorMgr_ptr self);
00767 
00774 void
00775 ErrorMgr_warning_fsm_init_and_fairness_empty(ErrorMgr_ptr self);
00776 
00783 void
00784 ErrorMgr_error_var_appear_twice_in_order_file (ErrorMgr_ptr self,
00785                                                     node_ptr n) NUSMV_FUNCATTR_NORETURN;
00786 
00793 void
00794 ErrorMgr_warning_var_appear_twice_in_order_file(ErrorMgr_ptr self,
00795                                                 node_ptr n);
00796 
00803 void
00804 ErrorMgr_warning_id_appears_twice_in_idlist_file(ErrorMgr_ptr self,
00805                                                  node_ptr n);
00806 
00813 void
00814 ErrorMgr_error_var_not_in_order_file (ErrorMgr_ptr self, node_ptr n) NUSMV_FUNCATTR_NORETURN;
00815 
00822 void
00823 ErrorMgr_error_not_proper_number (ErrorMgr_ptr self,
00824                                        const char* op, node_ptr n) NUSMV_FUNCATTR_NORETURN;
00825 
00832 void
00833 ErrorMgr_error_not_proper_numbers (ErrorMgr_ptr self, const char* op,
00834                                         node_ptr n1, node_ptr n2) NUSMV_FUNCATTR_NORETURN;
00835 
00842 void
00843 ErrorMgr_error_ambiguous (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00844 
00851 void
00852 ErrorMgr_error_undefined (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00853 
00860 void
00861 ErrorMgr_error_shadowing (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00862 
00869 void
00870 ErrorMgr_error_redefining (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00871 
00878 void
00879 ErrorMgr_error_redefining_operational_symbol (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00880 
00887 void
00888 ErrorMgr_error_redefining_input_var (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00889 
00896 void
00897 ErrorMgr_error_reassigning (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00898 
00905 void
00906 ErrorMgr_error_assign_input_var (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00907 
00914 void
00915 ErrorMgr_error_assign_frozen_var (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00916 
00923 void
00924 ErrorMgr_error_assign_expected_var (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00925 
00932 void
00933 ErrorMgr_error_circular (ErrorMgr_ptr self, node_ptr s) NUSMV_FUNCATTR_NORETURN;
00934 
00941 void
00942 ErrorMgr_error_too_many_vars (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
00943 
00950 void
00951 ErrorMgr_error_out_of_memory (ErrorMgr_ptr self, size_t size) NUSMV_FUNCATTR_NORETURN;
00952 
00959 void
00960 ErrorMgr_error_invalid_subrange (ErrorMgr_ptr self, node_ptr range) NUSMV_FUNCATTR_NORETURN;
00961 
00968 void
00969 ErrorMgr_error_invalid_bool_cast (ErrorMgr_ptr self, node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00970 
00977 void
00978 ErrorMgr_error_out_of_bounds_word_toint_cast (ErrorMgr_ptr self,
00979                                                    node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00980 
00987 void
00988 ErrorMgr_error_invalid_toint_cast (ErrorMgr_ptr self, node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00989 
00996 void
00997 ErrorMgr_error_invalid_count_operator (ErrorMgr_ptr self, node_ptr expr) NUSMV_FUNCATTR_NORETURN;
00998 
01005 void
01006 ErrorMgr_error_invalid_enum_value (ErrorMgr_ptr self, node_ptr value) NUSMV_FUNCATTR_NORETURN;
01007 
01014 void
01015 ErrorMgr_error_game_definition_contains_input_vars (ErrorMgr_ptr self,
01016                                                          node_ptr var_name) NUSMV_FUNCATTR_NORETURN;
01017 
01024 void
01025 ErrorMgr_error_property_contains_input_vars (ErrorMgr_ptr self,
01026                                                   Prop_ptr prop) NUSMV_FUNCATTR_NORETURN;
01027 
01034 void
01035 ErrorMgr_error_assign_exp_contains_input_vars (ErrorMgr_ptr self,
01036                                                     node_ptr exp) NUSMV_FUNCATTR_NORETURN;
01037 
01044 void
01045 ErrorMgr_error_next_exp_contains_input_vars (ErrorMgr_ptr self,
01046                                                   node_ptr exp) NUSMV_FUNCATTR_NORETURN;
01047 
01054 void
01055 ErrorMgr_error_invar_exp_contains_input_vars (ErrorMgr_ptr self,
01056                                                    node_ptr exp) NUSMV_FUNCATTR_NORETURN;
01057 
01064 void
01065 ErrorMgr_error_init_exp_contains_input_vars (ErrorMgr_ptr self, node_ptr exp) NUSMV_FUNCATTR_NORETURN;
01066 
01073 void
01074 ErrorMgr_error_second_player_var (ErrorMgr_ptr self, node_ptr exp) NUSMV_FUNCATTR_NORETURN;
01075 
01082 void
01083 ErrorMgr_error_second_player_next_var (ErrorMgr_ptr self, node_ptr exp) NUSMV_FUNCATTR_NORETURN;
01084 
01091 void
01092 ErrorMgr_error_unknown_preprocessor (ErrorMgr_ptr self,
01093                                           const char* prep_name) NUSMV_FUNCATTR_NORETURN;
01094 
01101 void
01102 ErrorMgr_error_set_preprocessor(ErrorMgr_ptr self,
01103                                 const char* name,
01104                                 boolean is_warning);
01105 
01112 void
01113 ErrorMgr_error_type_system_violation (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
01114 
01121 void
01122 ErrorMgr_error_psl_not_supported_feature (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
01123 
01130 void
01131 ErrorMgr_error_psl_not_supported_feature_next_number (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
01132 
01139 void
01140 ErrorMgr_error_not_supported_feature (ErrorMgr_ptr self, const char* msg) NUSMV_FUNCATTR_NORETURN;
01141 
01148 void
01149 ErrorMgr_error_expected_number (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
01150 
01157 void
01158 ErrorMgr_warning_psl_not_supported_feature(ErrorMgr_ptr self,
01159                                            node_ptr psl_spec, int index);
01160 
01167 void
01168 ErrorMgr_error_psl_repeated_replicator_id (ErrorMgr_ptr self) NUSMV_FUNCATTR_NORETURN;
01169 
01176 void
01177 ErrorMgr_error_invalid_number(ErrorMgr_ptr self, const char* szNumber);
01178 
01185 void
01186 ErrorMgr_error_bmc_invalid_k_l(ErrorMgr_ptr self,const int k, const int l);
01187 
01194 void
01195 ErrorMgr_error_property_already_specified(ErrorMgr_ptr self);
01196 
01203 void
01204 ErrorMgr_error_invalid_numeric_value (ErrorMgr_ptr self,
01205                                            int value, const char* reason) NUSMV_FUNCATTR_NORETURN;
01206 
01213 void
01214 ErrorMgr_error_file_not_found (ErrorMgr_ptr self, const char* filename) NUSMV_FUNCATTR_NORETURN;
01215 
01222 void
01223 ErrorMgr_error_file_clobbering (ErrorMgr_ptr self, const char* filename) NUSMV_FUNCATTR_NORETURN;
01224 
01231 void
01232 ErrorMgr_warning_processes_deprecated(ErrorMgr_ptr self);
01233 
01240 node_ptr
01241 ErrorMgr_failure_make(ErrorMgr_ptr self, const char* msg,
01242                       FailureKind kind, int lineno);
01243 
01251 const char*
01252 ErrorMgr_failure_get_msg(ErrorMgr_ptr self, node_ptr failure);
01253 
01261 FailureKind
01262 ErrorMgr_failure_get_kind(ErrorMgr_ptr self, node_ptr failure);
01263 
01270 int
01271 ErrorMgr_failure_get_lineno(ErrorMgr_ptr self, node_ptr failure);
01272 
01278 void ErrorMgr_enable_tag(ErrorMgr_ptr self, const char* tag);
01279 
01285 void ErrorMgr_disable_tag(ErrorMgr_ptr self, const char* tag);
01286 
01291 #endif /* __NUSMV_CORE_UTILS_ERROR_MGR_H__ */