jack.plugin.compile
Class PoGenerator

java.lang.Object
  jack.plugin.RunnableWithError
      jack.plugin.Generator
          jack.plugin.compile.PoGenerator

All Implemented Interfaces:

org.eclipse.jface.operation.IRunnableWithProgress

public class PoGenerator

extends Generator

implements org.eclipse.jface.operation.IRunnableWithProgress

Class that calls jml2b in order to generate proof obligations.

Author:

A. Requet, L. Burdy

Field Summary

Fields inherited from class jack.plugin.Generator

ECLIPSE_RESOURCE_KEY, PROBLEM_MARKER_TYPE

Constructor Summary

PoGenerator(org.eclipse.jdt.core.ICompilationUnit c)

PoGenerator(java.util.Iterator compilation_units)
Create a new PoGenerator allowing to generate proof obligations for the given compilation units.

Method Summary

static void

compile(org.eclipse.jdt.core.ICompilationUnit ci)

Methods inherited from class jack.plugin.Generator

loadDefaultClasses, run

Methods inherited from class jack.plugin.RunnableWithError

getErrorDescription, getErrorDetails, hasDetails, hasSucceeded

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.eclipse.jface.operation.IRunnableWithProgress

run

Constructor Detail

PoGenerator

public PoGenerator(java.util.Iterator compilation_units)

Create a new PoGenerator allowing to generate proof obligations for the given compilation units.

Parameters:

compilation_units - the compilations units for which the POs should be generated.

PoGenerator

public PoGenerator(org.eclipse.jdt.core.ICompilationUnit c)

Method Detail

compile

public static void compile(org.eclipse.jdt.core.ICompilationUnit ci)