Fix use of old flag name

External_value_set_exprt used to have a "modified" flag, but it was
renamed to "initializer" (and its sense was inverted). This use of it
was missed because it accessed the underlying irep directly rather than
using a method of external_value_set_exprt itself.

After some discussion, we think that this flag is probably ignored when
this object is passed back to LVSA anyway, so the only purpose of
removing it is so that two EVSs which only differ by this flag are
considered the same.

This PR changes it so that instead of both being set as "not modified"
they are both set as "non_initializers", i.e. as "modified". I chose
this because if there ever is a difference in the way that LVSA treats
them the "initializer" EVS would return fewer values and so might be
unsound.

Author: Owen Jones

src/taint-analysis/taint_summary.cpp

@@ -127,8 +127,7 @@ static exprt transform_external_objects(const exprt& e)
     evs_copy.extend_access_path(new_entry, external_value_set_typet::PER_FIELD);
     evs_copy.label()=constant_exprt("external_objects",string_typet());
     evs_copy.type()=e.type();
-    evs_copy.remove("modified");
-    return evs_copy;
+    return evs_copy.as_non_initializer();
   }
   else if(e.id()==ID_external_value_set)
   {
@@ -139,8 +138,7 @@ static exprt transform_external_objects(const exprt& e)
     evs_copy.extend_access_path(new_entry, external_value_set_typet::PER_FIELD);
     evs_copy.label()=constant_exprt("external_objects",string_typet());
     evs_copy.type()=e.type();
-    evs_copy.remove("modified");
-    return evs_copy;
+    return evs_copy.as_non_initializer();
   }
   else
     return e;