diff --git a/regression/smv/range-type/range_type9.desc b/regression/smv/range-type/range_type9.desc new file mode 100644 index 000000000..e650620d0 --- /dev/null +++ b/regression/smv/range-type/range_type9.desc @@ -0,0 +1,8 @@ +CORE +range_type9.smv + +^file .* line 5: Expected expression of type `1..6', but got expression `7', which is of type `7..7'$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/range-type/range_type9.smv b/regression/smv/range-type/range_type9.smv new file mode 100644 index 000000000..7abfacdc8 --- /dev/null +++ b/regression/smv/range-type/range_type9.smv @@ -0,0 +1,5 @@ +MODULE main +VAR x: 1..6; + +-- out of range +ASSIGN x := 7; diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 9c446d7ca..acb885a47 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1297,31 +1297,40 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type) } else if(type.id() == ID_range) { - if(expr.id() == ID_constant && expr.type().id() == ID_range) - { - // re-type the constant - auto value = numeric_cast_v(to_constant_expr(expr)); - expr = from_integer(value, type); - return; - } - else if(expr.id() == ID_cond && expr.type().id() == ID_range) + if(expr.type().id() == ID_range) { - // re-type the cond - bool condition = true; - - for(auto &op : expr.operands()) + // range to range + if(expr.id() == ID_constant) { - if(!condition) - convert_expr_to(op, type); + // re-type the constant + auto value = numeric_cast_v(to_constant_expr(expr)); + if(to_range_type(type).includes(value)) + { + expr = from_integer(value, type); + return; + } + } + else if(expr.id() == ID_cond) + { + // re-type the cond + bool condition = true; + + for(auto &op : expr.operands()) + { + if(!condition) + convert_expr_to(op, type); - condition = !condition; + condition = !condition; + } + expr.type() = type; + return; + } + else + { + expr = typecast_exprt{expr, type}; + return; } - expr.type() = type; - return; } - - expr = typecast_exprt{expr, type}; - return; } else if(type.id() == ID_bool) {