diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 2348f7870..5ae7d0f51 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -17,8 +17,11 @@ IREP_ID_ONE(F) IREP_ID_ONE(E) IREP_ID_ONE(G) IREP_ID_ONE(X) -IREP_ID_ONE(smv_next) IREP_ID_ONE(smv_iff) +IREP_ID_ONE(smv_assign_current) +IREP_ID_ONE(smv_assign_init) +IREP_ID_ONE(smv_assign_next) +IREP_ID_ONE(smv_next) IREP_ID_TWO(C_smv_iff, "#smv_iff") IREP_ID_ONE(smv_setin) IREP_ID_ONE(smv_setnotin) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 982484b62..e7b7e558b 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -468,8 +468,8 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';' assignment_var: variable_name ; -assignment_head: init_Token { init($$, ID_init); } - | NEXT_Token { init($$, ID_smv_next); } +assignment_head: init_Token { init($$, ID_smv_assign_init); } + | NEXT_Token { init($$, ID_smv_assign_next); } ; defines: define diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h index fb3746aed..8fc4337bd 100644 --- a/src/smvlang/smv_parse_tree.h +++ b/src/smvlang/smv_parse_tree.h @@ -106,7 +106,7 @@ class smv_parse_treet } // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE - const equal_exprt &equal_expr() + equal_exprt &equal_expr() { PRECONDITION( is_assign_current() || is_assign_init() || is_assign_next() || @@ -223,7 +223,7 @@ class smv_parse_treet typedef std::unordered_map modulest; modulest modules; - + void swap(smv_parse_treet &smv_parse_tree); void clear(); }; diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index e1094b76a..3426154f9 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1162,46 +1162,60 @@ Function: smv_typecheckt::typecheck void smv_typecheckt::typecheck( smv_parse_treet::modulet::itemt &item) { - modet mode; - switch(item.item_type) { case smv_parse_treet::modulet::itemt::ASSIGN_CURRENT: - mode = OTHER; + { + auto &equal_expr = item.equal_expr(); + auto &symbol_expr = to_symbol_expr(equal_expr.lhs()); + auto &nil_type = static_cast(get_nil_irep()); + typecheck(symbol_expr, nil_type, OTHER); + typecheck(equal_expr.rhs(), symbol_expr.type(), OTHER); + } break; case smv_parse_treet::modulet::itemt::ASSIGN_INIT: - mode = INIT; + { + auto &equal_expr = item.equal_expr(); + auto &symbol_expr = to_symbol_expr(to_unary_expr(equal_expr.lhs()).op()); + auto &nil_type = static_cast(get_nil_irep()); + typecheck(symbol_expr, nil_type, OTHER); + typecheck(equal_expr.rhs(), symbol_expr.type(), INIT); + } break; case smv_parse_treet::modulet::itemt::ASSIGN_NEXT: - mode = TRANS; + { + auto &equal_expr = item.equal_expr(); + auto &symbol_expr = to_symbol_expr(to_unary_expr(equal_expr.lhs()).op()); + auto &nil_type = static_cast(get_nil_irep()); + typecheck(symbol_expr, nil_type, OTHER); + typecheck(equal_expr.rhs(), symbol_expr.type(), TRANS); + } break; case smv_parse_treet::modulet::itemt::INIT: - mode=INIT; + typecheck(item.expr, bool_typet(), INIT); break; case smv_parse_treet::modulet::itemt::TRANS: - mode=TRANS; + typecheck(item.expr, bool_typet(), TRANS); break; case smv_parse_treet::modulet::itemt::CTLSPEC: - mode = CTL; + typecheck(item.expr, bool_typet(), CTL); break; case smv_parse_treet::modulet::itemt::LTLSPEC: - mode = LTL; + typecheck(item.expr, bool_typet(), LTL); break; case smv_parse_treet::modulet::itemt::DEFINE: case smv_parse_treet::modulet::itemt::INVAR: case smv_parse_treet::modulet::itemt::FAIRNESS: default: - mode=OTHER; + typecheck(item.expr, bool_typet(), OTHER); } - - typecheck(item.expr, bool_typet(), mode); } /*******************************************************************\