Re: SPARK option set

[Christophe Massol <cmassol@sophia.inria.fr>]

I use :


System.out.println("*** Reading default options ");
		String defaultOptions = SparkOptions.getDefaultOptions();
		StringTokenizer decoupe = new StringTokenizer(defaultOptions, " ");
		while(decoupe.hasMoreElements()){
			String option = decoupe.nextToken();
			StringTokenizer decoupeOption = new StringTokenizer(option, ":");
			String key = decoupeOption.nextToken();
			String value = decoupeOption.nextToken();
			// Modify an option
			if(key.startsWith("forceGCs"))
				value = "true";
			map.put(key, value);
		}

Le Dimanche 3 Août 2003 01:43, Eric Bodden a écrit :
> Hi!
>
> I am currently about to use SPARK using the API and not soot.Main etc. So I
> came across the class SparkOptions and I don't really understand how it
> works. My current code is:

-- 

Cordialement,

	Massol Christophe
---------------------------------------------------------------
Stagiaire Projet OASIS  
[049238 7558]

 Etudiant en maîtrise MIAGE à l'université de Nice

 Tel: 06 12 53 72 44
 Adresse: 217 bd de la madeleine
 06000 Nice