import gov.nasa.jpf.util.JPFLogger; //导入依赖的package包/类
private static void log (JPFLogger logger, int logLevel, String msg){
  switch (logLevel){
  case SEVERE:
    logger.severe( msg);
    break;
  case WARNING:
    logger.warning( msg);
    break;
  case INFO:
    logger.info( msg);
    break;
  case FINE:
    logger.fine( msg);
    break;
  case FINER:
    logger.finer( msg);
    break;
  case FINEST:
    logger.finest( msg);
    break;
  default:
    throw new JPFException("unknown log level " + logLevel + " for logger " + logger.getName());
  }    
}
 

import gov.nasa.jpf.util.JPFLogger; //导入依赖的package包/类
@MJI
public static void log__Ljava_lang_String_2ILjava_lang_String_2_3Ljava_lang_Object_2__V (MJIEnv env, int clsObjRef,
    int loggerIdRef, int logLevel, int fmtRef, int argsRef){
  String loggerId = env.getStringObject(loggerIdRef);
  String fmt = env.getStringObject(fmtRef);
  JPFLogger logger = JPF.getLogger(loggerId);

  int[] argRefs = env.getReferenceArrayObject( argsRef);
  Object[] args = new Object[argRefs.length];
  for (int i=0; i<args.length; i++){
    ElementInfo eiArg = env.getElementInfo(argRefs[i]);
    if (eiArg.isStringObject()){
      args[i] = env.getStringObject(argRefs[i]);
    } else if (eiArg.isBoxObject()){
      args[i] = eiArg.asBoxObject(); 
    } else {
      args[i] = eiArg.toString();
    }
  }
  
  String msg = String.format(fmt, args);
  
  log( logger, logLevel, msg);
}
 

import gov.nasa.jpf.util.JPFLogger; //导入依赖的package包/类
private static void writeResultToFile(String content, String filename) {
  try (PrintWriter writer = new PrintWriter(filename)) {
    writer.print(content);
  } catch (IOException e) {
    JPFLogger.getLogger("psyco").severe(e.getStackTrace().toString());
  }
}
 

import gov.nasa.jpf.util.JPFLogger; //导入依赖的package包/类
@MJI
public static void log__Ljava_lang_String_2ILjava_lang_String_2__V (MJIEnv env, int clsObjRef,
    int loggerIdRef, int logLevel, int msgRef){
  String loggerId = env.getStringObject(loggerIdRef);
  String msg = env.getStringObject(msgRef);
  JPFLogger logger = JPF.getLogger(loggerId);
  
  log( logger, logLevel, msg);
}
 

import gov.nasa.jpf.util.JPFLogger; //导入依赖的package包/类
@MJI
public static void log__Ljava_lang_String_2ILjava_lang_String_2Ljava_lang_String_2__V (MJIEnv env, int clsObjRef,
    int loggerIdRef, int logLevel, int arg1Ref, int arg2Ref){
  String loggerId = env.getStringObject(loggerIdRef);
  String msg = env.getStringObject(arg1Ref) + env.getStringObject(arg2Ref);
  JPFLogger logger = JPF.getLogger(loggerId);
  
  log( logger, logLevel, msg);
}
 

import gov.nasa.jpf.util.JPFLogger; //导入依赖的package包/类
public SearchEngine(PsycoConfig pconf) {
  this.pconf = pconf;
  logger = JPFLogger.getLogger(HelperMethods.getLoggerName());
  updateFolderName(pconf);
}
 

import gov.nasa.jpf.util.JPFLogger; //导入依赖的package包/类
/**
 * use this one to get a Logger that is initialized via our Config mechanism. Note that
 * our own Loggers do NOT pass
 */
public static JPFLogger getLogger (String name) {
  return LogManager.getLogger( name);
}