java.lang
Class SecurityManager

java.lang.Object
  java.lang.SecurityManager

public class SecurityManager

extends Object

JML's specification of java.lang.SecurityManager

Version:

$Revision: 1.4 $

Author:

Gary T. Leavens and Tabitha Johnson

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
protected  boolean	inCheck           Deprecated.

 

Constructor Summary

SecurityManager()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	checkAccept(String host, int port)
void	checkAccess(Thread t)
void	checkAccess(ThreadGroup g)
void	checkAwtEventQueueAccess()
void	checkConnect(String host, int port)
void	checkConnect(String host, int port, Object context)
void	checkCreateClassLoader()
void	checkDelete(String file)
void	checkExec(String cmd)
void	checkExit(int status)
void	checkLink(String lib)
void	checkListen(int port)
void	checkMemberAccess(Class clazz, int which)
void	checkMulticast(InetAddress maddr)
void	checkMulticast(InetAddress maddr, byte ttl)           Deprecated.
void	checkPackageAccess(String pkg)
void	checkPackageDefinition(String pkg)
void	checkPermission(Permission perm)
void	checkPermission(Permission perm, nullable Object context)
void	checkPrintJobAccess()
void	checkPropertiesAccess()
void	checkPropertyAccess(String key)
void	checkRead(FileDescriptor fd)
void	checkRead(String file)
void	checkRead(String file, Object context)
void	checkSecurityAccess(String target)
void	checkSetFactory()
void	checkSystemClipboardAccess()
boolean	checkTopLevelWindow(Object window)
void	checkWrite(FileDescriptor fd)
void	checkWrite(String file)
protected  int	classDepth(String name)           Deprecated.
protected  int	classLoaderDepth()           Deprecated.
protected  ClassLoader	currentClassLoader()           Deprecated.
protected  Class	currentLoadedClass()           Deprecated.
protected  Class[]	getClassContext()
boolean	getInCheck()           Deprecated.
Object	getSecurityContext()
ThreadGroup	getThreadGroup()
protected  boolean	inClass(String name)           Deprecated.
protected  boolean	inClassLoader()           Deprecated.

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

inCheck

protected boolean inCheck

Deprecated.  

SecurityManager

public SecurityManager()

Specifications:

signals_only java.lang.SecurityException;

getInCheck

public boolean getInCheck()

Deprecated.  

getClassContext

protected Class[] getClassContext()

Specifications:

ensures \nonnullelements(\result );

currentClassLoader

protected ClassLoader currentClassLoader()

Deprecated.  

currentLoadedClass

protected Class currentLoadedClass()

Deprecated.  

classDepth

protected int classDepth(String name)

Deprecated.  

classLoaderDepth

protected int classLoaderDepth()

Deprecated.  

inClass

protected boolean inClass(String name)

Deprecated.  

inClassLoader

protected boolean inClassLoader()

Deprecated.  

getSecurityContext

public Object getSecurityContext()

Specifications:

ensures_redundantly \result != null;

checkPermission

public void checkPermission(Permission perm)

Specifications: pure

requires_redundantly perm != null;
signals_only java.lang.SecurityException;

checkPermission

public void checkPermission(Permission perm,
                            nullable Object context)

Specifications: pure

requires context instanceof java.security.AccessControlContext;
requires_redundantly perm != null;
signals_only java.security.AccessControlException;

     also

requires !(context instanceof java.security.AccessControlContext);
signals_only java.lang.SecurityException;

    implies_that

requires context == null;
signals_only java.lang.SecurityException;

checkCreateClassLoader

public void checkCreateClassLoader()

Specifications: pure

signals_only java.lang.SecurityException;

checkAccess

public void checkAccess(Thread t)

Specifications: pure

requires_redundantly t != null;
signals_only java.lang.SecurityException;

checkAccess

public void checkAccess(ThreadGroup g)

Specifications: pure

requires_redundantly g != null;
signals_only java.lang.SecurityException;

checkExit

public void checkExit(int status)

Specifications: pure

signals_only java.lang.SecurityException;

checkExec

public void checkExec(String cmd)

Specifications: pure

