diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg index baee6236d0f6588b655bf3634d86900aa5a21925..0f5a8992066f61a70ade1ec14836ec8b93408f83 100644 --- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg +++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate_e.stg @@ -344,7 +344,7 @@ if <if(forall)>!<endif><predicate> { quantified_expression(identifier, identity, useBigInteger, setType, hasCondition, conditionalPredicate, evaluation, isInteger) ::= << //quantified_expression -let mut <identifier> = <if(isInteger)>BInteger::new(<identity>);<else>BSet::\<<setType>\>::new(vec![]);<endif> +let mut <identifier> = <if(isInteger)><identity>;<else>BSet::\<<setType>\>::new(vec![]);<endif> <if(hasCondition)> if <conditionalPredicate> { <evaluation> @@ -543,11 +543,11 @@ let mut _ld_<name> = <identifier>.clone(); >> function_call_range_element(expr, leftType, rightType, arg, val) ::= << -<expr>._override(&BRelation<if(!leftType)>::\<bobject::Dummy, bobject::Dummy><endif>::new(vec![BTuple::new(<arg>,<val>)])) +<expr>._override_single(<arg>, <val>) >> function_call_nested(expr, arg, isNested) ::= << -<if(!isNested)><expr><else><expr>.functionCall(<arg>)<endif> +<if(!isNested)><expr><else><expr>.functionCall(&<arg>)<endif> >> assignments(assignments) ::= << diff --git a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestOtherConstructs.java b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestOtherConstructs.java new file mode 100644 index 0000000000000000000000000000000000000000..42485d721f019955bf7fe45d91d65d560a48c386 --- /dev/null +++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestOtherConstructs.java @@ -0,0 +1,205 @@ +package de.hhu.stups.codegenerator.rust_embedded; + +import de.hhu.stups.codegenerator.rust.TestRS; +import org.junit.Test; + +import java.io.IOException; +import java.net.URISyntaxException; + +public class TestOtherConstructs extends TestRSE { + public TestOtherConstructs() throws URISyntaxException, IOException {} + + @Test + public void testWhile() throws Exception { + testRSE("While", "WhileAddition.strs"); + } + + @Test + public void testEquivalence() throws Exception { + testRSE("Equivalence", "EquivalenceAddition.strs"); + } + + @Test() + public void testBooleanPredicate() throws Exception { + testRSE("BooleanPredicate", "BooleanPredicateAddition.strs"); + } + + @Test + public void testBooleanPredicateWD() throws Exception { + testRSE("BooleanPredicateWD", "BooleanPredicateAdditionWD.strs"); + } + + @Test + public void testNondeterminism() throws Exception { + testRSE("Nondeterminism", "NondeterminismAddition.strs"); + } + + @Test + public void testNondeterminism2() throws Exception { + testRSE("Nondeterminism2", "Nondeterminism2Addition.strs"); + } + + @Test + public void testMapFunction() throws Exception { + testRSE("MapFunction", "MapFunctionAddition.strs"); + } + + @Test + public void testSetUnion() throws Exception { + testRSE("SetUnion", null); + } + + + @Test + public void testManyLocalDeclarations() throws Exception { + testRSE("ManyLocalDeclarations", "ManyLocalDeclarationsAddition.strs"); + } + + @Test + public void testManyLocalDeclarations2() throws Exception { + testRSE("ManyLocalDeclarations2", "ManyLocalDeclarations2Addition.strs"); + } + + @Test + public void testAssert() throws Exception { + testRSE("Assert", null); + } + + @Test + public void testChoice() throws Exception { + testRSE("Choice", "ChoiceAddition.strs"); + } + + @Test + public void testDanglingElseWD() throws Exception { + testRSE("DanglingElseWD", "DanglingElseAdditionWD.strs"); + } + + @Test + public void testIfAndPredicates() throws Exception { + testRSE("IfAndPredicates", "IfAndPredicatesAddition.strs"); + } + + @Test + public void testNameCollision() throws Exception { + testRSE("NameCollision", "NameCollisionAddition.strs"); + } + + @Test + public void testSwap() throws Exception { + testRSE("Swap", "SwapAddition.strs"); + } + + + @Test + public void testSwap2() throws Exception { + testRSE("Swap2", "Swap2Addition.strs"); + } + + @Test + public void testUnion() throws Exception { + testRSE("Union", "UnionAddition.strs"); + } + + @Test + public void testIfExpression() throws Exception { + testRSE("IfExpression", "IfExpressionAddition.strs"); + } + + @Test + public void testIfPredicate() throws Exception { + testRSE("IfPredicate", "IfPredicateAddition.strs"); + } + + + @Test + public void testRecords() throws Exception { + testRSE("Records", null); + } + + @Test + public void testRecordsAccess() throws Exception { + testRSE("RecordsAccess", null); + } + + @Test + public void testRecordsAccess2() throws Exception { + testRSE("RecordsAccess2", null); + } + + @Test + public void testRecordsAccess3() throws Exception { + testRSE("RecordsAccess3", "RecordsAccess3.strs"); + } + + @Test + public void testRecordAccessNested() throws Exception { + testRSE("RecordAccessNested", "RecordAccessNested.strs"); + } + + @Test + public void testRecordAccessNested2() throws Exception { + testRSE("RecordAccessNested2", "RecordAccessNested2.strs"); + } + + @Test + public void testRecordAccessNested3() throws Exception { + testRSE("RecordAccessNested3", "RecordAccessNested3.strs"); + } + + @Test + public void testFunctionCallAccessNested() throws Exception { + testRSE("FunctionCallAccessNested", "FunctionCallAccessNested.strs"); + } + + @Test + public void testFunctionCallAccessNested2() throws Exception { + testRSE("FunctionCallAccessNested2", "FunctionCallAccessNested2.strs"); + } + + @Test + public void testFunctionCallAccessNested3() throws Exception { + testRSE("FunctionCallAccessNested3", "FunctionCallAccessNested3.strs"); + } + + @Test + public void testFunctionCallAccessNested4() throws Exception { + testRSE("FunctionCallAccessNested4", "FunctionCallAccessNested4.strs"); + } + + @Test + public void testFunctionCallAccessNested5() throws Exception { + testRSE("FunctionCallAccessNested5", "FunctionCallAccessNested5.strs"); + } + + @Test + public void testFunctionCallAccessNested6() throws Exception { + testRSE("FunctionCallAccessNested6", "FunctionCallAccessNested6.strs"); + } + + @Test + public void testFunctionCallAccessNested7() throws Exception { + testRSE("FunctionCallAccessNested7", "FunctionCallAccessNested7.strs"); + } + + @Test + public void testDeferredSet() throws Exception { + testRSE("DeferredSet", null); + } + + @Test + public void testDeferredSet2() throws Exception { + testRSE("DeferredSet2", null); + } + + @Test + public void testDeferredSet3() throws Exception { + testRSE("DeferredSet3", null); + } + + @Test + public void testDeferredSet4() throws Exception { + testRSE("DeferredSet4", null); + } + +} diff --git a/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.mch b/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.mch index 6ba6c4e10970052ea9497273cf39bd979bfb946d..078fb4d92725b01567be799901a67f1efd15e842 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.mch +++ b/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.mch @@ -1,22 +1,24 @@ MACHINE FunctionCallAccessNested +SETS EINT = {ONE, TWO, FOUR} + VARIABLES x, y, res INVARIANT - x : INTEGER +-> (INTEGER +-> INTEGER) & - y : INTEGER & - res : INTEGER + x : EINT +-> (EINT +-> EINT) & + y : EINT & + res : EINT INITIALISATION - x := {1|->{2|->3}, 2|->{3|->4}}; - y := 0; - res := -1 + x := {ONE|->{TWO|->ONE}, TWO|->{FOUR|->ONE}}; + y := ONE; + res := ONE OPERATIONS calculate = BEGIN - y := x(1)(2); - x(1)(2) := 4; - res := x(1)(2) + y := x(ONE)(TWO); + x(ONE)(TWO) := FOUR; + res := x(ONE)(TWO) END; out <-- getRes = BEGIN diff --git a/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.out b/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.out index bf0d87ab1b2b0ec1a11a3973d2845b42413d9767..354044830878140ee6a5d97773a778ad916456a3 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.out +++ b/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.out @@ -1 +1 @@ -4 \ No newline at end of file +FOUR \ No newline at end of file diff --git a/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.strs b/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.strs index 1b659700e3e0fc971a189cb52b662b2d20770e91..a8d43803d0bf9554fef463769285cf3df2535e7e 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.strs +++ b/src/test/resources/de/hhu/stups/codegenerator/FunctionCallAccessNested.strs @@ -1,5 +1,5 @@ fn main() { let mut functional = FunctionCallAccessNested::new(); functional.calculate(); - println!("{}", functional.getRes()); + println!("{:?}", functional.getRes()); } \ No newline at end of file diff --git a/src/test/resources/de/hhu/stups/codegenerator/IfAndPredicatesAddition.strs b/src/test/resources/de/hhu/stups/codegenerator/IfAndPredicatesAddition.strs index 8af10386254d11689add674344b32c9ba1b58d9e..ddcf3bf4e919605cad4e151f4cd54825a85c649f 100644 --- a/src/test/resources/de/hhu/stups/codegenerator/IfAndPredicatesAddition.strs +++ b/src/test/resources/de/hhu/stups/codegenerator/IfAndPredicatesAddition.strs @@ -1,5 +1,5 @@ fn main() { let mut iff = IfAndPredicates::new(); - iff.calculate(); - println!(iff.getRes()); + iff.Inc(BInteger::new(10)); + println!("{}", iff.getRes()); } \ No newline at end of file