Pushing runtime to debug

TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs

@@ -3,11 +3,13 @@
 using Wrappers_Compile;
 using Simple.Constraints;
 using Simple.Constraints.Wrapped;
-using TypeConversion = Simple.Constraints.TypeConversion ;
+using TypeConversion = Simple.Constraints.TypeConversion;
 namespace simple.constraints.internaldafny.wrapped
 {
- public partial class __default {
- public static _IResult<types.ISimpleConstraintsClient, types._IError> WrappedSimpleConstraints(types._ISimpleConstraintsConfig config) {
+ public partial class __default
+ {
+ public static _IResult<types.ISimpleConstraintsClient, types._IError> WrappedSimpleConstraints(types._ISimpleConstraintsConfig config)
+ {
  var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_constraints__S23_SimpleConstraintsConfig(config);
  var impl = new SimpleConstraints(wrappedConfig);
  var wrappedClient = new SimpleConstraintsShim(impl);

TestModels/Constraints/runtimes/net/ImplementationFromDafny-cs.dtr

@@ -0,0 +1,7 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.SimpleConstraintsTypes]
+[options_by_module.AbstractSimpleConstraintsOperations]
+[options_by_module.AbstractSimpleConstraintsService]
+[options_by_module.SimpleConstraintsImpl]
+[options_by_module.SimpleConstraints]

TestModels/Constraints/runtimes/net/tests/TestsFromDafny-cs.dtr

@@ -0,0 +1,7 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.Helpers]
+[options_by_module.SimpleConstraintsImplTest]
+[options_by_module.WrappedAbstractSimpleConstraintsService]
+[options_by_module.WrappedSimpleConstraintsService]
+[options_by_module.WrappedSimpleConstraintsTest]

TestModels/Union/runtimes/java/.gitattributes

@@ -0,0 +1,9 @@
+#
+# https://help.github.com/articles/dealing-with-line-endings/
+#
+# Linux start script should use lf
+/gradlew text eol=lf
+
+# These are Windows script files and should use crlf
+*.bat text eol=crlf
+

TestModels/Union/runtimes/java/.gitignore

@@ -0,0 +1,5 @@
+# Ignore Gradle project-specific cache directory
+.gradle
+
+# Ignore Gradle build output directory
+build

TestModels/Union/runtimes/java/build.gradle.kts

@@ -0,0 +1,73 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+import java.io.File
+import java.io.FileInputStream
+import java.util.Properties
+
+tasks.wrapper {
+ gradleVersion = "7.6"
+}
+
+plugins {
+ `java-library`
+ `maven-publish`
+}
+
+var props = Properties().apply {
+ load(FileInputStream(File(rootProject.rootDir, "../../project.properties")))
+}
+var dafnyVersion = props.getProperty("dafnyVersion")
+
+group = "simple"
+version = "1.0-SNAPSHOT"
+description = "Constraints"
+
+java {
+ toolchain.languageVersion.set(JavaLanguageVersion.of(8))
+ sourceSets["main"].java {
+ srcDir("src/main/java")
+ srcDir("src/main/dafny-generated")
+ srcDir("src/main/smithy-generated")
+ }
+ sourceSets["test"].java {
+ srcDir("src/test/java")
+ srcDir("src/test/dafny-generated")
+ srcDir("src/test/smithy-generated")
+ }
+}
+
+repositories {
+ mavenCentral()
+ mavenLocal()
+}
+
+dependencies {
+ implementation("org.dafny:DafnyRuntime:${dafnyVersion}")
+ implementation("software.amazon.smithy.dafny:conversion:0.1")
+ implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
+ testImplementation("org.testng:testng:7.5")
+}
+
+publishing {
+ publications.create<MavenPublication>("maven") {
+ groupId = "simple"
+ artifactId = "Constraints"
+ from(components["java"])
+ }
+ repositories { mavenLocal() }
+}
+
+tasks.withType<JavaCompile>() {
+ options.encoding = "UTF-8"
+}
+
+tasks {
+ register("runTests", JavaExec::class.java) {
+ mainClass.set("TestsFromDafny")
+ classpath = sourceSets["test"].runtimeClasspath
+ }
+}
+
+tasks.named<Test>("test") {
+ useTestNG()
+}

TestModels/Union/runtimes/java/lib/build.gradle.kts

@@ -0,0 +1,41 @@
+/*
+ * This file was generated by the Gradle 'init' task.
+ *
+ * This generated file contains a sample Java library project to get you started.
+ * For more details on building Java & JVM projects, please refer to https://docs.gradle.org/8.7/userguide/building_java_projects.html in the Gradle documentation.
+ */
+
+plugins {
+ // Apply the java-library plugin for API and implementation separation.
+ `java-library`
+}
+
+repositories {
+ // Use Maven Central for resolving dependencies.
+ mavenCentral()
+}
+
+dependencies {
+ // Use JUnit Jupiter for testing.
+ testImplementation(libs.junit.jupiter)
+
+ testRuntimeOnly("org.junit.platform:junit-platform-launcher")
+
+ // This dependency is exported to consumers, that is to say found on their compile classpath.
+ api(libs.commons.math3)
+
+ // This dependency is used internally, and not exposed to consumers on their own compile classpath.
+ implementation(libs.guava)
+}
+
+// Apply a specific Java toolchain to ease working on different environments.
+java {
+ toolchain {
+ languageVersion.set(JavaLanguageVersion.of(17))
+ }
+}
+
+tasks.named<Test>("test") {
+ // Use JUnit Platform for unit tests.
+ useJUnitPlatform()
+}

TestModels/Union/runtimes/java/lib/src/main/java/org/example/Library.java

@@ -0,0 +1,10 @@
+/*
+ * This source file was generated by the Gradle 'init' task
+ */
+package org.example;
+
+public class Library {
+ public boolean someLibraryMethod() {
+ return true;
+ }
+}

TestModels/Union/runtimes/java/lib/src/test/java/org/example/LibraryTest.java

@@ -0,0 +1,14 @@
+/*
+ * This source file was generated by the Gradle 'init' task
+ */
+package org.example;
+
+import org.junit.jupiter.api.Test;
+import static org.junit.jupiter.api.Assertions.*;
+
+class LibraryTest {
+ @Test void someLibraryMethodReturnsTrue() {
+ Library classUnderTest = new Library();
+ assertTrue(classUnderTest.someLibraryMethod(), "someLibraryMethod should return 'true'");
+ }
+}

TestModels/Union/runtimes/java/settings.gradle.kts

@@ -0,0 +1,14 @@
+/*
+ * This file was generated by the Gradle 'init' task.
+ *
+ * The settings file is used to specify which projects to include in your build.
+ * For more detailed information on multi-project builds, please refer to https://docs.gradle.org/8.7/userguide/multi_project_builds.html in the Gradle documentation.
+ */
+
+plugins {
+ // Apply the foojay-resolver plugin to allow automatic download of JDKs
+ id("org.gradle.toolchains.foojay-resolver-convention") version "0.8.0"
+}
+
+rootProject.name = "java"
+include("lib")

TestModels/Union/runtimes/net/Extern/WrappedSimpleUnionService.cs

@@ -6,8 +6,10 @@
 using TypeConversion = Simple.Union.TypeConversion;
 namespace simple.union.internaldafny.wrapped
 {
- public partial class __default {
- public static _IResult<types.ISimpleUnionClient, types._IError> WrappedSimpleUnion(types._ISimpleUnionConfig config) {
+ public partial class __default
+ {
+ public static _IResult<types.ISimpleUnionClient, types._IError> WrappedSimpleUnion(types._ISimpleUnionConfig config)
+ {
  var wrappedConfig = TypeConversion.FromDafny_N6_simple__N5_union__S17_SimpleUnionConfig(config);
  var impl = new SimpleUnion(wrappedConfig);
  var wrappedClient = new SimpleUnionShim(impl);

TestModels/Union/runtimes/net/ImplementationFromDafny-cs.dtr

@@ -0,0 +1,7 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.SimpleUnionTypes]
+[options_by_module.AbstractSimpleUnionOperations]
+[options_by_module.AbstractSimpleUnionService]
+[options_by_module.SimpleUnionImpl]
+[options_by_module.SimpleUnion]

TestModels/Union/runtimes/net/tests/TestsFromDafny-cs.dtr

@@ -0,0 +1,6 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.SimpleUnionImplTest]
+[options_by_module.WrappedAbstractSimpleUnionService]
+[options_by_module.WrappedSimpleUnionService]
+[options_by_module.WrappedSimpleUnionTest]