From 0fd473599e18b148cfa5dda6b2d7edc48e1afe04 Mon Sep 17 00:00:00 2001 From: l-kent Date: Mon, 9 Oct 2023 15:33:20 +1000 Subject: [PATCH] make sure globals in pre/postconditions are defined --- src/main/scala/translating/IRToBoogie.scala | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/translating/IRToBoogie.scala b/src/main/scala/translating/IRToBoogie.scala index 4c06ae490..597211ee4 100644 --- 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