From 179c27eb29878662ef44fe7c2690d52f131d3b0d Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Thu, 27 Aug 2015 14:48:01 +0000
Subject: [PATCH] Update on how guards are handled by the proverif code
generator
---
src/avatartranslator/toproverif/AVATAR2ProVerif.java | 10 ++++++++--
src/ui/AvatarDesignPanel.java | 6 +++---
src/ui/CheckingError.java | 4 ++--
src/ui/GTURTLEModeling.java | 1 +
src/ui/window/JDialogProVerifGeneration.java | 4 ++++
5 files changed, 18 insertions(+), 7 deletions(-)
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 6d31a4a0d5..ed2bc3d312 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -51,6 +51,7 @@ import java.util.*;
import proverifspec.*;
import myutil.*;
import avatartranslator.*;
+import ui.*;
public class AVATAR2ProVerif {
@@ -961,14 +962,14 @@ public class AVATAR2ProVerif {
}
public void makeBlockProcesses(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, ProVerifProcess _p, LinkedList<ProVerifProcess> _processes, LinkedList<AvatarState> _states, String _choiceInfo) {
- AvatarSignal as;
+ avatartranslator.AvatarSignal as;
AvatarActionOnSignal aaos;
AvatarTransition at;
ProVerifProcess p, ptmp, ptmp1, ptmp2;
String tmp, name, value, term;
int i, j;
int index0, index1;
- AvatarMethod am;
+ avatartranslator.AvatarMethod am;
boolean found;
LinkedList<String> pos;
@@ -1143,6 +1144,11 @@ public class AVATAR2ProVerif {
TraceManager.addDev(" Adding guard: " + tmp);
addLineNoEnd(_p, "if " + tmp + " then");
} else {
+ CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Guard: " + at.getGuard() + " in block " + _block.getName() + " is not supported. Replacing by an empty guard");
+ ce.setAvatarBlock(_block);
+ ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(_block.getName()));
+ ce.setTGComponent((TGComponent)(at.getReferenceObject()));
+ warnings.add(ce);
addLineNoEnd(_p, "(* Unsuported guard:" + at.getGuard() + " *)");
}
}
diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java
index 20630c76fa..f4c39f7c32 100644
--- a/src/ui/AvatarDesignPanel.java
+++ b/src/ui/AvatarDesignPanel.java
@@ -324,12 +324,12 @@ public class AvatarDesignPanel extends TURTLEPanel {
}
public void modelBacktracingProVerif(ProVerifOutputAnalyzer pvoa) {
-
+
if (abdp == null) {
return;
}
- resetModelBacktracingProVerif();
+ resetModelBacktracingProVerif();
String block, attr, state;
int index;
@@ -339,7 +339,7 @@ public class AvatarDesignPanel extends TURTLEPanel {
TGComponent tgc;
// Confidential attributes
- for(String s: pvoa.getSecretTerms()) {
+ for(String s: pvoa.getSecretTerms()) {
index = s.indexOf("__");
if (index != -1) {
block = s.substring(0, index);
diff --git a/src/ui/CheckingError.java b/src/ui/CheckingError.java
index 937a5c5132..cb00ca9b92 100755
--- a/src/ui/CheckingError.java
+++ b/src/ui/CheckingError.java
@@ -65,7 +65,7 @@ public class CheckingError {
private TMLTask tmlt;
private TDiagramPanel tdp;
private TGComponent tgc;
- private AvatarBlock ab;
+ private AvatarBlock ab;
public CheckingError(int _type, String _message) {
type = _type;
@@ -84,7 +84,7 @@ public class CheckingError {
t = _t;
}
- public void setAvatarBlock(AvatarBlock _ab) {
+ public void setAvatarBlock(AvatarBlock _ab) {
ab = _ab;
}
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index c54eff9384..e7c952f163 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -629,6 +629,7 @@ public class GTURTLEModeling {
//tml2uppaal.setChoiceDeterministic(choices);
//tml2uppaal.setSizeInfiniteFIFO(_size);
proverif = avatar2proverif.generateProVerif(true, true, _stateReachability, _advancedTranslation);
+ warnings = avatar2proverif.getWarnings();
languageID = PROVERIF;
mgui.setMode(MainGUI.EDIT_PROVERIF_OK);
//mgui.setMode(MainGUI.MODEL_PROVERIF_OK);
diff --git a/src/ui/window/JDialogProVerifGeneration.java b/src/ui/window/JDialogProVerifGeneration.java
index acc74dcc61..7af509132b 100644
--- a/src/ui/window/JDialogProVerifGeneration.java
+++ b/src/ui/window/JDialogProVerifGeneration.java
@@ -331,6 +331,10 @@ public class JDialogProVerifGeneration extends javax.swing.JDialog implements Ac
} else {
jta.append("Could not generate proverif code\n");
}
+
+ //if (mgui.gtm.getCheckingWarnings().size() > 0) {
+ jta.append("" + mgui.gtm.getCheckingWarnings().size() + " warning(s)\n");
+ //}
}
--
GitLab