Get basic testing working

robin-aws · Oct 13, 2023 · 578cdfa · 578cdfa
1 parent c03d80b
commit 578cdfa
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 8 deletions.
diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs
@@ -34,7 +34,7 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
     CancellationToken cancellationToken) {
     var options = errorReporter.Options;
     var builtIns = new SystemModuleManager(options);
-    var defaultModule = new DefaultModuleDefinition(files.Where(f => !f.IsPreverified).Select(f => f.Uri).ToList());
+    var defaultModule = new DefaultModuleDefinition(files.Select(f => f.Uri).ToList());
 
     var verifiedRoots = files.Where(df => df.IsPreverified).Select(df => df.Uri).ToHashSet();
     var compiledRoots = files.Where(df => df.IsPrecompiled).Select(df => df.Uri).ToHashSet();

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -241,6 +241,8 @@ public enum DefaultFunctionOpacityOptions {
 `opaque` means functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.".TrimStart()) {
   };
 
+  public static readonly Option<bool> AllowStdLibs = new("--allow-standard-libraries");
+
   static CommonOptionBag() {
     QuantifierSyntax = QuantifierSyntax.FromAmong("3", "4");
     DafnyOptions.RegisterLegacyBinding(JsonDiagnostics, (options, value) => {

diff --git a/Source/DafnyStandardLibraries/Makefile b/Source/DafnyStandardLibraries/Makefile
@@ -6,7 +6,12 @@ build:
 	$(DAFNY) build -t:lib src/dfyconfig.toml --output:build/stdlib.doo
 
 test:
-	$(DAFNY) test examples/dfyconfig.toml
+	$(DAFNY) test -t:cs examples/dfyconfig.toml
+	$(DAFNY) test -t:java examples/dfyconfig.toml
+	$(DAFNY) test -t:go examples/dfyconfig.toml
+	$(DAFNY) test -t:py examples/dfyconfig.toml
+	$(DAFNY) test -t:js examples/dfyconfig.toml
+#	$(DAFNY) test -t:rs examples/dfyconfig.toml
 
 clean:
 	rm -rf build
diff --git a/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy b/Source/DafnyStandardLibraries/examples/WrappersExamples.dfy
@@ -1,5 +1,5 @@
 module {:options "--function-syntax:4"} Demo {
-  import opened Dafny.Wrappers
+  import opened DafnyStdLibs.Wrappers
 
   // ------ Demo for Option ----------------------------
   // We use Option when we don't need to pass around a reason for the failure,

diff --git a/Source/DafnyStandardLibraries/examples/dfyconfig.toml b/Source/DafnyStandardLibraries/examples/dfyconfig.toml
@@ -1,4 +1,2 @@
 
-
-[options]
-library = "build/stdlib.doo"
+includes = ["**/*.dfy", "../build/stdlib.doo"]
diff --git a/Source/DafnyStandardLibraries/src/dafny/Wrappers.dfy b/Source/DafnyStandardLibraries/src/dafny/Wrappers.dfy
@@ -14,7 +14,7 @@ All three of these may be used with `:-` as Dafny failure-compatible types
 The module also defines two forms of `Need`, that check the truth of a predicate and
 return a failure value if false.
  */
-module {:options "--function-syntax:4"} Dafny.Wrappers {
+module {:options "--function-syntax:4"} DafnyStdLibs.Wrappers {
 
   /** This datatype is the conventional Some/None datatype that is often used
       in place of a reference or null.
@@ -210,7 +210,7 @@ module {:options "--function-syntax:4"} Dafny.Wrappers {
   /** In verification, this method functions as an `assert` of the given condition;
       at run-time functions as an `expect`. The arguments may not be ghost.
    */
-  method AssertAndExpect(condition: bool, maybeMsg: Option<string> := None)
+  method AssertAndExpect<T>(condition: bool, maybeMsg: Option<T> := None)
     requires condition
   {
     match maybeMsg {