Merge branch 'master' into highprecision

nickbattle · Nov 28, 2023 · 3e95f0c · 3e95f0c
2 parents 04df687 + 4db600d
commit 3e95f0c
Show file tree

Hide file tree

Showing 17 changed files with 22 additions and 3 deletions.
diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QCRunCommand.java
@@ -46,7 +46,7 @@ public QCRunCommand(String line)
 	{
 		super(line);
 
-		if (!argv[0].equals("qcrun"))
+		if (!argv[0].equals("qcrun") && !argv[0].equals("qr"))
 		{
 			throw new IllegalArgumentException(USAGE);
 		}

diff --git a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java
@@ -76,6 +76,7 @@ public AnalysisCommand getCommand(String line)
 				return new QuickCheckLSPCommand(line);
 
 			case "qcrun":
+			case "qr":
 				return new QCRunLSPCommand(line);
 		}
 

diff --git a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckPlugin.java b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckPlugin.java
@@ -63,6 +63,7 @@ public AnalysisCommand getCommand(String line)
 				return new QuickCheckCommand(line);
 
 			case "qcrun":
+			case "qr":
 				return new QCRunCommand(line);
 		}
 

diff --git a/lsp/src/main/java/workspace/LSPWorkspaceManager.java b/lsp/src/main/java/workspace/LSPWorkspaceManager.java
@@ -38,6 +38,7 @@
 import java.nio.file.Paths;
 import java.nio.file.attribute.BasicFileAttributes;
 import java.nio.file.attribute.FileTime;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.HashMap;
 import java.util.HashSet;
@@ -421,6 +422,7 @@ private void loadProjectFiles(File root) throws IOException
 	{
 		FilenameFilter filter = getFilenameFilter();
 		File[] files = root.listFiles();
+		Arrays.sort(files);		// Predictable order
 		List<File> ignored = new Vector<File>();
 
 		for (File file: files)

diff --git a/stdlib/src/main/resources/CSV.vdmpp b/stdlib/src/main/resources/CSV.vdmpp
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class CSV
 
 --  Overture STANDARD LIBRARY: INPUT/OUTPUT

diff --git a/stdlib/src/main/resources/CSV.vdmrt b/stdlib/src/main/resources/CSV.vdmrt
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class CSV
 
 --  Overture STANDARD LIBRARY: INPUT/OUTPUT

diff --git a/stdlib/src/main/resources/CSV.vdmsl b/stdlib/src/main/resources/CSV.vdmsl
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this module
 module CSV
 -- 	Overture STANDARD LIBRARY: INPUT/OUTPUT
 --      --------------------------------------------

diff --git a/stdlib/src/main/resources/IO.vdmpp b/stdlib/src/main/resources/IO.vdmpp
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class IO
 
 -- 	VDMTools STANDARD LIBRARY: INPUT/OUTPUT

diff --git a/stdlib/src/main/resources/IO.vdmrt b/stdlib/src/main/resources/IO.vdmrt
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class IO
 
 -- 	VDMTools STANDARD LIBRARY: INPUT/OUTPUT

diff --git a/stdlib/src/main/resources/IO.vdmsl b/stdlib/src/main/resources/IO.vdmsl
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this module
 module IO
 exports all
 definitions

diff --git a/stdlib/src/main/resources/MATH.vdmpp b/stdlib/src/main/resources/MATH.vdmpp
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class MATH
 
 -- 	VDMTools STANDARD LIBRARY: MATH

diff --git a/stdlib/src/main/resources/MATH.vdmrt b/stdlib/src/main/resources/MATH.vdmrt
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class MATH
 
 -- 	VDMTools STANDARD LIBRARY: MATH

diff --git a/stdlib/src/main/resources/MATH.vdmsl b/stdlib/src/main/resources/MATH.vdmsl
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this module
 module MATH
 exports all
 definitions
@@ -56,7 +57,7 @@ definitions
     sqrt:real -> real
     sqrt(a) ==
     is not yet specified
-    ;--pre a >= 0;
+    pre a >= 0;
 
     pi_f:() +> real
     pi_f () ==

diff --git a/stdlib/src/main/resources/VDMUtil.vdmpp b/stdlib/src/main/resources/VDMUtil.vdmpp
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class VDMUtil
 
 -- 	VDMTools STANDARD LIBRARY: MiscUtils

diff --git a/stdlib/src/main/resources/VDMUtil.vdmrt b/stdlib/src/main/resources/VDMUtil.vdmrt
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this class
 class VDMUtil
 
 -- 	VDMTools STANDARD LIBRARY: MiscUtils

diff --git a/stdlib/src/main/resources/VDMUtil.vdmsl b/stdlib/src/main/resources/VDMUtil.vdmsl
@@ -1,3 +1,4 @@
+-- @NoPOG - do not generate obligations for this module
 module VDMUtil
 
 -- 	VDMTools STANDARD LIBRARY: MiscUtils

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/Lifecycle.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/Lifecycle.java
@@ -352,7 +352,10 @@ protected void findFiles()
 
 			if (file.isDirectory())
 			{
-				for (File subfile: file.listFiles(Settings.dialect.getFilter()))
+				File[] list = file.listFiles(Settings.dialect.getFilter());
+				Arrays.sort(list);	// Predictable order
+
+				for (File subfile: list)
 				{
 					if (subfile.isFile())
 					{