diff --git a/src/avatartranslator/AvatarBlock.java b/src/avatartranslator/AvatarBlock.java index 948eff39f4c5c015f05d52d19f6d78497f4ba419..4c7005c9d2491877eb34cc4c3991f7c7986335c4 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 bb7715f9e32f39c0b66d0d4f73baaa589d5d5069..0ec7cca4d134ec1d545c1105bc5adb5666adc10a 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 509ddc4c2b0a48236b99b4463097db43931086a8..86da67c446389f758b2f02c68210b86685530a8e 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))