Skip to content

Commit

Permalink
graceful handling of unsupported JML features (issue #930)
Browse files Browse the repository at this point in the history
  • Loading branch information
Benjamin Weiss committed Dec 22, 2008
1 parent 37519ec commit 2bf9425
Show file tree
Hide file tree
Showing 12 changed files with 369 additions and 243 deletions.
3 changes: 2 additions & 1 deletion system/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -257,7 +257,8 @@ GENERATED_SETS=logic/SetAsListOfTerm collection/SetAsListOfString \
java/statement/SetAsListOfLoopStatement \
proof/SetAsListOfGoalChooserBuilder \
strategy/SetAsListOfStrategyFactory \
logic/op/SetAsListOfLocation
logic/op/SetAsListOfLocation \
speclang/SetAsListOfPositionedString

GENERATED_MAPS= collection/MapAsListFromIntegerToString \
logic/op/MapAsListFromQuantifiableVariableToInteger \
Expand Down
42 changes: 25 additions & 17 deletions system/de/uka/ilkd/key/java/recoderext/JMLTransformer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,9 @@
import de.uka.ilkd.key.collection.SLListOfString;
import de.uka.ilkd.key.gui.configuration.ProofSettings;
import de.uka.ilkd.key.speclang.PositionedString;
import de.uka.ilkd.key.speclang.jml.pretranslation.KeYJMLPreParser;
import de.uka.ilkd.key.speclang.jml.pretranslation.ListOfTextualJMLConstruct;
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLFieldDecl;
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLMethodDecl;
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSetStatement;
import de.uka.ilkd.key.speclang.SetAsListOfPositionedString;
import de.uka.ilkd.key.speclang.SetOfPositionedString;
import de.uka.ilkd.key.speclang.jml.pretranslation.*;
import de.uka.ilkd.key.speclang.translation.SLTranslationException;
import recoder.CrossReferenceServiceConfiguration;
import recoder.abstraction.Constructor;
Expand All @@ -47,6 +44,8 @@ public class JMLTransformer extends RecoderModelTransformer {
"public",
"static"});

private static SetOfPositionedString warnings;


