From 6cacc9485038fc3aa7e32646be57773f3d0af4f6 Mon Sep 17 00:00:00 2001
From: Florian Lugou <florian.lugou@telecom-paristech.fr>
Date: Tue, 6 Oct 2015 12:21:06 +0000
Subject: [PATCH] added constant translation and public pragma translation in
ProVerif
---
src/avatartranslator/AvatarBlock.java | 4 ++++
src/avatartranslator/AvatarTerm.java | 7 +++++++
src/avatartranslator/toproverif/AVATAR2ProVerif.java | 6 ++++++
3 files changed, 17 insertions(+)
diff --git a/src/avatartranslator/AvatarBlock.java b/src/avatartranslator/AvatarBlock.java
index 948eff39f4..4c7005c9d2 100644
--- a/src/avatartranslator/AvatarBlock.java
+++ b/src/avatartranslator/AvatarBlock.java
@@ -138,6 +138,10 @@ public class AvatarBlock extends AvatarElement {
return this.avspec.getAvatarConstantWithName (_name);
}
+ public void addConstant (AvatarConstant _constant) {
+ this.avspec.addConstant (_constant);
+ }
+
public void addIntAttributeIfApplicable(String _name) {
if (getAvatarAttributeWithName(_name) == null) {
AvatarAttribute aa = new AvatarAttribute(_name, AvatarType.INTEGER, this, null);
diff --git a/src/avatartranslator/AvatarTerm.java b/src/avatartranslator/AvatarTerm.java
index bb7715f9e3..0ec7cca4d1 100644
--- a/src/avatartranslator/AvatarTerm.java
+++ b/src/avatartranslator/AvatarTerm.java
@@ -78,6 +78,13 @@ public abstract class AvatarTerm extends AvatarElement {
result = block.getAvatarConstantWithName (toParse);
if (result != null)
return result;
+
+ // Consider that new names are constants
+ if (AvatarTerm.isValidName (toParse)) {
+ result = new AvatarConstant (toParse, block);
+ block.addConstant ((AvatarConstant) result);
+ return result;
+ }
//TraceManager.addDev ("AvatarConstant '" + toParse + "' couldn't be parsed");
//TraceManager.addDev ("AvatarTerm '" + toParse + "' couldn't be parsed");
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 509ddc4c2b..86da67c446 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -592,6 +592,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
allKnowledge.add (arg);
}
+ for (AvatarPragma pragma: this.avspec.getPragmas ())
+ if (pragma instanceof AvatarPragmaPublic)
+ for (AvatarAttribute attr: pragma.getArgs ())
+ if (attr.getBlock () == ab)
+ lastInstr = lastInstr.setNextInstr ( new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm (attr, null) + ");"));
+
// Call the first "real" process
String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((call__" + ab.getName () + "__0";
for(ProVerifVar aa: this.getAttributesFromBlock (ab))
--
GitLab