Use make_skip to turn an instruction into a SKIP

tautschnig · tautschnig · commit 9e355e9cc869 · 2018-06-04T11:09:47.000Z
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -1649,12 +1649,16 @@ void goto_checkt::goto_check(
       if((is_user_provided && !enable_assertions &&
           i.source_location.get_property_class()!="error label") ||
          (!is_user_provided && !enable_built_in_assertions))
-        i.type=SKIP;
+      {
+        i.make_skip();
+      }
     }
     else if(i.is_assume())
     {
       if(!enable_assumptions)
-        i.type=SKIP;
+      {
+        i.make_skip();
+      }
     }
     else if(i.is_dead())
     {
diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp
@@ -32,7 +32,7 @@ void set_properties(
       property_set.find(property_id);
 
     if(c_it==property_set.end())
-      it->type=SKIP;
+      it->make_skip();
     else
       property_set.erase(c_it);
   }

Original file line number	Diff line number	Diff line change
`@@ -1649,12 +1649,16 @@ void goto_checkt::goto_check(`
`1649`	`1649`	`if((is_user_provided && !enable_assertions &&`
`1650`	`1650`	`i.source_location.get_property_class()!="error label") \|\|`
`1651`	`1651`	`(!is_user_provided && !enable_built_in_assertions))`
`1652`		`- i.type=SKIP;`
	`1652`	`+ {`
	`1653`	`+ i.make_skip();`
	`1654`	`+ }`
`1653`	`1655`	`}`
`1654`	`1656`	`else if(i.is_assume())`
`1655`	`1657`	`{`
`1656`	`1658`	`if(!enable_assumptions)`
`1657`		`- i.type=SKIP;`
	`1659`	`+ {`
	`1660`	`+ i.make_skip();`
	`1661`	`+ }`
`1658`	`1662`	`}`
`1659`	`1663`	`else if(i.is_dead())`
`1660`	`1664`	`{`
Original file line number	Diff line number	Diff line change
`@@ -32,7 +32,7 @@ void set_properties(`
`32`	`32`	`property_set.find(property_id);`
`33`	`33`
`34`	`34`	`if(c_it==property_set.end())`
`35`		`- it->type=SKIP;`
	`35`	`+ it->make_skip();`
`36`	`36`	`else`
`37`	`37`	`property_set.erase(c_it);`
`38`	`38`	`}`