requires_redundantly cmd != null;
signals_only java.lang.SecurityException;

checkLink

public void checkLink(String lib)

Specifications: pure

requires_redundantly lib != null;
signals_only java.lang.SecurityException;

checkRead

public void checkRead(FileDescriptor fd)

Specifications: pure

requires_redundantly fd != null;
signals_only java.lang.SecurityException;

checkRead

public void checkRead(String file)

Specifications: pure

requires_redundantly file != null;
signals_only java.lang.SecurityException;

checkRead

public void checkRead(String file,
                      Object context)

Specifications: pure

requires context instanceof java.security.AccessControlContext;
requires_redundantly file != null;
signals_only java.security.AccessControlException;

     also

requires !(context instanceof java.security.AccessControlContext);
signals_only java.lang.SecurityException;

    implies_that

requires context == null;
signals_only java.lang.SecurityException;

checkWrite

public void checkWrite(FileDescriptor fd)

Specifications: pure

requires_redundantly fd != null;
signals_only java.lang.SecurityException;

checkWrite

public void checkWrite(String file)

Specifications: pure

requires_redundantly file != null;
signals_only java.lang.SecurityException;

checkDelete

public void checkDelete(String file)

Specifications: pure

requires_redundantly file != null;
signals_only java.lang.SecurityException;

checkConnect

public void checkConnect(String host,
                         int port)

Specifications: pure

requires_redundantly host != null;
signals_only java.lang.SecurityException;

checkConnect

public void checkConnect(String host,
                         int port,
                         Object context)

Specifications: pure

requires context instanceof java.security.AccessControlContext;
requires_redundantly host != null;
signals_only java.security.AccessControlException;

     also

requires !(context instanceof java.security.AccessControlContext);
signals_only java.lang.SecurityException;

    implies_that

requires context == null;
signals_only java.lang.SecurityException;

checkListen

public void checkListen(int port)

Specifications: pure

signals_only java.lang.SecurityException;

checkAccept

public void checkAccept(String host,
                        int port)

Specifications: pure

requires_redundantly host != null;
signals_only java.lang.SecurityException;

checkMulticast

public void checkMulticast(InetAddress maddr)

Specifications: pure

requires_redundantly maddr != null;
signals_only java.lang.SecurityException;

checkMulticast

public void checkMulticast(InetAddress maddr,
                           byte ttl)

Deprecated.  

Specifications: pure

requires_redundantly maddr != null;
signals_only java.lang.SecurityException;

checkPropertiesAccess

public void checkPropertiesAccess()

Specifications: pure

signals_only java.lang.SecurityException;

checkPropertyAccess

public void checkPropertyAccess(String key)

Specifications: pure

requires_redundantly key != null;
signals_only java.lang.SecurityException;

checkTopLevelWindow

public boolean checkTopLevelWindow(Object window)

Specifications: pure

requires_redundantly window != null;

checkPrintJobAccess

public void checkPrintJobAccess()

Specifications: pure

signals_only java.lang.SecurityException;

checkSystemClipboardAccess

public void checkSystemClipboardAccess()

Specifications: pure

signals_only java.lang.SecurityException;

checkAwtEventQueueAccess

public void checkAwtEventQueueAccess()

Specifications: pure

signals_only java.lang.SecurityException;

checkPackageAccess

public void checkPackageAccess(String pkg)

Specifications: pure

requires_redundantly pkg != null;
signals_only java.lang.SecurityException;

checkPackageDefinition

public void checkPackageDefinition(String pkg)

Specifications: pure

requires_redundantly pkg != null;
signals_only java.lang.SecurityException;

checkSetFactory

public void checkSetFactory()

Specifications: pure

signals_only java.lang.SecurityException;

checkMemberAccess

public void checkMemberAccess(Class clazz,
                              int which)

Specifications: pure

requires_redundantly clazz != null;
signals_only java.lang.SecurityException;

checkSecurityAccess

public void checkSecurityAccess(String target)

Specifications: pure

requires !target.equals("");
signals_only java.lang.SecurityException;

getThreadGroup

public ThreadGroup getThreadGroup()

Specifications: pure

ensures_redundantly \result != null;