Skip to content

Commit

Permalink
Testing in-place sequence update.
Browse files Browse the repository at this point in the history
  • Loading branch information
Victor Bandur committed Nov 18, 2016
1 parent cd01a15 commit 3873795
Show file tree
Hide file tree
Showing 3 changed files with 55 additions and 15 deletions.
Expand Up @@ -2,6 +2,7 @@

import java.io.IOException;

import org.junit.Ignore;
import org.junit.Test;
import org.overture.codegen.vdm2c.CMakeUtil.CMakeGenerateException;

Expand Down Expand Up @@ -188,12 +189,13 @@ public void ClassValueInheritance() throws IOException,
}

//Some "scratch work" tests.
@Ignore("This is only used internally for development debugging purposes.")
@Test
public void ClassScratchWork() throws IOException,
InterruptedException, CMakeGenerateException
{
generate(getPath("classes/ClassScratchWork.vdmrt"));
compileAndTest();
compileAndTest(getTestCppFile("classes/ClassScratchWork_Tests.cpp"));
}

@Test
Expand Down
@@ -0,0 +1,21 @@
#include "gtest/gtest.h"

extern "C"
{
#include "Vdm.h"
#include <stdio.h>
#include "ClassCollectionUpdate.h"
}

#define CHECK_TRUE(methodId) TVP c=_Z21ClassCollectionUpdateEV(NULL);\
TVP res=CALL_FUNC(ClassCollectionUpdate, ClassCollectionUpdate, c, methodId);\
EXPECT_EQ (true, res->value.boolVal);\
vdmFree(res);\
vdmFree(c)



TEST(ClassScratchWork, op)
{
CHECK_TRUE(CLASS_ClassCollectionUpdate__Z20updateSeqInstanceVarEV);
}
45 changes: 31 additions & 14 deletions core/vdm2c/src/test/resources/vdmrt/classes/ClassScratchWork.vdmrt
@@ -1,19 +1,36 @@
class ScratchA
end ScratchA
class ClassCollectionUpdate

instance variables

ivarSeq : seq of nat := [1];

class ClassScratchWork
operations
op : () ==> ()
op() ==

public updateSeqInstanceVar : () ==> bool
updateSeqInstanceVar () ==
(
dcl a : ScratchA := new ScratchA();
dcl b : ScratchA;
dcl c : int := 0;
dcl d: int;
b := a;
d := c;
c := 3;
)
end ClassScratchWork
ivarSeq(1) := 5;
return ivarSeq(1) = 5;
);

end ClassCollectionUpdate

--class ScratchA
--end ScratchA
--
--class ClassScratchWork
--operations
--op : () ==> ()
--op() ==
--(
-- dcl a : ScratchA := new ScratchA();
-- dcl b : ScratchA;
-- dcl c : int := 0;
-- dcl d: int;
-- b := a;
-- d := c;
-- c := 3;
-- )
--end ClassScratchWork
-- This test illustrates that assignment needs to be more sophisticated to achieve value semantics.
-- Check generated code to observe aliasing.

0 comments on commit 3873795

Please sign in to comment.