From 1331c16424852d824055dfd5e0caeb62c42ce22a Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Wed, 23 Feb 2022 17:54:49 +0100
Subject: [PATCH] Solving bug on proverif: arithmetic ops had no diviser
---
.../avatartranslator/AvatarArithmeticOp.java | 2 +-
.../AvatarStateMachineElement.java | 2 +-
.../toproverif/AVATAR2ProVerif.java | 16 +++++++++++++---
3 files changed, 15 insertions(+), 5 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarArithmeticOp.java b/src/main/java/avatartranslator/AvatarArithmeticOp.java
index 051e56af12..19f10503e8 100644
--- a/src/main/java/avatartranslator/AvatarArithmeticOp.java
+++ b/src/main/java/avatartranslator/AvatarArithmeticOp.java
@@ -53,7 +53,7 @@ public class AvatarArithmeticOp extends AvatarTerm {
AvatarTerm term2;
String operator;
- private static final String [] knownOp = {"+", "-", "*"};
+ private static final String [] knownOp = {"+", "-", "*", "/"};
public AvatarArithmeticOp (AvatarTerm _term1, AvatarTerm _term2, String _operator, Object _referenceObject) {
super (_term1.getName () + _operator + _term2.getName (), _referenceObject);
diff --git a/src/main/java/avatartranslator/AvatarStateMachineElement.java b/src/main/java/avatartranslator/AvatarStateMachineElement.java
index 64384093f1..7cd31738a3 100644
--- a/src/main/java/avatartranslator/AvatarStateMachineElement.java
+++ b/src/main/java/avatartranslator/AvatarStateMachineElement.java
@@ -196,7 +196,7 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
return false;
}
-
+
public boolean inAnUpperStateOf(AvatarState _state) {
if (_state == null) {
diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index 01d12b6d73..57953a87f0 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -231,10 +231,14 @@ public class AVATAR2ProVerif implements AvatarTranslator {
protected static String translateTerm (AvatarTerm term, Map<AvatarAttribute, Integer> attributeCmp) {
if (term instanceof AvatarAttribute) {
AvatarAttribute attr = (AvatarAttribute) term;
+
if (attributeCmp != null) {
+ TraceManager.addDev("Mae Attr name 1");
return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName (), attributeCmp.get (attr).toString ());
- } else
- return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName ());
+ } else {
+ TraceManager.addDev("Mae Attr name 2");
+ return AVATAR2ProVerif.makeAttrName(attr.getBlock().getName(), attr.getName());
+ }
}
if (term instanceof AvatarConstant) {
@@ -259,16 +263,18 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return sb.toString ();
} else {
+ TraceManager.addDev("ERROR=ZERO");
// TODO: raise error
return ZERO;
}
- } catch (NumberFormatException e) { }
+ } catch (NumberFormatException e) { TraceManager.addDev("ERROR=NFE");}
return constant.getName ();
}
if (term instanceof AvatarArithmeticOp) {
AvatarArithmeticOp op = (AvatarArithmeticOp) term;
+ TraceManager.addDev("TERM=" + op.toString());
if (op.getOperator ().compareTo ("+") == 0) {
AvatarTerm t1, t2;
t1 = op.getTerm1 ();
@@ -279,6 +285,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
t2 = t;
} else if (!(t2 instanceof AvatarConstant)) {
// TODO: raise error
+ TraceManager.addDev("ERROR= t2!=constant");
return null;
}
@@ -299,16 +306,19 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return sb.toString ();
} else {
// TODO: raise error
+ TraceManager.addDev("ERROR= max int");
return AVATAR2ProVerif.translateTerm(t1, attributeCmp);
}
} catch (NumberFormatException e) {
// TODO: raise error
+ TraceManager.addDev("ERROR= NumberFormatException");
return AVATAR2ProVerif.translateTerm(t1, attributeCmp);
}
} else {
// TODO: raise error
+ TraceManager.addDev("ERROR= not a +");
return null;
}
}
--
GitLab