Rename getCurrentThreadID to getCurrentThreadId

to comply with Google Java coding guidelines.

Author: peterschrammel

jbmc/regression/jbmc-concurrency/get-current-thread/A.class

@@ -8,7 +8,7 @@ public class A
   // expected verification success
   public void me()
   {
-    int g = CProver.getCurrentThreadID();
+    int g = CProver.getCurrentThreadId();
     assert(g == 0);
   }
 
@@ -40,7 +40,7 @@ public void me_bug()
   public void me2()
   {
     CProver.startThread(333);
-    g = CProver.getCurrentThreadID();
+    g = CProver.getCurrentThreadId();
     assert(g == 1);
     CProver.endThread(333);
   }
@@ -51,7 +51,7 @@ public void me2()
   public void me3()
   {
     CProver.startThread(333);
-    int i = CProver.getCurrentThreadID();
+    int i = CProver.getCurrentThreadId();
     assert(g == 1);
     CProver.endThread(333);
   }
@@ -83,7 +83,7 @@ public void me6()
 
   public void check()
   {
-    g = CProver.getCurrentThreadID();
+    g = CProver.getCurrentThreadId();
     assert(g == 1);
   }
 }
@@ -94,7 +94,7 @@ class B implements Runnable
   @Override
   public void run()
   {
-    g = CProver.getCurrentThreadID();
+    g = CProver.getCurrentThreadId();
     assert(g == 1);
   }
 }
@@ -106,7 +106,7 @@ class C extends Thread
   @Override
   public void run()
   {
-    g = CProver.getCurrentThreadID();
+    g = CProver.getCurrentThreadId();
     assert(g == 1);
   }
 }

jbmc/regression/jbmc-concurrency/get-current-thread/A.java

@@ -201,11 +201,11 @@ calls to the these functions are well-formed, more specifically, each call to
 
 The instrumentation process (described here) will transform the aforementioned
 function calls, synchronized blocks/methods and calls to
-`java.lang.Thread.getCurrentThreadID:()I` into appropriate codet. As part of
+`java.lang.Thread.getCurrentThreadId:()I` into appropriate codet. As part of
 this process a new variable per thread  is created  along with a single global
 variable that is used keep track of thread identifiers. These
 variables are needed to handle calls to
-`java.lang.Thread.getCurrentThreadID:()I`.
+`java.lang.Thread.getCurrentThreadId:()I`.
 
 Hold on, how do we go from Java threads to `CProver.startThread:(I)V` and
 `CProver.endThread:(I)V`? Well, two ways
@@ -264,13 +264,13 @@ is transformed into the following codet:
 ```
 
 The ID of the thread is made accessible to the Java program by having calls
-to the function `CProver.getCurrentThreadID()I` replaced by the variable
+to the function `CProver.getCurrentThreadId()I` replaced by the variable
 `__CPROVER__thread_id`.
 
 Example, the following Java code:
 
 ```java
-  int g = java.lang.thead.getCurrentThreadID();
+  int g = java.lang.thead.getCurrentThreadId();
 ```
 
 is transformed into the following codet:

jbmc/regression/jbmc-concurrency/get-current-thread/B.class

@@ -362,12 +362,12 @@ static void instrument_end_thread(
 }
 
 /// Transforms the codet stored in in \p f_code, which is a call to function
-/// CProver.getCurrentThreadID:()I into a code_assignt as described by the
+/// CProver.getCurrentThreadId:()I into a code_assignt as described by the
 /// documentation of the function convert_thread_block.
 ///
 /// The resulting code_blockt is stored in the output parameter \p code.
 ///
-/// \param f_code: function call to CProver.getCurrentThreadID:()I
+/// \param f_code: function call to CProver.getCurrentThreadId:()I
 /// \param [out] code: resulting transformation
 /// \param symbol_table: a symbol table
 static void instrument_get_current_thread_id(
@@ -409,10 +409,10 @@ static void instrument_get_current_thread_id(
 /// variable __CPROVER__next_thread_id.
 ///
 /// The ID of the thread is made accessible to the Java program by having calls
-/// to the function 'CProver.getCurrentThreadID()I' replaced by the variable
+/// to the function 'CProver.getCurrentThreadId()I' replaced by the variable
 /// __CPROVER__thread_id. We also perform this substitution in here. The
 /// substitution that we perform here assumes that calls to
-/// getCurrentThreadID() are ONLY made in the RHS of an expression.
+/// getCurrentThreadId() are ONLY made in the RHS of an expression.
 ///
 /// Example:
 ///
@@ -495,7 +495,7 @@ void convert_threadblock(symbol_tablet &symbol_table)
           std::placeholders::_1,
           std::placeholders::_2,
           std::placeholders::_3);
-      else if(f_name == "org.cprover.CProver.getCurrentThreadID:()I")
+      else if(f_name == "org.cprover.CProver.getCurrentThreadId:()I")
         cb = std::bind(
           &instrument_get_current_thread_id,
           std::placeholders::_1,

jbmc/regression/jbmc-concurrency/get-current-thread/C.class

@@ -529,8 +529,7 @@ bool is_non_null_library_global(const irep_idt &symbolid)
 
 /// Methods belonging to the class org.cprover.CProver that should be ignored
 /// (not converted), leaving the driver program to stub them if it wishes.
-const std::unordered_set<std::string> cprover_methods_to_ignore
-{
+const std::unordered_set<std::string> cprover_methods_to_ignore{
   "nondetBoolean",
   "nondetByte",
   "nondetChar",
@@ -546,8 +545,7 @@ const std::unordered_set<std::string> cprover_methods_to_ignore
   "atomicEnd",
   "startThread",
   "endThread",
-  "getCurrentThreadID"
-};
+  "getCurrentThreadId"};
 
 /// \param type: type of new symbol
 /// \param basename_prefix: new symbol will be named