Merge pull request #4639 from owen-jones-diffblue/irep_id_set_may_etc

smowton · web-flow · commit 6364659a7572 · 2019-05-09T21:26:25.000+01:00
Turn get_may, set_may, etc into irep_ids
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
@@ -450,10 +450,9 @@ void custom_bitvector_domaint::transform(
       const auto &code = instruction.get_other();
       const irep_idt &statement = code.get_statement();
 
-      if(statement=="set_may" ||
-         statement=="set_must" ||
-         statement=="clear_may" ||
-         statement=="clear_must")
+      if(
+        statement == ID_set_may || statement == ID_set_must ||
+        statement == ID_clear_may || statement == ID_clear_must)
       {
         DATA_INVARIANT(
           code.operands().size() == 2, "set/clear_may/must has two operands");
@@ -463,13 +462,13 @@ void custom_bitvector_domaint::transform(
         // initialize to make Visual Studio happy
         modet mode = modet::SET_MUST;
 
-        if(statement=="set_must")
+        if(statement == ID_set_must)
           mode=modet::SET_MUST;
-        else if(statement=="clear_must")
+        else if(statement == ID_clear_must)
           mode=modet::CLEAR_MUST;
-        else if(statement=="set_may")
+        else if(statement == ID_set_may)
           mode=modet::SET_MAY;
-        else if(statement=="clear_may")
+        else if(statement == ID_clear_may)
           mode=modet::CLEAR_MAY;
         else
           UNREACHABLE;
@@ -687,8 +686,7 @@ void custom_bitvector_domaint::erase_blank_vectors(bitst &bits)
 
 bool custom_bitvector_domaint::has_get_must_or_may(const exprt &src)
 {
-  if(src.id()=="get_must" ||
-     src.id()=="get_may")
+  if(src.id() == ID_get_must || src.id() == ID_get_may)
     return true;
 
   forall_operands(it, src)
@@ -702,7 +700,7 @@ exprt custom_bitvector_domaint::eval(
   const exprt &src,
   custom_bitvector_analysist &custom_bitvector_analysis) const
 {
-  if(src.id()=="get_must" || src.id()=="get_may")
+  if(src.id() == ID_get_must || src.id() == ID_get_may)
   {
     if(src.operands().size()==2)
     {
@@ -717,15 +715,15 @@ exprt custom_bitvector_domaint::eval(
       if(pointer.is_constant() &&
          to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all
       {
-        if(src.id()=="get_may")
+        if(src.id() == ID_get_may)
         {
           for(const auto &bit : may_bits)
             if(get_bit(bit.second, bit_nr))
               return true_exprt();
 
           return false_exprt();
         }
-        else if(src.id()=="get_must")
+        else if(src.id() == ID_get_must)
         {
           return false_exprt();
         }
@@ -739,9 +737,9 @@ exprt custom_bitvector_domaint::eval(
 
         bool value=false;
 
-        if(src.id()=="get_must")
+        if(src.id() == ID_get_must)
           value=get_bit(v.must_bits, bit_nr);
-        else if(src.id()=="get_may")
+        else if(src.id() == ID_get_may)
           value=get_bit(v.may_bits, bit_nr);
 
         if(value)
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -2074,7 +2074,7 @@ exprt c_typecheck_baset::do_special_functions(
     typecheck_function_call_arguments(expr);
 
     binary_predicate_exprt get_must_expr(
-      expr.arguments()[0], "get_must", expr.arguments()[1]);
+      expr.arguments()[0], ID_get_must, expr.arguments()[1]);
     get_must_expr.add_source_location()=source_location;
 
     return std::move(get_must_expr);
@@ -2091,7 +2091,7 @@ exprt c_typecheck_baset::do_special_functions(
     typecheck_function_call_arguments(expr);
 
     binary_predicate_exprt get_may_expr(
-      expr.arguments()[0], "get_may", expr.arguments()[1]);
+      expr.arguments()[0], ID_get_may, expr.arguments()[1]);
     get_may_expr.add_source_location()=source_location;
 
     return std::move(get_may_expr);
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -2911,8 +2911,7 @@ std::string expr2ct::convert_code(
   if(statement==ID_array_replace)
     return convert_code_array_replace(src, indent);
 
-  if(statement=="set_may" ||
-     statement=="set_must")
+  if(statement == ID_set_may || statement == ID_set_must)
     return indent_str(indent) + convert_function(src, id2string(statement)) +
            ";";
 
@@ -3451,10 +3450,10 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_pointer_object)
     return convert_function(src, "POINTER_OBJECT");
 
-  else if(src.id()=="get_must")
+  else if(src.id() == ID_get_must)
     return convert_function(src, CPROVER_PREFIX "get_must");
 
-  else if(src.id()=="get_may")
+  else if(src.id() == ID_get_may)
     return convert_function(src, CPROVER_PREFIX "get_may");
 
   else if(src.id()=="object_value")
diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
@@ -162,7 +162,7 @@ void taint_analysist::instrument(
             {
             case taint_parse_treet::rulet::SOURCE:
             {
-              codet code_set_may("set_may");
+              codet code_set_may{ID_set_may};
               code_set_may.operands().resize(2);
               code_set_may.op0() = where;
               code_set_may.op1() =
@@ -174,10 +174,10 @@ void taint_analysist::instrument(
 
             case taint_parse_treet::rulet::SINK:
             {
-              binary_predicate_exprt get_may(
+              binary_predicate_exprt get_may{
                 where,
-                "get_may",
-                address_of_exprt(string_constantt(rule.taint)));
+                ID_get_may,
+                address_of_exprt(string_constantt(rule.taint))};
               goto_programt::targett t =
                 insert_before.add(goto_programt::make_assertion(
                   not_exprt(get_may), instruction.source_location));
@@ -189,7 +189,7 @@ void taint_analysist::instrument(
 
             case taint_parse_treet::rulet::SANITIZER:
             {
-              codet code_clear_may("clear_may");
+              codet code_clear_may{ID_clear_may};
               code_clear_may.operands().resize(2);
               code_clear_may.op0() = where;
               code_clear_may.op1() =
diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp
@@ -41,10 +41,10 @@ void thread_exit_instrumentation(goto_programt &goto_program)
   const string_constantt mutex_locked_string("mutex-locked");
 
   // NULL is any
-  binary_predicate_exprt get_may(
+  binary_predicate_exprt get_may{
     null_pointer_exprt(pointer_type(empty_typet())),
-    "get_may",
-    address_of_exprt(mutex_locked_string));
+    ID_get_may,
+    address_of_exprt(mutex_locked_string)};
 
   *end = goto_programt::make_assertion(not_exprt(get_may), source_location);
 
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
@@ -722,6 +722,12 @@ IREP_ID_ONE(to_member)
 IREP_ID_ONE(pointer_to_member)
 IREP_ID_ONE(tuple)
 IREP_ID_ONE(function_body)
+IREP_ID_ONE(get_may)
+IREP_ID_ONE(set_may)
+IREP_ID_ONE(clear_may)
+IREP_ID_ONE(get_must)
+IREP_ID_ONE(set_must)
+IREP_ID_ONE(clear_must)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree
