From 8d8c2e0ca010117a018943fb2dc76cbfb1352011 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 1 Mar 2018 10:25:44 +0000 Subject: [PATCH] Fix bug causing crash on Windows A reference was being kept to a field of an element of a vector that had been swapped with another vector. Whether the original element still exists at the original memory location, preserving references, is implementation dependant and should not be relied upon. --- src/ansi-c/c_typecheck_expr.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 12f324d0c86..b49ccb2289d 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1244,7 +1244,10 @@ void c_typecheck_baset::typecheck_expr_index(exprt &expr) make_index_type(index_expr); - const typet &final_array_type=follow(array_expr.type()); + // array_expr is a reference to one of expr.operands(), when that vector is + // swapped below the reference is no longer valid. final_array_type exists + // beyond that point so can't be a reference + const typet final_array_type = follow(array_expr.type()); if(final_array_type.id()==ID_array || final_array_type.id()==ID_vector)