001: package de.uka.ilkd.key.casetool.eclipse;
002:
003: /*
004: * This file is part of KeY - Integrated Deductive Software Design
005: * Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
006: * Universitaet Koblenz-Landau, Germany
007: * Chalmers University of Technology, Sweden
008: *
009: * The KeY system is protected by the GNU General Public License.
010: */
011:
012: import java.util.Vector;
013:
014: import org.eclipse.core.resources.IProject;
015: import org.eclipse.jdt.core.ICompilationUnit;
016: import org.eclipse.jdt.core.IMethod;
017: import org.eclipse.jdt.core.IType;
018: import org.eclipse.jdt.core.JavaModelException;
019: import org.eclipse.jface.action.IAction;
020: import org.eclipse.jface.dialogs.MessageDialog;
021: import org.eclipse.jface.viewers.ISelection;
022: import org.eclipse.jface.viewers.StructuredSelection;
023: import org.eclipse.jface.window.Window;
024: import org.eclipse.ui.IActionDelegate;
025: import org.eclipse.ui.IObjectActionDelegate;
026: import org.eclipse.ui.IWorkbenchPart;
027: import org.eclipse.ui.PlatformUI;
028:
029: import de.uka.ilkd.key.collection.ListOfString;
030: import de.uka.ilkd.key.collection.SLListOfString;
031: import de.uka.ilkd.key.gui.JMLPOAndSpecProvider;
032: import de.uka.ilkd.key.gui.Main;
033: import de.uka.ilkd.key.jml.JMLSpec;
034: import de.uka.ilkd.key.proof.init.AssignableCheckProofOblInput;
035:
036: /**
037: * @author Marius Hillenbrand
038: *
039: * Action which lets the user select proof obligations for a method.
040: * This action is selectable from the context menu of a java method.
041: */
042: public class MethodPOAction implements IObjectActionDelegate {
043:
044: ISelection selection;
045:
046: // quick-and-dirty for syncExec(dialog.open()) in swt thread
047: MethodPOSelectionDialog dialog;
048: int state;
049:
050: /**
051: * Constructor for Action1.
052: */
053: public MethodPOAction() {
054: super ();
055: }
056:
057: /**
058: * @see IObjectActionDelegate#setActivePart(IAction, IWorkbenchPart)
059: */
060: public void setActivePart(IAction action, IWorkbenchPart targetPart) {
061: }
062:
063: /**
064: * @see IActionDelegate#run(IAction)
065: */
066: public void run(IAction action) {
067: // MessageDialog.openInformation(
068: // PlatformUI.getWorkbench().getActiveWorkbenchWindow().getShell(),
069: // "KeYPlugIn Plug-in",
070: // "KeY Action was executed.");
071:
072: //new MethodPOSelectionDialog(PlatformUI.getWorkbench().getActiveWorkbenchWindow().getShell(), new Vector()).open();
073:
074: if (selection != null
075: && selection instanceof StructuredSelection) {
076: IMethod selectedMethod = (IMethod) ((StructuredSelection) selection)
077: .getFirstElement();
078: ICompilationUnit srcFile = selectedMethod
079: .getCompilationUnit();
080:
081: if (srcFile == null) {
082: MessageDialog.openError(PlatformUI.getWorkbench()
083: .getActiveWorkbenchWindow().getShell(),
084: "Not source method",
085: "The method you selected does not exist in source form. "
086: + "It cannot be used for a proof.");
087: } else {
088: // TODO generalize to consider packageFragmentRoots (needed to support
089: // special source locations like folders only linked into the eclipse
090: // project
091: IProject project = srcFile.getJavaProject()
092: .getProject();
093:
094: // assure the sources are parsed
095: int status = KeYPlugin.getDefault()
096: .assertProjectParsed(project, false);
097: // int status = KeYPlugin.PROJECT_ALREADY_OPEN;
098:
099: if (status == KeYPlugin.PROJECT_ALREADY_OPEN
100: || status == KeYPlugin.PROJECT_LOAD_SUCESSFUL) {
101: // determine the encapsulating class of the selected method
102: IType declaringType = selectedMethod
103: .getDeclaringType();
104:
105: // extract signature of method
106: //int paramCount = selectedMethod.getNumberOfParameters();
107: try {
108: //selectedMethod.get
109: String[] parameterNames = selectedMethod
110: .getParameterNames();
111: String[] parameterTypes = selectedMethod
112: .getParameterTypes();
113: ListOfString sigStrings = SLListOfString.EMPTY_LIST;
114:
115: for (int i = 0; i < parameterNames.length; i++) {
116: // System.out.println(parameterNames[i]+" \"" +parameterTypes[i]+"\"");
117:
118: String javaType = EclipseSignaturesHelper
119: .determineJavaType(
120: parameterTypes[i],
121: declaringType);
122:
123: if (javaType != null) {
124: sigStrings = sigStrings
125: .append(javaType);
126: } else {
127: MessageDialog
128: .openError(
129: PlatformUI
130: .getWorkbench()
131: .getActiveWorkbenchWindow()
132: .getShell(),
133: "Error determining signature types !",
134: "Could not resolve type "
135: + parameterTypes[i]
136: + " of the method's parameter "
137: + parameterNames[i]
138: + " !"
139: + " This is probably a syntax problem, check your import statements.");
140: return;
141: }
142: }
143:
144: JMLPOAndSpecProvider provider = Main
145: .getInstance()
146: .getJMLPOAndSpecProvider();
147: Main.getInstance().toBack();
148:
149: Vector methodSpecs = provider.getMethodSpecs(
150: declaringType.getFullyQualifiedName(),
151: selectedMethod.getElementName(),
152: sigStrings);
153: dialog = new MethodPOSelectionDialog(PlatformUI
154: .getWorkbench()
155: .getActiveWorkbenchWindow().getShell(),
156: methodSpecs);
157: state = dialog.open();
158:
159: boolean allInvariants = dialog
160: .isAllInvariantsSelected();
161: boolean addInvariantsToPostCondition = dialog
162: .isAddInvariantsToPostConditionSelected();
163:
164: if (state == Window.OK) {
165: Object selectedPO = dialog
166: .getSelectionOnOK()
167: .getFirstElement();
168: //System.out.println("Selected proof obligation: "+selectedPO);
169:
170: // TODO complete this step-by-step
171: // assignable: see JML Specification browser
172: //boolean assignablePO = (selectedPO instanceof AssignableCheckProofOblInput);
173: if (selectedPO instanceof AssignableCheckProofOblInput) {
174: AssignableCheckProofOblInput assignableCheckPO = (AssignableCheckProofOblInput) selectedPO;
175: provider.createPOandStartProver(
176: assignableCheckPO.getSpec(),
177: allInvariants,
178: addInvariantsToPostCondition,
179: true);
180: //assignableCheckPO.get
181:
182: } else if (selectedPO instanceof JMLSpec) {
183: provider.createPOandStartProver(
184: (JMLSpec) selectedPO,
185: allInvariants,
186: addInvariantsToPostCondition,
187: false);
188:
189: } else {
190: // TODO handle error case
191: }
192: }
193:
194: } catch (JavaModelException e) {
195: // TODO Auto-generated catch block
196: e.printStackTrace();
197: }
198: }
199: }
200: }
201: }
202:
203: /**
204: * @see IActionDelegate#selectionChanged(IAction, ISelection)
205: */
206: public void selectionChanged(IAction action, ISelection selection) {
207: this.selection = selection;
208: }
209:
210: }
|