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

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

@@ -0,0 +1,9 @@
+/*
+ * 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;
+public abstract class Formatter {
+  public abstract String format(LogRecord record);
+}

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

@@ -0,0 +1,20 @@
+/*
+ * 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.io.IOException;
+
+/**
+ * MJI model class for java.util.logging.Handler.
+ */
+public abstract class Handler {
+  public abstract void publish(LogRecord record);
+
+  // Mentor requested 'throws IOException'
+  public abstract void flush() throws IOException;
+
+  public abstract void close();
+}

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

@@ -0,0 +1,35 @@
+/*
+ * 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,40 @@
+/*
+ * 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/LogRecord.java

@@ -0,0 +1,23 @@
+/*
+ * 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.LogRecord.
+ */
+public class LogRecord {
+  private Level level;
+  private String message;
+  public LogRecord(Level level, String msg) {
+    this.level = level;
+    this.message = msg;
+  }
+  public Level getLevel() {
+    return level;
+  }
+  public String getMessage() {
+    return message;
+  }
+}

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

@@ -0,0 +1,73 @@
+/*
+ * 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;
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * MJI model class for java.util.logging.Logger
+ */
+public class Logger {
+
+  private static final Map<String, Logger> loggers = new HashMap<>();
+  private String name;
+  private final List<Handler> handlers = new ArrayList<>();
+
+  protected Logger(String name, String resourceBundleName) {
+    this.name = name;
+  }
+
+  public static synchronized Logger getLogger(String name) {
+    Logger logger = loggers.get(name);
+    if (logger == null) {
+      logger = new Logger(name, null);
+      loggers.put(name, logger);
+    }
+    return logger;
+  }
+
+  public static Logger getAnonymousLogger() {
+    return new Logger("", null);
+  }
+
+  public String getName() {
+    return name;
+  }
+
+  public void addHandler(Handler handler) {
+    handlers.add(handler);
+  }
+
+  public void removeHandler(Handler handler) {
+    handlers.remove(handler);
+  }
+
+  public Handler[] getHandlers() {
+    return handlers.toArray(new Handler[0]);
+  }
+
+  public void log(Level level, String msg) {
+    LogRecord record = new LogRecord(level, msg);
+    for (Handler h : handlers) {
+      h.publish(record);
+    }
+  }
+
+  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);
+  }
+}

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

@@ -0,0 +1,62 @@
+/*
+ * 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.io.OutputStream;
+import java.io.IOException;
+
+/**
+ * MJI model class for java.util.logging.StreamHandler.
+ */
+public class StreamHandler extends Handler {
+  private OutputStream out;
+
+  public StreamHandler() {
+    this.out = System.out;
+  }
+
+  public StreamHandler(OutputStream out, Formatter formatter) {
+    this.out = out;
+  }
+
+  protected void setOutputStream(OutputStream out) {
+    this.out = out;
+  }
+
+  @Override
+  public void publish(LogRecord record) {
+    if (out == null) return;
+    try {
+      String msg;
+      if (record.getLevel() != null) {
+          msg = "[" + record.getLevel().getName() + "] " + record.getMessage() + "\n";
+      } else {
+          msg = "[UNKNOWN] " + record.getMessage() + "\n";
+      }
+      out.write(msg.getBytes());
+      flush();
+    } catch (IOException e) {
+      e.printStackTrace();
+    }
+  }
+
+  @Override
+  public void flush() throws IOException {
+    if (out != null) {
+      out.flush();
+    }
+  }
+
+  @Override
+  public void close() {
+    try {
+      flush();
+    } catch (IOException e) {
+      e.printStackTrace();
+    }
+    out = null;
+  }
+}

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

@@ -0,0 +1,38 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ */
+package gov.nasa.jpf.test.java.util;
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+import java.util.logging.Logger;
+import java.util.logging.Level;
+import java.util.logging.StreamHandler;
+import java.io.ByteArrayOutputStream;
+public class LoggerTest extends TestJPF {
+  @Test
+  public void testGetLogger() {
+    if (verifyNoPropertyViolation()) {
+      Logger log = Logger.getLogger("testLogger");
+      assertEquals("testLogger", log.getName());
+      Logger log2 = Logger.getLogger("testLogger");
+      assertTrue(log == log2);
+    }
+  }
+  @Test
+  public void testLogOutput() {
+    if (verifyNoPropertyViolation()) {
+      Logger log = Logger.getLogger("captureLogger");
+      ByteArrayOutputStream baos = new ByteArrayOutputStream();
+      StreamHandler handler = new StreamHandler(baos, null);
+      log.addHandler(handler);
+      String message = "This is a test warning";
+      log.warning(message);
+      handler.flush();
+      String output = baos.toString();
+      assertTrue(output.contains("WARNING"));
+      assertTrue(output.contains(message));
+    }
+  }
+}