From d007442b13fdfbba25ff085974fe9ddd72b2f6e8 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Mon, 11 Dec 2023 16:08:41 -0800 Subject: [PATCH] fix --- TestModels/ExternV2/src/IndexDotNamespaced.dfy | 2 ++ TestModels/ExternV2/src/IndexUnderscoreNamespaced.dfy | 2 ++ TestModels/ExternV2/test/WrappedTestUnderscoreNamespaced.dfy | 4 +++- 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/TestModels/ExternV2/src/IndexDotNamespaced.dfy b/TestModels/ExternV2/src/IndexDotNamespaced.dfy index be5c9fb0c..f7968cbd8 100644 --- a/TestModels/ExternV2/src/IndexDotNamespaced.dfy +++ b/TestModels/ExternV2/src/IndexDotNamespaced.dfy @@ -1,3 +1,5 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 include "Index.dfy" module {:extern "simple.dafnyexternv2.internaldafny"} UnderscoreNamespacedSimpleExternV2 replaces SimpleExternV2 {} \ No newline at end of file diff --git a/TestModels/ExternV2/src/IndexUnderscoreNamespaced.dfy b/TestModels/ExternV2/src/IndexUnderscoreNamespaced.dfy index de8c39600..724615e21 100644 --- a/TestModels/ExternV2/src/IndexUnderscoreNamespaced.dfy +++ b/TestModels/ExternV2/src/IndexUnderscoreNamespaced.dfy @@ -1,3 +1,5 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 include "Index.dfy" // TODO: Python will use this syntax. diff --git a/TestModels/ExternV2/test/WrappedTestUnderscoreNamespaced.dfy b/TestModels/ExternV2/test/WrappedTestUnderscoreNamespaced.dfy index 746e6b874..14293bdc1 100644 --- a/TestModels/ExternV2/test/WrappedTestUnderscoreNamespaced.dfy +++ b/TestModels/ExternV2/test/WrappedTestUnderscoreNamespaced.dfy @@ -5,4 +5,6 @@ include "SimpleExternV2ImplTest.dfy" include "WrappedSimpleExternV2ImplTest.dfy" // TOOD: Python will use this syntax. -module {:extern "simple_dafnyexternv2_internaldafny_wrapped"} UnderscoreNamespacedWrappedSimpleExternV2Service replaces WrappedSimpleExternV2Service {} +module {:extern "simple_dafnyexternv2_internaldafny_wrapped"} UnderscoreNamespacedWrappedSimpleExternV2Service replaces WrappedSimpleExternV2Service { + +}