Fix #341: Add model classes for java.util.logging

- Created Logger, LogManager, and Level model classes
- Bypasses native method calls and complex JDK initialization
- Adds test case to verify Logger.getLogger() works in JPF

Author: HritikRaj2

src/classes/modules/java.logging/java/util/logging/FileHandler.java

@@ -6,13 +6,13 @@
  * The Java Pathfinder core (jpf-core) platform is licensed under the
  * Apache License, Version 2.0 (the "License"); you may not use this file except
  * in compliance with the License. You may obtain a copy of the License at
- * 
- *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ *        http://www.apache.org/licenses/LICENSE-2.0.
  *
  * Unless required by applicable law or agreed to in writing, software
  * distributed under the License is distributed on an "AS IS" BASIS,
  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and 
+ * See the License for the specific language governing permissions and
  * limitations under the License.
  */
 
@@ -25,12 +25,12 @@
  * simple stub to avoid execptions when using basic logging
  */
 public class FileHandler extends StreamHandler {
-  public FileHandler() throws IOException {
-    this("log.log");
-  }
+    public FileHandler() throws IOException {
+        this("log.log");
+    }
 
-  public FileHandler(String pattern) throws IOException {
-    super();
-    setOutputStream(new FileOutputStream(pattern));
-  }
-}
+    public FileHandler(String pattern) throws IOException {
+        super();
+        setOutputStream(new FileOutputStream(pattern));
+    }
+}

src/classes/modules/java.logging/java/util/logging/Level.java

@@ -0,0 +1,41 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ */
+package java.util.logging;
+
+/**
+ * MJI model class for java.util.logging.Level
+ */
+public class Level {
+  private final String name;
+  private final int value;
+
+  protected Level(String name, int value) {
+    this.name = name;
+    this.value = value;
+  }
+
+  public String getName() {
+    return name;
+  }
+
+  public final int intValue() {
+    return value;
+  }
+
+  public static final Level OFF = new Level("OFF", Integer.MAX_VALUE);
+  public static final Level SEVERE = new Level("SEVERE", 1000);
+  public static final Level WARNING = new Level("WARNING", 900);
+  public static final Level INFO = new Level("INFO", 800);
+  public static final Level CONFIG = new Level("CONFIG", 700);
+  public static final Level FINE = new Level("FINE", 500);
+  public static final Level FINER = new Level("FINER", 400);
+  public static final Level FINEST = new Level("FINEST", 300);
+  public static final Level ALL = new Level("ALL", Integer.MIN_VALUE);
+
+  public String toString() {
+    return name;
+  }
+}

src/classes/modules/java.logging/java/util/logging/LogManager.java

@@ -0,0 +1,48 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ */
+package java.util.logging;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * MJI model class for java.util.logging.LogManager
+ */
+public class LogManager {
+  
+  private static final LogManager manager = new LogManager();
+  private final Map<String, Logger> loggers = new HashMap<>();
+  
+  protected LogManager() {
+  }
+  
+  public static LogManager getLogManager() {
+    return manager;
+  }
+  
+  public synchronized Logger getLogger(String name) {
+    return loggers.get(name);
+  }
+  
+  public synchronized boolean addLogger(Logger logger) {
+    String name = logger.getName();
+    if (loggers.containsKey(name)) {
+      return false;
+    }
+    loggers.put(name, logger);
+    return true;
+  }
+  
+  Logger demandLogger(String name, String resourceBundleName, Class<?> caller) {
+    Logger result = getLogger(name);
+    if (result == null) {
+      Logger newLogger = new Logger(name, resourceBundleName);
+      addLogger(newLogger);
+      result = newLogger;
+    }
+    return result;
+  }
+}

src/classes/modules/java.logging/java/util/logging/Logger.java

@@ -0,0 +1,77 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ */
+package java.util.logging;
+
+/**
+ * MJI model class for java.util.logging.Logger
+ */
+public class Logger {
+
+  private String name;
+  private String resourceBundleName;
+
+  protected Logger(String name, String resourceBundleName) {
+    this.name = name;
+    this.resourceBundleName = resourceBundleName;
+  }
+
+  public static Logger getLogger(String name) {
+    return getLogger(name, null);
+  }
+  
+  public static Logger getLogger(String name, String resourceBundleName) {
+    LogManager manager = LogManager.getLogManager();
+    return manager.demandLogger(name, resourceBundleName, null);
+  }
+
+  public static Logger getAnonymousLogger() {
+    return new Logger("", null);
+  }
+  
+  public static Logger getAnonymousLogger(String resourceBundleName) {
+    return new Logger("", resourceBundleName);
+  }
+
+  public String getName() {
+    return name;
+  }
+  
+  public String getResourceBundleName() {
+    return resourceBundleName;
+  }
+
+  public void info(String msg) {
+    log(Level.INFO, msg);
+  }
+
+  public void warning(String msg) {
+    log(Level.WARNING, msg);
+  }
+  
+  public void severe(String msg) {
+    log(Level.SEVERE, msg);
+  }
+  
+  public void config(String msg) {
+    log(Level.CONFIG, msg);
+  }
+  
+  public void fine(String msg) {
+    log(Level.FINE, msg);
+  }
+  
+  public void finer(String msg) {
+    log(Level.FINER, msg);
+  }
+  
+  public void finest(String msg) {
+    log(Level.FINEST, msg);
+  }
+  
+  public void log(Level level, String msg) {
+    System.out.println("[" + level.getName() + "] " + name + ": " + msg);
+  }
+}

src/tests/gov/nasa/jpf/test/java/util/LoggerTest.java

@@ -0,0 +1,18 @@
+package gov.nasa.jpf.test.java.util;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+import java.util.logging.Logger;
+
+public class LoggerTest extends TestJPF {
+
+    @Test
+    public void testGetLogger() {
+        if (verifyNoPropertyViolation()) {
+            System.out.println("--- calling getLogger");
+            Logger log = Logger.getLogger("testLogger");
+            assertNotNull(log);
+            System.out.println("--- success: " + log.getName());
+        }
+    }
+}