remove extern axioms

UQ-PAC · Oct 31, 2023 · 6ed9c42 · 6ed9c42
1 parent 68c0336
commit 6ed9c42
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/src/main/scala/boogie/BCmd.scala b/src/main/scala/boogie/BCmd.scala
@@ -24,7 +24,7 @@ sealed trait BCmd() extends BCmdOrBlock {
   def attributes: List[(String, String)]
 
   val attrString: String = if (attributes.nonEmpty) then {
-    attributes.map(a => s"{${a._1} ${a._2}}").mkString(" ")
+    (attributes.map(a => s"{${a._1} ${a._2}}").mkString(" ")) + " "
   } else {
     ""
   }

diff --git a/src/main/scala/boogie/BProgram.scala b/src/main/scala/boogie/BProgram.scala
@@ -9,7 +9,7 @@ trait BDeclaration() {
   def toBoogie: List[String] = List(toString)
 
   val attrString: String = if (attributes.nonEmpty) then {
-    attributes.map(a => s"{${a._1} ${a._2}}").mkString(" ")
+    attributes.map(a => s"{${a._1} ${a._2}}").mkString(" ") + " "
   } else {
     ""
   }

diff --git a/src/main/scala/specification/Specification.scala b/src/main/scala/specification/Specification.scala
@@ -23,7 +23,7 @@ case class SpecGlobal(name: String, override val size: Int, arraySize: Option[In
   override val toAddrVar: BVar = BVariable("$" + s"${name}_addr", BitVecBType(64), Scope.Const)
   override val toOldVar: BVar = BVariable(s"${name}_old", BitVecBType(size), Scope.Local)
   override val toOldGamma: BVar = BVariable(s"Gamma_${name}_old", BoolBType, Scope.Local)
-  val toAxiom: BAxiom = BAxiom(BinaryBExpr(BoolEQ, toAddrVar, BitVecBLiteral(address, 64)), List((":extern", "")))
+  val toAxiom: BAxiom = BAxiom(BinaryBExpr(BoolEQ, toAddrVar, BitVecBLiteral(address, 64)), List.empty)
   override def resolveSpec: BMemoryLoad = BMemoryLoad(
     BMapVar("mem", MapBType(BitVecBType(64), BitVecBType(8)), Scope.Global),
     toAddrVar,