FIxed some annotation

Hotmoka · Jan 7, 2025 · 95185a7 · 95185a7
1 parent 5298b89
commit 95185a7
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 3 deletions.
diff --git a/...on/internal/instrumentationsOfMethod/AddRuntimeChecksForWhiteListingProofObligations.java b/...on/internal/instrumentationsOfMethod/AddRuntimeChecksForWhiteListingProofObligations.java
@@ -23,6 +23,7 @@
 import java.lang.reflect.Method;
 import java.lang.reflect.Modifier;
 import java.util.ArrayList;
+import java.util.HashMap;
 import java.util.List;
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
@@ -49,6 +50,7 @@
 import org.apache.bcel.generic.InvokeInstruction;
 import org.apache.bcel.generic.LDC;
 import org.apache.bcel.generic.MethodGen;
+import org.apache.bcel.generic.NEW;
 import org.apache.bcel.generic.ObjectType;
 import org.apache.bcel.generic.ReferenceType;
 import org.apache.bcel.generic.Type;
@@ -58,6 +60,7 @@
 import io.hotmoka.instrumentation.internal.InstrumentedClassImpl.Builder.MethodLevelInstrumentation;
 import io.hotmoka.whitelisting.HasDeterministicTerminatingToString;
 import io.hotmoka.whitelisting.MustBeFalse;
+import io.hotmoka.whitelisting.MustBeSafeLibraryMap;
 import io.hotmoka.whitelisting.WhiteListingClassLoaders;
 import io.hotmoka.whitelisting.WhitelistingConstants;
 import io.hotmoka.whitelisting.api.WhiteListingProofObligation;
@@ -305,16 +308,29 @@ private boolean hasProofObligations(Executable method) {
 			Stream.of(method.getParameterAnnotations()).flatMap(Stream::of).map(Annotation::annotationType).anyMatch(annotation -> annotation.isAnnotationPresent(WhiteListingProofObligation.class));
 	}
 
+	private final static ObjectType HASH_MAP_OT = new ObjectType(HashMap.class.getName());
+
 	private boolean canBeStaticallyDicharged(Class<? extends Annotation> annotationType, InstructionHandle ih, int slots) {
 		// ih contains an InvokeInstruction distinct from INVOKEDYNAMIC
 		if (annotationType == MustBeFalse.class)
 			return pushers.getPushers(ih, slots, method.getInstructionList(), cpg)
 				.map(InstructionHandle::getInstruction)
 				.allMatch(ins -> ins instanceof ICONST iconst && iconst.getValue().equals(0));
+		/*else if (annotationType == MustBeSafeLibraryMap.class) {
+			pushers.getPushers(ih, slots, method.getInstructionList(), cpg)
+			.map(InstructionHandle::getInstruction).forEach(System.out::println);
+			return pushers.getPushers(ih, slots, method.getInstructionList(), cpg)
+				.map(InstructionHandle::getInstruction)
+				.allMatch(ins -> ins instanceof NEW _new && isSafeLibraryMap(_new.getType(cpg)));
+		}*/
 		else
 			return false;
 	}
 
+	private static boolean isSafeLibraryMap(Type type) {
+		return type.equals(HASH_MAP_OT);
+	}
+
 	private boolean isCallToConcatenationMetaFactory(INVOKEDYNAMIC invokedynamic) {
 		BootstrapMethod bootstrap = bootstraps.getBootstrapFor(invokedynamic);
 		Constant constant = cpg.getConstant(bootstrap.getBootstrapMethodRef());

diff --git a/...ting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryMapCheck.java b/...ting/src/main/java/io/hotmoka/whitelisting/internal/checks/MustBeSafeLibraryMapCheck.java
@@ -32,8 +32,7 @@ public boolean test(Object value, WhiteListingWizard wizard) {
 		return value == null || isSafeLibraryMap(value.getClass());
 	}
 
-	private static boolean isSafeLibraryMap(Class<?> clazz) {
-		System.out.println(clazz.getName());
+	public static boolean isSafeLibraryMap(Class<?> clazz) {
 		return clazz == HashMap.class;
 	}
 

diff --git a/...src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Character.java b/...src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Character.java
@@ -21,4 +21,5 @@ public interface Character {
 	boolean equals(java.lang.Object other);
 	int hashCode();
 	java.lang.String toString();
+	char charValue();
 }
diff --git a/...ting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Enum.java b/...ting/src/main/java/io/hotmoka/whitelisting/internal/database/version0/java/lang/Enum.java
@@ -18,7 +18,7 @@
 
 public abstract class Enum {
 	public Enum(java.lang.String name, int ordinal) {}
-	public abstract java.lang.Enum<?> valueOf(java.lang.Class<?> clazz, java.lang.String name);
+	//public abstract java.lang.Enum<?> valueOf(java.lang.Class<?> clazz, java.lang.String name);
 	public abstract int ordinal();
 	public abstract boolean equals(java.lang.Object other);
 	public abstract int hashCode();