From 04e9b2d2da2ba4a64b1fc1e5c3e2a9722c50887a Mon Sep 17 00:00:00 2001 From: Shuvendu Lahiri Date: Sun, 12 Apr 2020 21:43:57 -0700 Subject: [PATCH] fix for crash --- Sources/SolToBoogie/ProcedureTranslator.cs | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/Sources/SolToBoogie/ProcedureTranslator.cs b/Sources/SolToBoogie/ProcedureTranslator.cs index d5cd1d1c..6bb1500a 100644 --- a/Sources/SolToBoogie/ProcedureTranslator.cs +++ b/Sources/SolToBoogie/ProcedureTranslator.cs @@ -378,17 +378,18 @@ public override bool Visit(FunctionDefinition node) for (int i = 0; i < node.Modifiers.Count; ++i) { var outVars = new List(); - // local variables declared in the prelude of a modifier (before _ ) becomes out variables and then in parameters of postlude - foreach (var localVar in context.ModifierToPreludeLocalVars[node.Modifiers[i].ModifierName.ToString()]) - { - var outVar = new BoogieLocalVariable(new BoogieTypedIdent("__mod_out_" + localVar.Name, localVar.TypedIdent.Type)); - boogieToLocalVarsMap[currentBoogieProc].Add(outVar); - outVars.Add(new BoogieIdentifierExpr(outVar.Name)); - } - + // insert call to modifier prelude if (context.ModifierToBoogiePreImpl.ContainsKey(node.Modifiers[i].ModifierName.Name)) { + // local variables declared in the prelude of a modifier (before _ ) becomes out variables and then in parameters of postlude + foreach (var localVar in context.ModifierToPreludeLocalVars[node.Modifiers[i].ModifierName.ToString()]) + { + var outVar = new BoogieLocalVariable(new BoogieTypedIdent("__mod_out_" + localVar.Name, localVar.TypedIdent.Type)); + boogieToLocalVarsMap[currentBoogieProc].Add(outVar); + outVars.Add(new BoogieIdentifierExpr(outVar.Name)); + } + List arguments = TransUtils.GetDefaultArguments(); if (node.Modifiers[i].Arguments != null) arguments.AddRange(node.Modifiers[i].Arguments.ConvertAll(TranslateExpr));