Support non-deterministic statements #108

overturetool · Oct 19, 2017 · 9045250 · 9045250
1 parent ac2f061
commit 9045250
Show file tree

Hide file tree

Showing 4 changed files with 41 additions and 0 deletions.
diff --git a/core/vdm2c/src/main/java/org/overture/codegen/vdm2c/CTransSeries.java b/core/vdm2c/src/main/java/org/overture/codegen/vdm2c/CTransSeries.java
@@ -24,6 +24,7 @@
 import org.overture.codegen.trans.patterns.PatternTrans;
 import org.overture.codegen.trans.patterns.PatternVarPrefixes;
 import org.overture.codegen.trans.quantifier.CounterData;
+import org.overture.codegen.trans.uniontypes.NonDetStmTrans;
 import org.overture.codegen.vdm2c.transformations.*;
 
 import java.util.LinkedList;
@@ -70,6 +71,7 @@ public List<DepthFirstAnalysisAdaptor> consAnalyses()
 		// Construct the transformations
 		transformations.add(new RecTypeToClassTypeTrans(transAssistant));
 		transformations.add(new FuncTrans(transAssistant));
+		transformations.add(new NonDetStmTrans(transAssistant));
 		transformations.add(new PrePostTrans(transAssistant.getInfo()));
 		transformations.add(new FieldInitializerExtractorTrans(transAssistant));
 		transformations.add(new RemoveRTConstructs(transAssistant));

diff --git a/core/vdm2c/src/test/java/org/overture/codegen/vdm2c/NativeTests.java b/core/vdm2c/src/test/java/org/overture/codegen/vdm2c/NativeTests.java
@@ -186,4 +186,12 @@ public void ExpressionIs() throws IOException, InterruptedException,
 		generate(getPath("expressions/ExpressionIs.vdmrt"));
 		compileAndTest(getTestCppFile("is/ExpressionsIs_Tests.cpp"));
 	}
+
+	@Test
+	public void NonDet() throws IOException, InterruptedException,
+			CMakeGenerateException
+	{
+		generate(getPath("nondet/NonDet.vdmrt"));
+		compileAndTest(getTestCppFile("nondet/NonDet_Tests.cpp"));
+	}
 }
diff --git a/core/vdm2c/src/test/resources/native/nondet/NonDet_Tests.cpp b/core/vdm2c/src/test/resources/native/nondet/NonDet_Tests.cpp
@@ -0,0 +1,22 @@
+
+#include "gtest/gtest.h"
+#include "TestFlowFunctions.h"
+
+extern "C"
+{
+#include "Vdm.h"
+#include <stdio.h>
+#include "NonDet.h"
+
+}
+
+#define CHECK(methodId) TVP c = _Z6NonDetEV(NULL);\
+TVP res=CALL_FUNC(NonDet,NonDet,c,methodId);\
+EXPECT_EQ (true,res->value.boolVal);\
+vdmFree(res);\
+vdmFree(c);
+
+TEST_F(TestFlowFunctions, nonDet)
+{
+  CHECK(CLASS_NonDet__Z9nonDetStmEV);
+}
diff --git a/core/vdm2c/src/test/resources/vdmrt/nondet/NonDet.vdmrt b/core/vdm2c/src/test/resources/vdmrt/nondet/NonDet.vdmrt
@@ -0,0 +1,9 @@
+class NonDet
+
+operations
+
+public nonDetStm : () ==> bool
+nonDetStm () ==
+  || (return true, return true);
+
+end NonDet