Added Attributes to CfgStatement

boogie-org · Jun 29, 2014 · 5119802 · 5119802
1 parent 8bea8d7
commit 5119802
Show file tree

Hide file tree

Showing 5 changed files with 33 additions and 2 deletions.
diff --git a/boogieamp/dist/boogieamp.jar b/boogieamp/dist/boogieamp.jar
diff --git a/boogieamp/src/boogie/controlflow/DefaultControlFlowFactory.java b/boogieamp/src/boogie/controlflow/DefaultControlFlowFactory.java
@@ -205,9 +205,10 @@ private BasicBlock constructCfg(Statement s, BasicBlock b) {
 			Log.error("Statement " + s + " is unreachable");
 			return null;
 		}
-		if (s instanceof AssertStatement) {
+		if (s instanceof AssertStatement) {			
 			CfgAssertStatement asrt = new CfgAssertStatement(
 					s.getLocation(),
+					s.getAttributes(),
 					expression2CfgExpression(((AssertStatement) s).getFormula()));
 			this.astStatementMap.put(asrt, s);
 			b.addStatement(asrt);
@@ -280,6 +281,7 @@ private BasicBlock constructCfg(Statement s, BasicBlock b) {
 		} else if (s instanceof AssumeStatement) {
 			CfgAssumeStatement assm = new CfgAssumeStatement(
 					s.getLocation(),
+					s.getAttributes(),
 					expression2CfgExpression(((AssumeStatement) s).getFormula()));
 			b.addStatement(assm);			
 			this.astStatementMap.put(assm, s);

diff --git a/boogieamp/src/boogie/controlflow/statement/CfgAssertStatement.java b/boogieamp/src/boogie/controlflow/statement/CfgAssertStatement.java
@@ -19,6 +19,7 @@
 
 package boogie.controlflow.statement;
 
+import boogie.ast.Attribute;
 import boogie.controlflow.expression.CfgExpression;
 import boogie.location.ILocation;
 
@@ -30,6 +31,11 @@ public class CfgAssertStatement extends CfgStatement {
 
 	private CfgExpression condition;
 
+	public CfgAssertStatement(ILocation loc, Attribute[] attributes, CfgExpression cond) {
+		super(loc, attributes);
+		this.condition = cond;
+	}	
+
 	public CfgAssertStatement(ILocation loc, CfgExpression cond) {
 		super(loc);
 		this.condition = cond;

diff --git a/boogieamp/src/boogie/controlflow/statement/CfgAssumeStatement.java b/boogieamp/src/boogie/controlflow/statement/CfgAssumeStatement.java
@@ -19,6 +19,7 @@
 
 package boogie.controlflow.statement;
 
+import boogie.ast.Attribute;
 import boogie.controlflow.expression.CfgExpression;
 import boogie.location.ILocation;
 
@@ -30,6 +31,12 @@ public class CfgAssumeStatement extends CfgStatement {
 
 	private CfgExpression condition;
 
+	public CfgAssumeStatement(ILocation loc, Attribute[] attributes, CfgExpression cond) {
+		super(loc, attributes);
+		this.condition = cond;
+	}
+
+
 	public CfgAssumeStatement(ILocation loc, CfgExpression cond) {
 		super(loc);
 		this.condition = cond;

diff --git a/boogieamp/src/boogie/controlflow/statement/CfgStatement.java b/boogieamp/src/boogie/controlflow/statement/CfgStatement.java
@@ -19,6 +19,7 @@
 
 package boogie.controlflow.statement;
 
+import boogie.ast.Attribute;
 import boogie.location.ILocation;
 
 /**
@@ -28,15 +29,30 @@
 public abstract class CfgStatement {
 
 	private ILocation location;
+	private Attribute[] attributes;
 
 	public CfgStatement(ILocation loc) {
 		this.location = loc;
 	}
 
+	public CfgStatement(ILocation loc, Attribute[] attributes) {
+		this.location = loc;
+		this.attributes = attributes;
+	}
+
+
 	public ILocation getLocation() {
 		return this.location;
 	}
 
 	@Override
-	public abstract CfgStatement clone(); 
+	public abstract CfgStatement clone();
+
+	/**
+	 * @return the attributes
+	 */
+	public Attribute[] getAttributes() {
+		return attributes;
+	}
+
 }