Validate renamings before inserting in value set

I noticed writting unit tests, that the argument of this function should
have been renamed to level 1 to get the expected result.
It took some time to realize that fact by debugging and having a check
early would have made it much faster.

Author: romainbrenguier

src/pointer-analysis/value_set.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 #include <util/range.h>
+#include <goto-symex/renamed.h>
 
 #ifdef DEBUG
 #include <iostream>
@@ -1220,7 +1221,8 @@ void value_sett::assign(
   std::cout << "--------------------------------------------\n";
   output(ns, std::cout);
 #endif
-
+  PRECONDITION(is_l1_renamed(lhs));
+  PRECONDITION(is_l1_renamed(rhs));
   const typet &type=ns.follow(lhs.type());
 
   if(type.id()==ID_struct ||

src/pointer-analysis/value_set.h

@@ -374,8 +374,8 @@ class value_sett
 
   /// Transforms this value-set by executing executing the assignment
   /// `lhs := rhs` against it.
-  /// \param lhs: written expression
-  /// \param rhs: read expression
+  /// \param lhs: written expression, renamed to level 1
+  /// \param rhs: read expression, renamed to level 1
   /// \param ns: global namespace
   /// \param is_simplified: if false, `simplify` will be used to simplify
   ///   RHS and LHS before execution. If you know they are already simplified,