Commit c8d455a6 authored by Florian Lugou's avatar Florian Lugou

Added new compilation flags for warnings and cleaned up code

parent 04609774
......@@ -62,7 +62,7 @@ export TTOOL_LIBS = $(TTOOL_PATH)/libs
export TTOOL_LIBRARIES = $(wildcard $(TTOOL_LIBS)/*.jar)
export TTOOL_CLASSPATH = $(subst $(eval) ,:,$(TTOOL_LIBRARIES))
export GLOBAL_CFLAGS = -encoding "UTF8" -Xlint:unchecked -Xlint:deprecation
export GLOBAL_CFLAGS = -encoding "UTF8" -Xlint:unchecked -Xlint:deprecation -Xlint:cast -Xlint:divzero -Xlint:empty -Xlint:finally -Xlint:fallthrough
export TTOOL_DIR = $(TTOOL_PATH)/ttool
export TTOOL_BINARY = $(TTOOL_BIN)/ttool.jar
......
......@@ -96,11 +96,8 @@ public class Attack {
}
public boolean isFinal() {
if (destinationNodes.size() == 0) {
return true;
}
return destinationNodes.size() == 0;
return false;
}
}
......@@ -70,11 +70,7 @@ public abstract class AttackNode {
return false;
}
if (inputAttacks.size() < 1) {
return false;
}
return true;
return inputAttacks.size() >= 1;
}
......
......@@ -79,7 +79,7 @@ public class Automata {
}
public State getState(int index) {
return (State)(states.get(index));
return states.get(index);
}
public void addState(State s) {
......
......@@ -48,24 +48,24 @@ package avatartranslator;
import java.util.HashMap;
public interface AvatarAction {
public boolean isAMethodCall ();
public boolean isAVariableSetting ();
public boolean isABasicVariableSetting ();
public String getName ();
boolean isAMethodCall();
boolean isAVariableSetting();
boolean isABasicVariableSetting();
String getName();
/**
* Returns True if the whole action contains a method call.
*
* @return True if the whole action contains a method call. False otherwise.
*/
public boolean containsAMethodCall ();
boolean containsAMethodCall();
/**
* Returns a full clone of the action.
*
* @return A clone of the action.
*/
public AvatarAction clone ();
AvatarAction clone();
/**
* Replaces attributes in this action according to the provided mapping.
......@@ -73,5 +73,5 @@ public interface AvatarAction {
* @param attributesMapping
* The mapping used to replace the attributes of the action. All the attributes of the block should be present as keys.
*/
public void replaceAttributes (HashMap<AvatarAttribute, AvatarAttribute> attributesMapping);
void replaceAttributes(HashMap<AvatarAttribute, AvatarAttribute> attributesMapping);
}
......@@ -99,12 +99,12 @@ public class AvatarActionAssignment implements AvatarAction {
@Override
public void replaceAttributes (HashMap<AvatarAttribute, AvatarAttribute> attributesMapping) {
if (this.leftHand instanceof AvatarAttribute)
this.leftHand = attributesMapping.get ((AvatarAttribute) this.leftHand);
this.leftHand = attributesMapping.get (this.leftHand);
else
this.leftHand.replaceAttributes (attributesMapping);
if (this.rightHand instanceof AvatarAttribute)
this.rightHand = attributesMapping.get ((AvatarAttribute) this.rightHand);
this.rightHand = attributesMapping.get (this.rightHand);
else
this.rightHand.replaceAttributes (attributesMapping);
}
......
......@@ -114,12 +114,12 @@ public class AvatarArithmeticOp extends AvatarTerm {
@Override
public void replaceAttributes (HashMap<AvatarAttribute, AvatarAttribute> attributesMapping) {
if (this.term1 instanceof AvatarAttribute)
this.term1 = attributesMapping.get ((AvatarAttribute) this.term1);
this.term1 = attributesMapping.get (this.term1);
else
this.term1.replaceAttributes (attributesMapping);
if (this.term2 instanceof AvatarAttribute)
this.term2 = attributesMapping.get ((AvatarAttribute) this.term2);
this.term2 = attributesMapping.get (this.term2);
else
this.term2.replaceAttributes (attributesMapping);
}
......
......@@ -344,11 +344,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
String params = _s.substring(index0+1, index1).trim();
//TraceManager.addDev("params=" + params);
if (params.length() == 0) {
if (am.getListOfAttributes().size() == 0) {
return true;
} else {
return false;
}
return am.getListOfAttributes().size() == 0;
}
//TraceManager.addDev("params=" + params);
String [] actions = params.split(",");
......
......@@ -125,7 +125,7 @@ public class AvatarSignal extends AvatarMethod {
public AvatarSignal advancedClone(AvatarStateMachineOwner _block) {
AvatarSignal as = new AvatarSignal(getName(), getInOut(), getReferenceObject());
setAdvancedClone((AvatarMethod)as, _block);
setAdvancedClone(as, _block);
return as;
}
......@@ -135,6 +135,6 @@ public class AvatarSignal extends AvatarMethod {
return false;
}
return super.isCompatibleWith((AvatarMethod)_as);
return super.isCompatibleWith(_as);
}
}
......@@ -88,7 +88,7 @@ public class AvatarSimpleGuardDuo extends AvatarSimpleGuard {
public void replaceAttributes (HashMap<AvatarAttribute, AvatarAttribute> attributesMapping) {
if (this.termA instanceof AvatarAttribute)
{
this.termA = attributesMapping.get((AvatarAttribute) this.termA);
this.termA = attributesMapping.get(this.termA);
}
else
{
......@@ -96,7 +96,7 @@ public class AvatarSimpleGuardDuo extends AvatarSimpleGuard {
}
if (this.termB instanceof AvatarAttribute)
{
this.termB = attributesMapping.get((AvatarAttribute) this.termB);
this.termB = attributesMapping.get(this.termB);
}
else
{
......
......@@ -79,7 +79,7 @@ public class AvatarSimpleGuardMono extends AvatarSimpleGuard {
}
if (this.term instanceof AvatarAttribute)
{
this.term = attributesMapping.get(((AvatarAttribute) this.term));
this.term = attributesMapping.get(this.term);
}
else
{
......
......@@ -1562,7 +1562,7 @@ public class AvatarStateMachine extends AvatarElement {
for (AvatarStateMachineElement asme: curAsme.getNexts ()) {
/* Check if it is a function call */
if (asme instanceof AvatarLibraryFunctionCall) {
AvatarStateMachineElement replaceBy = callsTranslated.get ((AvatarLibraryFunctionCall) asme);
AvatarStateMachineElement replaceBy = callsTranslated.get (asme);
/* Check if function call has already been translated */
if (replaceBy != null) {
/* replace by the translated function call */
......
......@@ -323,8 +323,8 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
gg1 = new AvatarSimpleGuardDuo (gg1.getTermA (), gg1.getTermB (), gg2.getBinaryOp ());
String s1, s2;
s1 = this.myTrim (gg1.getRealGuard (this).toString ());
s2 = this.myTrim (gg2.getRealGuard (this).toString ());
s1 = myTrim (gg1.getRealGuard (this).toString ());
s2 = myTrim (gg2.getRealGuard (this).toString ());
return s1.equals (s2);
}
......@@ -333,8 +333,8 @@ public abstract class AvatarStateMachineElement extends AvatarElement {
}
String s1, s2;
s1 = this.myTrim (g1.getRealGuard (this).toString ());
s2 = this.myTrim (((AvatarComposedGuard) g2).getOpposite ().toString ());
s1 = myTrim (g1.getRealGuard (this).toString ());
s2 = myTrim (((AvatarComposedGuard) g2).getOpposite ().toString ());
return s1.equals (s2);
}
......
......@@ -46,10 +46,10 @@ import java.util.LinkedList;
* @author Florian LUGOU
*/
public interface AvatarStateMachineOwner {
public String getName ();
public AvatarStateMachine getStateMachine ();
public AvatarSignal getAvatarSignalWithName (String signalName);
public AvatarMethod getAvatarMethodWithName (String methodName);
String getName();
AvatarStateMachine getStateMachine();
AvatarSignal getAvatarSignalWithName(String signalName);
AvatarMethod getAvatarMethodWithName(String methodName);
/**
* Look for an attribute in the list of local attributes, parameters and return values.
......@@ -59,10 +59,10 @@ public interface AvatarStateMachineOwner {
*
* @return The corresponding attribute if found, null otherwise.
*/
public AvatarAttribute getAvatarAttributeWithName (String attributeName);
AvatarAttribute getAvatarAttributeWithName(String attributeName);
public AvatarSpecification getAvatarSpecification ();
public LinkedList<AvatarAttribute> getAttributes ();
public void addAttribute (AvatarAttribute attribute);
public AvatarStateMachineOwner advancedClone(AvatarSpecification avspec);
AvatarSpecification getAvatarSpecification();
LinkedList<AvatarAttribute> getAttributes();
void addAttribute(AvatarAttribute attribute);
AvatarStateMachineOwner advancedClone(AvatarSpecification avspec);
}
......@@ -331,18 +331,11 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
public boolean hasDelay() {
if (minDelay.trim().length() == 0) {
return false;
}
return true;
return minDelay.trim().length() != 0;
}
public boolean hasCompute() {
if (minCompute.trim().length() ==0) {
return false;
}
return true;
return minCompute.trim().length() != 0;
}
public boolean hasActions() {
......
......@@ -46,12 +46,12 @@
package avatartranslator;
public interface AvatarTranslator {
public void translateTimerOperator (AvatarTimerOperator _asme, Object _arg);
public void translateActionOnSignal (AvatarActionOnSignal _asme, Object _arg);
public void translateTransition (AvatarTransition _asme, Object _arg);
public void translateStartState (AvatarStartState _asme, Object _arg);
public void translateState (AvatarState _asme, Object _arg);
public void translateRandom (AvatarRandom _asme, Object _arg);
public void translateStopState (AvatarStopState _asme, Object _arg);
public void translateLibraryFunctionCall (AvatarLibraryFunctionCall _asme, Object _arg);
void translateTimerOperator(AvatarTimerOperator _asme, Object _arg);
void translateActionOnSignal(AvatarActionOnSignal _asme, Object _arg);
void translateTransition(AvatarTransition _asme, Object _arg);
void translateStartState(AvatarStartState _asme, Object _arg);
void translateState(AvatarState _asme, Object _arg);
void translateRandom(AvatarRandom _asme, Object _arg);
void translateStopState(AvatarStopState _asme, Object _arg);
void translateLibraryFunctionCall(AvatarLibraryFunctionCall _asme, Object _arg);
}
......@@ -144,7 +144,7 @@ public class AvatarTuple extends AvatarLeftHand {
LinkedList<AvatarTerm> components = new LinkedList<AvatarTerm> ();
for (AvatarTerm term: this.components)
if (term instanceof AvatarAttribute)
components.add (attributesMapping.get ((AvatarAttribute) term));
components.add (attributesMapping.get (term));
else {
components.add (term);
term.replaceAttributes (attributesMapping);
......
......@@ -318,7 +318,7 @@ public class AvatarSimulationBlock {
}
ast.clockValueWhenFinished = _clockValue;
ast.duration = 0;
ast.id = ast.setID();
ast.id = AvatarSimulationTransaction.setID();
if (_aspt != null) {
ast.silent = _aspt.isSilent;
} else {
......
......@@ -50,7 +50,7 @@ package avatartranslator.directsimulation;
public interface AvatarSimulationInteraction {
public void setMode(int _mode);
void setMode(int _mode);
public void updateTransactionAndTime(int _nbOfTransactions, long clockValue);
void updateTransactionAndTime(int _nbOfTransactions, long clockValue);
}
\ No newline at end of file
......@@ -151,21 +151,14 @@ public class AvatarSimulationPendingTransaction {
if (!hasDelay) {
return false;
}
if (myMinDuration>0) {
return true;
}
return false;
return myMinDuration > 0;
}
if ((!durationOnCurrent) && (!durationOnOther)) {
return false;
}
if (myMinDuration >0) {
return true;
}
return false;
return myMinDuration > 0;
}
......
......@@ -982,11 +982,7 @@ public class AvatarSpecificationSimulation {
if (_aspt.elementToExecute instanceof AvatarActionOnSignal) {
AvatarSignal sig = ((AvatarActionOnSignal)(_aspt.elementToExecute)).getSignal();
AvatarRelation rel = avspec.getAvatarRelationWithSignal(sig);
if (sig.isOut()) {
_aspt.isSending = true;
} else {
_aspt.isSending = false;
}
_aspt.isSending = sig.isOut();
if (rel.isAsynchronous()) {
_aspt.isSynchronous = false;
if (sig.isOut()) {
......
......@@ -1246,8 +1246,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
private synchronized void addState(SpecificationState newState) {
newState.id = stateID;;
//newState.computeHash(blockValues);
newState.id = stateID;
//newState.computeHash(blockValues);
states.put(newState.getHash(blockValues), newState);
statesByID.put(newState.id, newState);
stateID ++;
......
......@@ -979,7 +979,7 @@ public class AVATAR2CPOSIX {
ret += actModified + ";" + CR;
} else {
TraceManager.addDev("Else");
String actModified = modifyMethodName (_block, (AvatarTerm) ((AvatarActionAssignment) act).getLeftHand ())
String actModified = modifyMethodName (_block, ((AvatarActionAssignment) act).getLeftHand ())
+ " = " + modifyMethodName (_block, ((AvatarActionAssignment) act).getRightHand ());
AvatarLeftHand leftHand = ((AvatarActionAssignment) act).getLeftHand ();
ret += actModified + ";" + CR;
......
......@@ -572,7 +572,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
continue;
visited.add (asme);
if (asme instanceof AvatarState && (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL || ((AvatarState) asme).isCheckable ())) {
if (asme instanceof AvatarState && (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL || asme.isCheckable ())) {
this.spec.addDeclaration (new ProVerifQueryEv (new ProVerifVar[] {}, "enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName()));
this.spec.addDeclaration (new ProVerifEvDecl ("enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName(), new String[] {}));
TraceManager.addDev("| event (enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName() + ")");
......@@ -792,7 +792,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
containsPublicKey = this.nameEquivalence.get (privateK);
// Let the public key
lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));;
lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));
// Make the public key public
tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm (first, null) + ");");
} else
......@@ -910,7 +910,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
// Let the public key
lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, PK_PK + "(" + privateKStr + ")"));;
lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, PK_PK + "(" + privateKStr + ")"));
// Make the public key public
tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + str + ");");
} else {
......
......@@ -1354,7 +1354,7 @@ public class AVATAR2UPPAAL {
// int i;
while(iterator.hasNext()) {
template = (UPPAALTemplate)(iterator.next());
template = iterator.next();
if (template.getNbOfTransitions() > 0) {
dec += template.getName() + "__" + id + " = " + template.getName() + "();\n";
if (id > 0) {
......
......@@ -11,26 +11,26 @@ interface Node {
/** This method is called after the node has been made the current
node. It indicates that child nodes can now be added to it. */
public void jjtOpen();
void jjtOpen();
/** This method is called after all the child nodes have been
added. */
public void jjtClose();
void jjtClose();
/** This pair of methods are used to inform the node of its
parent. */
public void jjtSetParent(Node n);
public Node jjtGetParent();
void jjtSetParent(Node n);
Node jjtGetParent();
/** This method tells the node to add its argument to the node's
list of children. */
public void jjtAddChild(Node n, int i);
void jjtAddChild(Node n, int i);
/** This method returns a child node. The children are numbered
from zero, left to right. */
public Node jjtGetChild(int i);
Node jjtGetChild(int i);
/** Return the number of children the node has. */
public int jjtGetNumChildren();
int jjtGetNumChildren();
}
/* JavaCC - OriginalChecksum=4ad84079284f044103e44453dfa3546c (do not edit this line) */
......@@ -201,7 +201,6 @@ public class TMLExprParser/*@bgen(jjtree)*/implements TMLExprParserTreeConstants
break;
default:
jj_la1[1] = jj_gen;
;
}
break;
case FIRST:
......@@ -219,7 +218,6 @@ public class TMLExprParser/*@bgen(jjtree)*/implements TMLExprParserTreeConstants
break;
default:
jj_la1[2] = jj_gen;
;
}
break;
case NATURAL_LITERAL:
......@@ -234,7 +232,6 @@ public class TMLExprParser/*@bgen(jjtree)*/implements TMLExprParserTreeConstants
break;
default:
jj_la1[3] = jj_gen;
;
}
break;
case IDENTIFIER:
......@@ -249,7 +246,6 @@ public class TMLExprParser/*@bgen(jjtree)*/implements TMLExprParserTreeConstants
break;
default:
jj_la1[4] = jj_gen;
;
}
break;
default:
......@@ -644,7 +640,6 @@ public class TMLExprParser/*@bgen(jjtree)*/implements TMLExprParserTreeConstants
break;
default:
jj_la1[12] = jj_gen;
;
}
} else if (jj_2_2(2000000)) {
LParen();
......@@ -658,7 +653,6 @@ public class TMLExprParser/*@bgen(jjtree)*/implements TMLExprParserTreeConstants
break;
default:
jj_la1[13] = jj_gen;
;
}
} else if (jj_2_3(2000000)) {
BooleanLiteral();
......@@ -670,7 +664,6 @@ public class TMLExprParser/*@bgen(jjtree)*/implements TMLExprParserTreeConstants
break;
default:
jj_la1[14] = jj_gen;
;
}