From ef939ab676ce35f80fc7718382fe584a513c7ca7 Mon Sep 17 00:00:00 2001
From: Florian Lugou <florian.lugou@telecom-paristech.fr>
Date: Wed, 31 May 2017 16:46:12 +0200
Subject: [PATCH] fixed ProVerif Output analysis for TML
---
src/proverifspec/ProVerifOutputAnalyzer.java | 9 ++++++---
src/tmltranslator/toavatar/TML2Avatar.java | 13 ++++++++-----
src/ui/window/JDialogProverifVerification.java | 3 ++-
3 files changed, 16 insertions(+), 9 deletions(-)
diff --git a/src/proverifspec/ProVerifOutputAnalyzer.java b/src/proverifspec/ProVerifOutputAnalyzer.java
index 9f08b95f39..cfe3301e1d 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 846e24026a..385552838b 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 4cdfe6d031..560a6aee91 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());
}
}
--
GitLab