diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java index 9f08b95f3963b64c897ec16249bab68b23788c7c..cfe3301e1da8086d14139840103d7d1e679fa31d 100644 --- a/src/proverifspec/ProVerifOutputAnalyzer.java +++ b/src/proverifspec/ProVerifOutputAnalyzer.java @@ -228,10 +228,13 @@ public class ProVerifOutputAnalyzer { { for (AvatarPragma pragma: pragmas) { - if (pragma instanceof AvatarPragmaSecret - && this.avatar2proverif.getTrueName(((AvatarPragmaSecret) pragma).getArg()).equals(attributeName)) + if (pragma instanceof AvatarPragmaSecret) { - this.results.put(pragma, result); + String trueName = this.avatar2proverif.getTrueName(((AvatarPragmaSecret) pragma).getArg()); + if (trueName != null && trueName.equals(attributeName)) + { + this.results.put(pragma, result); + } } } } diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java index 846e24026abd8924db5cb7e4e7a1ef9bddbbea4c..385552838b2d4cedc79004c8900c52faec46e996 100644 --- a/src/tmltranslator/toavatar/TML2Avatar.java +++ b/src/tmltranslator/toavatar/TML2Avatar.java @@ -1081,11 +1081,14 @@ public class TML2Avatar { sig=signalOutMap.get(ch.getName()); } if (ch.checkConf){ - if (!attrsToCheck.contains(getName(ch.getName())+"_chData")){ - AvatarAttribute attr = new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null); - attrsToCheck.add(getName(ch.getName())+"_chData"); - avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"_chData", ch.getReferenceObject(), attr)); - } + if (!attrsToCheck.contains(getName(ch.getName())+"_chData")){ + AvatarAttribute attr = block.getAvatarAttributeWithName(getName(ch.getName())+"_chData"); + if (attr != null) + { + attrsToCheck.add(getName(ch.getName())+"_chData"); + avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"_chData", ch.getReferenceObject(), attr)); + } + } } if (ch.checkAuth){ if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){ diff --git a/src/ui/window/JDialogProverifVerification.java b/src/ui/window/JDialogProverifVerification.java index 4cdfe6d0318966f0017720d885c355cbfdab990a..560a6aee915f271c589b261fd82f5582502b6c62 100644 --- a/src/ui/window/JDialogProverifVerification.java +++ b/src/ui/window/JDialogProverifVerification.java @@ -593,6 +593,7 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements mode = STOPPED; } catch (Exception e) { mode = STOPPED; + throw e; } @@ -678,7 +679,7 @@ public class JDialogProverifVerification extends javax.swing.JDialog implements curList.setSelectedIndex(row); this.menuItem.pragma = curList.getModel().getElementAt(row); this.menuItem.result = this.results.get(this.menuItem.pragma); - this.menuItem.setEnabled(this.menuItem.result.getTrace() != null); + this.menuItem.setEnabled(this.adp != null && this.menuItem.result.getTrace() != null); popup.show(e.getComponent(), e.getX(), e.getY()); } }