Add length assumption at assign_string_constant beginning

This is to make sure that the length of the array before the assignment
isn't unconstrained. Otherwise it could be set to be arbitrarily large
by the solver which will causes invalid traces.

Author: romainbrenguier

src/goto-symex/goto_symex.cpp

@@ -199,6 +199,11 @@ void goto_symext::assign_string_constant(
   const ssa_exprt &char_array,
   const array_exprt &new_char_array)
 {
+  // We need to make sure that the length of the previous array isn't
+  // unconstrained, otherwise it could be arbitrarily large which causes
+  // invalid traces
+  symex_assume(state, equal_exprt{length, from_integer(0, length.type())});
+
   // assign length of string
   symex_assign.assign_symbol(length, expr_skeletont{}, new_length, {});
 

src/goto-symex/goto_symex.h

@@ -590,6 +590,9 @@ class goto_symext
   /// "abc", the symbol will be named "abc_constant_char_array"). Then, the
   /// expression `&sym[0]` is assigned to `char_array` (assuming `sym` denotes
   /// the symbol holding the string data given by `new_char_array`.
+  /// The assignment is preceeded by a assume statements ensuring `length`
+  /// before this call was zero, this is to avoid letting the previous array
+  /// unconstrained.
   ///
   /// \param state: goto symex state
   /// \param symex_assign: object handling symbol assignments