Add test for ignored method annotation

Author: Owen Jones

jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.class

@@ -0,0 +1,8 @@
+package org.cprover;
+
+/**
+ * Ignored methods are documented above
+ * `java_bytecode_convert_classt::is_ignored_method`.
+ */
+public @interface IgnoredMethodImplementation {
+}

jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java

@@ -0,0 +1,12 @@
+import org.cprover.OverlayClassImplementation;
+import org.cprover.IgnoredMethodImplementation;
+
+@OverlayClassImplementation
+public class Test
+{
+  @IgnoredMethodImplementation
+  public static void main(String[] args)
+  {
+    assert(true);
+  }
+}

jbmc/regression/jbmc/overlay-class/ignored-method/Test.class

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--classpath `../../../../scripts/format_classpath.sh . annotations . ignored-method` --verbosity 10
+^Ignoring method:  'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Adding symbol from overlay class:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$