tests run

TestModels/Aggregate/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/Constraints/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/Constructor/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/Errors/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/Extendable/runtimes/python/src/simple_extendable_resources/extern/native_resource.py

@@ -0,0 +1,52 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+from simple_extendable_resources_internaldafny_types import (
+  IExtendableResource as DafnyIExtendableResource
+)
+import ExtendableResource
+from simple_extendable_resources.smithygenerated.models import IExtendableResource
+import simple_extendable_resources_internaldafny_nativeresourcefactory
+
+class NativeResource(IExtendableResource):
+  _impl: DafnyIExtendableResource
+
+  def __init__(self, _impl):
+    self._impl = _impl
+
+  def GetExtendableResourceData(self, nativeInput):
+    print("nativeInput")
+    print(nativeInput)
+    a = self._impl.GetExtendableResourceData(nativeInput)
+    print("a")
+    print(a)
+    return a
+
+  def AlwaysModeledError(self, nativeInput):
+    print("AlwaysModeledError")
+    print(nativeInput)
+    return self._impl.AlwaysModeledError(nativeInput)
+
+  def AlwaysMultipleErrors(self, nativeInput):
+    return self._impl.AlwaysMultipleErrors(nativeInput)
+
+  def AlwaysOpaqueError(self, nativeInput):
+    if nativeInput.value == None:
+      raise Exception("Python Hard Coded Exception")
+    return self._impl.AlwaysOpaqueError(nativeInput)
+
+class NativeResourceFactory:
+
+  @staticmethod
+  def DafnyFactory():
+    dafny_resource = ExtendableResource.ExtendableResource()
+    dafny_resource.ctor__()
+    native_resource = NativeResource(dafny_resource)
+
+    # to_dafny
+    return native_resource
+
+
+simple_extendable_resources_internaldafny_nativeresourcefactory.default__ = NativeResourceFactory
+
+DafnyFactory = NativeResourceFactory

TestModels/Extendable/runtimes/python/src/simple_extendable_resources/extern/wrapped_simple_extendable_resources.py

@@ -4,11 +4,12 @@
 import simple_extendable_resources_internaldafny_wrapped
 from simple_extendable_resources.smithygenerated.client import SimpleExtendableResources
 from simple_extendable_resources.smithygenerated.shim import SimpleExtendableResourcesShim
+from simple_extendable_resources.smithygenerated.config import dafny_config_to_smithy_config
 import Wrappers
 
 @staticmethod
 def WrappedSimpleExtendableResources(config):
-    wrapped_config = config
+    wrapped_config = dafny_config_to_smithy_config(config)
     impl = SimpleExtendableResources(wrapped_config)
     wrapped_client = SimpleExtendableResourcesShim(impl)
     return Wrappers.Result_Success(wrapped_client)

TestModels/Extendable/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -14,11 +14,12 @@
 # This is not generated; these must be manually added.
 
 from simple_extendable_resources.extern import wrapped_simple_extendable_resources
+from simple_extendable_resources.extern import native_resource
 
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/Refinement/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/Resource/runtimes/python/src/simple_resources/extern/wrapped_simple_resources.py

@@ -4,11 +4,12 @@
 import simple_resources_internaldafny_wrapped
 from simple_resources.smithygenerated.client import SimpleResources
 from simple_resources.smithygenerated.shim import SimpleResourcesShim
+from simple_resources.smithygenerated.config import dafny_config_to_smithy_config
 import Wrappers
 
 @staticmethod
 def WrappedSimpleResources(config):
-    wrapped_config = config
+    wrapped_config = dafny_config_to_smithy_config(config)
     impl = SimpleResources(wrapped_config)
     wrapped_client = SimpleResourcesShim(impl)
     return Wrappers.Result_Success(wrapped_client)

TestModels/Resource/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/Resource/runtimes/python/tox.ini

@@ -10,4 +10,4 @@ commands_pre =
     poetry lock
     poetry install
 commands =
-    poetry run pytest test/ --import-mode importlib
+    poetry run pytest test/ -s -v --import-mode importlib

TestModels/SharedMakefile.mk

@@ -428,12 +428,13 @@ _comment_out_import_module_python:
 	# For a Dafny-generated module X, comment out `import module_`
 	# This import results in circular dependencies
 	find runtimes/python/src/$(PYTHON_MODULE_NAME)/dafnygenerated -type f -exec sed -i $(SED_PARAMETER) '/import module\_/s/^/# /g' {} \;
-	find runtimes/python/test/dafnygenerated -type f -exec sed -i $(SED_PARAMETER) '/import module\_/s/^/# /g' {} \;
+	rm runtimes/python/src/$(PYTHON_MODULE_NAME)/dafnygenerated/module_.py
+#	find runtimes/python/test/dafnygenerated -type f -exec sed -i $(SED_PARAMETER) '/import module\_/s/^/# /g' {} \;
 
 transpile_dependencies_python: LANG=python
 transpile_dependencies_python: transpile_dependencies
 
 test_python:
-	tox -c runtimes/python
+	tox -c runtimes/python --verbose
 
 clean: _clean

TestModels/SimpleTypes/SimpleBlob/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/SimpleTypes/SimpleBoolean/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/SimpleTypes/SimpleDouble/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/SimpleTypes/SimpleEnum/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/SimpleTypes/SimpleInteger/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/SimpleTypes/SimpleLong/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/SimpleTypes/SimpleString/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -18,7 +18,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]

TestModels/dafny-dependencies/StandardLibrary/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -16,7 +16,7 @@
 # End import modules required for Dafny-generated tests
 
 def test_dafny():
-  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafny/**/", "*.py"), recursive=True)
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/dafnygenerated/", "*.py"), recursive=True)
   for f in dafny_modules:
     if isfile(f) and f.endswith('test.py'):
       fname = str(f).split("/")[-1].split(".")[0]