Updates requested in the PR:

- rename uncasted_access_path -> uncast_access_path
- improved comments and error message.
- typos

Author: marek-trtik

src/taint-slicer/instrumenter.cpp

@@ -392,20 +392,20 @@ exprt taint_instrumentert::drive_access_path_through_super_classes(
     // data types. We resolve the typecast so that we build the struct
     // initialiser for the wrapper type and we initialise all members by making
     // accesses to the corresponding members in the origin wrapped access path.
-    exprt uncasted_access_path = access_path;
-    while(uncasted_access_path.id() == ID_typecast)
-      uncasted_access_path = to_typecast_expr(uncasted_access_path).op();
-    uncasted_access_path =
-      drive_access_path_through_super_classes(uncasted_access_path);
+    exprt uncast_access_path = access_path;
+    while(uncast_access_path.id() == ID_typecast)
+      uncast_access_path = to_typecast_expr(uncast_access_path).op();
+    uncast_access_path =
+      drive_access_path_through_super_classes(uncast_access_path);
     const typet uncasted_access_path_type =
-      instrumented_namespace.follow(uncasted_access_path.type());
+      instrumented_namespace.follow(uncast_access_path.type());
     struct_exprt struct_expr(fixed_type);
     // First we set the super instance (i.e. '@__CPROVER__super' member,
     // which is actually the instance of the primitive type).
     struct_expr.operands().push_back(
       typecast_exprt(
         get_super_if_subclassed(
-          uncasted_access_path,
+          uncast_access_path,
           get_inverse_type_substitutions(),
           get_instrumented_symbol_table()),
         access_path.type()));
@@ -427,7 +427,7 @@ exprt taint_instrumentert::drive_access_path_through_super_classes(
           )
         {
           struct_expr.operands().push_back(member_exprt(
-            uncasted_access_path, component.get_name(), bool_typet()));
+            uncast_access_path, component.get_name(), bool_typet()));
         }
         else
         {
@@ -587,9 +587,10 @@ void taint_instrumentert::instrument_instructions_with_shadow_variables(
 
           // There is a possibility, that asgn.lhs().type()!=asgn.rhs().type().
           // This may occur only when asgn.rhs().type() is a wrapper of
-          // a primitive data type and asgn.lhs() accesses the wrapped data.
+          // a primitive data type and asgn.lhs() is an unwrapped primitive
+          // (e.g. array length) that cannot carry taint.
           // The code below resolves the inconsistency, by applying member
-          // access to the super filed of the asgn.rhs() until we get to
+          // access to the super field of the asgn.rhs() until we get to
           // the right one.
 
           const auto &lhs_type =
@@ -613,8 +614,8 @@ void taint_instrumentert::instrument_instructions_with_shadow_variables(
             const auto &struct_type = to_struct_type(rhs_type);
             INVARIANT(
               struct_type.has_component(taint_name_of_super_variable()),
-              "The type difference could occur only for wrapped primitives, "
-                "so the struct must contain the super variable.");
+              "Assignment has type mismatch that couldn't be resolved by "
+              "unwrapping the rhs.");
             asgn.rhs() = member_exprt(
               asgn.rhs(),
               struct_type.get_component(taint_name_of_super_variable()));