/**
* Creates a transformation that adds JML specific elements, for example
Expand All @@ -64,13 +63,14 @@ public class JMLTransformer extends RecoderModelTransformer {
public JMLTransformer(CrossReferenceServiceConfiguration services,
TransformerCache cache) {
super(services, cache);
warnings = SetAsListOfPositionedString.EMPTY_SET;
}



// -------------------------------------------------------------------------
// private helper methods
// -------------------------------------------------------------------------
//-------------------------------------------------------------------------
//private helper methods
//-------------------------------------------------------------------------

/**
* Concatenates the passed comments in a position-preserving way.
Expand Down Expand Up @@ -204,9 +204,9 @@ private Comment[] getCommentsAndSetParent(ProgramElement pe) {



// -------------------------------------------------------------------------
// private transformation methods
// -------------------------------------------------------------------------
//-------------------------------------------------------------------------
//private transformation methods
//-------------------------------------------------------------------------

private void transformFieldDecl(TextualJMLFieldDecl decl,
Comment[] originalComments)
Expand Down Expand Up @@ -416,6 +416,7 @@ private void transformClasslevelComments(TypeDeclaration td,
= new KeYJMLPreParser(concatenatedComment, fileName, pos);
ListOfTextualJMLConstruct constructs
= preParser.parseClasslevelComment();
warnings = warnings.union(preParser.getWarnings());

//handle model and ghost declarations in textual constructs
//(and set assignments which RecodeR evilly left hanging *behind*
Expand Down Expand Up @@ -475,6 +476,7 @@ private void transformMethodlevelCommentsHelper(ProgramElement pe,
= new KeYJMLPreParser(concatenatedComment, fileName, pos);
ListOfTextualJMLConstruct constructs
= preParser.parseMethodlevelComment();
warnings = warnings.union(preParser.getWarnings());

//handle ghost declarations and set assignments in textual constructs
for(TextualJMLConstruct c : constructs) {
Expand All @@ -498,9 +500,9 @@ private void transformMethodlevelComments(MethodDeclaration md,



// -------------------------------------------------------------------------
// RecoderModelTransformer - abstract methods implementation
// -------------------------------------------------------------------------
//-------------------------------------------------------------------------
//RecoderModelTransformer - abstract methods implementation
//-------------------------------------------------------------------------

protected void makeExplicit(TypeDeclaration td) {
assert false;
Expand Down Expand Up @@ -544,6 +546,7 @@ public void makeExplicit() {
// use getOriginalDataLocation instead
DataLocation dl = unit.getOriginalDataLocation();
String fileName = dl == null ? "" : dl.toString();
fileName = fileName.replaceFirst("FILE:", "");

transformClasslevelComments(td, fileName);

Expand All @@ -554,7 +557,7 @@ public void makeExplicit() {
ConstructorDeclaration cd
= (ConstructorDeclaration)
constructorList.get(k);
transformMethodlevelComments(cd, unit.getName());
transformMethodlevelComments(cd, fileName);
}
}

Expand All @@ -564,7 +567,7 @@ public void makeExplicit() {
MethodDeclaration md
= (MethodDeclaration)
methodList.get(k);
transformMethodlevelComments(md, unit.getName());
transformMethodlevelComments(md, fileName);
}
}

Expand All @@ -583,6 +586,11 @@ public void makeExplicit() {
}


public static SetOfPositionedString getWarningsOfLastInstance() {
return warnings;
}


//-------------------------------------------------------------------------
//inner classes
//-------------------------------------------------------------------------
Expand Down
2 changes: 1 addition & 1 deletion system/de/uka/ilkd/key/speclang/PositionedString.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ public PositionedString(String text) {


public String toString() {
return text;
return text + " (" + fileName + ", " + pos + ")";
}


Expand Down
76 changes: 76 additions & 0 deletions system/de/uka/ilkd/key/speclang/SLEnvInput.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,19 @@

package de.uka.ilkd.key.speclang;

import java.awt.BorderLayout;
import java.awt.Container;
import java.awt.Dimension;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.awt.event.KeyEvent;
import java.util.Arrays;
import java.util.Comparator;
import java.util.Set;

import javax.swing.*;

import de.uka.ilkd.key.gui.Main;
import de.uka.ilkd.key.gui.configuration.GeneralSettings;
import de.uka.ilkd.key.gui.configuration.ProofSettings;
import de.uka.ilkd.key.java.JavaInfo;
Expand Down Expand Up @@ -79,6 +88,67 @@ public int compare(KeYJavaType o1, KeYJavaType o2) {
}


private void showWarningDialog(SetOfPositionedString warnings) {
if(!Main.visible) {
return;
}

final JDialog dialog = new JDialog(Main.getInstance(),
getLanguage() + " warning",
true);
dialog.setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE);
Container pane = dialog.getContentPane();
pane.setLayout(new BorderLayout());

//top label
JLabel label = new JLabel("The following non-fatal "
+ "problems occurred when translating your "
+ getLanguage() + " specifications:");
label.setBorder(BorderFactory.createEmptyBorder(5, 5, 0, 5));
pane.add(label, BorderLayout.NORTH);

//scrollable warning list
JScrollPane scrollpane = new JScrollPane();
scrollpane.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5));
JList list = new JList(warnings.toArray());
list.setBorder(BorderFactory.createLoweredBevelBorder());
scrollpane.setViewportView(list);
pane.add(scrollpane, BorderLayout.CENTER);

//ok button
final JButton button = new JButton("OK");
button.addActionListener(new ActionListener() {
public void actionPerformed(ActionEvent e) {
dialog.setVisible(false);
dialog.dispose();
}
});
Dimension buttonDim = new Dimension(100, 27);
button.setPreferredSize(buttonDim);
button.setMinimumSize(buttonDim);
JPanel panel = new JPanel();
panel.add(button);
pane.add(panel, BorderLayout.SOUTH);
dialog.getRootPane().setDefaultButton(button);

button.registerKeyboardAction(
new ActionListener() {
public void actionPerformed(ActionEvent event) {
if(event.getActionCommand().equals("ESC")) {
button.doClick();
}
}
},
"ESC",
KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0),
JComponent.WHEN_IN_FOCUSED_WINDOW);

dialog.setSize(700, 300);
dialog.setLocationRelativeTo(Main.getInstance());
dialog.setVisible(true);
}


private void createSpecs(SpecExtractor specExtractor)
throws ProofInputException {
JavaInfo javaInfo
Expand Down Expand Up @@ -124,6 +194,12 @@ private void createSpecs(SpecExtractor specExtractor)
}
}
}

//show warnings to user
SetOfPositionedString warnings = specExtractor.getWarnings();
if(warnings != null && warnings.size() > 0) {
showWarningDialog(warnings);
}
}


Expand Down
7 changes: 7 additions & 0 deletions system/de/uka/ilkd/key/speclang/SpecExtractor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,4 +38,11 @@ public SetOfClassInvariant extractClassInvariants(KeYJavaType kjt)
public LoopInvariant extractLoopInvariant(ProgramMethod pm,
LoopStatement loop)
throws SLTranslationException;

/**
* Returns all warnings generated so far in the translation process.
* (e.g. this may warn about unsupported features which have been ignored
* by the translation)
*/
public SetOfPositionedString getWarnings();
}

0 comments on commit 2bf9425

Please sign in to comment.