From ced42412ead32f213c5e256359ee66dd567a2aec Mon Sep 17 00:00:00 2001 From: "Felix A. Wolf" Date: Fri, 23 Feb 2024 18:59:48 +0100 Subject: [PATCH] Fix #713 --- .../encodings/closures/ClosureSpecsEncoder.scala | 3 ++- src/test/resources/regressions/issues/000713.gobra | 9 +++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/regressions/issues/000713.gobra diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala index 3b12c07bc..1719ca9c2 100644 --- a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala +++ b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala @@ -208,7 +208,8 @@ protected class ClosureSpecsEncoder { val result = in.Parameter.Out(Names.closureArg, genericFuncType)(info) val satisfiesSpec = in.ExprAssertion(in.ClosureImplements(result, in.ClosureSpec(func, Map.empty)(info))(info))(info) val (args, captAssertions) = capturedArgsAndAssertions(ctx)(result, captured(ctx)(func), info) - val getter = in.PureFunction(proxy, args, Vector(result), Vector.empty, Vector(satisfiesSpec) ++ captAssertions, Vector.empty, None, false)(memberOrLit(ctx)(func).info) + val notNil = in.ExprAssertion(in.UneqCmp(result, in.NilLit(genericFuncType)(info))(info))(info) + val getter = in.PureFunction(proxy, args, Vector(result), Vector.empty, Vector(satisfiesSpec) ++ captAssertions :+ notNil, Vector.empty, None, false)(memberOrLit(ctx)(func).info) ctx.defaultEncoding.pureFunction(getter)(ctx) } diff --git a/src/test/resources/regressions/issues/000713.gobra b/src/test/resources/regressions/issues/000713.gobra new file mode 100644 index 000000000..601f9dc1c --- /dev/null +++ b/src/test/resources/regressions/issues/000713.gobra @@ -0,0 +1,9 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue000713 + +func foo() { + f := func g() {} + assert f != nil +} \ No newline at end of file