make sure globals in pre/postconditions are defined

UQ-PAC · Oct 9, 2023 · 0fd4735 · 0fd4735
1 parent 2e3db86
commit 0fd4735
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/main/scala/translating/IRToBoogie.scala b/src/main/scala/translating/IRToBoogie.scala
@@ -32,7 +32,8 @@ class IRToBoogie(var program: Program, var spec: Specification) {
   def translate: BProgram = {
     val procedures = program.procedures.map(f => translateProcedure(f))
     val defaultGlobals = List(BVarDecl(mem), BVarDecl(Gamma_mem))
-    val globalDecls = (procedures.flatMap(p => p.globals).map(b => BVarDecl(b)) ++ defaultGlobals).distinct.sorted.toList
+    val globalVars = procedures.flatMap(p => p.globals ++ p.freeRequires.flatMap(_.globals) ++ p.freeEnsures.flatMap(_.globals) ++ p.ensures.flatMap(_.globals) ++ p.requires.flatMap(_.globals))
+    val globalDecls = (globalVars.map(b => BVarDecl(b)) ++ defaultGlobals).distinct.sorted.toList
 
     val globalConsts: List[BConstAxiomPair] = globals.map(g => BConstAxiomPair(BVarDecl(g.toAddrVar), g.toAxiom)).toList.sorted