From 4d806e44d042e838efc2570379fa69d64da4f81d Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 12 Oct 2016 16:45:54 +0100 Subject: [PATCH] array type mismatch bugfix --- src/goto-symex/goto_symex_state.cpp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 27a79bab974..8ffb413cf33 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -934,10 +934,20 @@ void goto_symex_statet::rename( { l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type)); - if(!l1_type_entry.second) + if(!l1_type_entry.second) // was already in map { - type=l1_type_entry.first->second; - return; + // do not change a complete array type to an incomplete one + + const typet &type_prev=l1_type_entry.first->second; + + if(type.id()!=ID_array || + type_prev.id()!=ID_array || + to_array_type(type).is_incomplete() || + to_array_type(type_prev).is_complete()) + { + type=l1_type_entry.first->second; + return; + } } }