Commit d7883686 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add some more variable declaration tests, covering boolean and subtypes. 

To ensure better test coverage, add boolean and predicate subtypes to the list
of generic tests.  Both are again very simple additions, and all current
generators are fine with them.  They are skippable in the usual way.
parent 0941ddf5

src/test/java/ca/mcscert/jtet/expression/GenericVariableDeclarationGeneratorTest.java

+32 −4
Original line number Diff line number Diff line
@@ -51,6 +51,8 @@ public class GenericVariableDeclarationGeneratorTest { 
                {new SMTLIBGenerator(),

                        "(declare-fun x () Real)\n",

                        "(declare-fun new_x_name () Real)\n",

                        "(declare-fun x () Real)\n(assert (> x 0.0))\n",

                        "(declare-fun x () Bool)\n",

                        null,

                        null,

                        "(declare-sort MyEnum 0)\n" +
@@ -83,6 +85,8 @@ public class GenericVariableDeclarationGeneratorTest { 
                {new CVC3Generator(),

                        "x:REAL;\n",

                        "new_x_name:REAL;\n",

                        "x:REAL;\nASSERT (x > 0);\n",

                        "x:BOOLEAN;\n",

                        "x:BITVECTOR(8);\n",

                        "x:BITVECTOR(8);\n",

                        "DATATYPE\n  MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\n",
@@ -104,6 +108,8 @@ public class GenericVariableDeclarationGeneratorTest { 
                        null,

                        null,

                        null,

                        null,

                        null,

                        null

                }

        });
@@ -118,18 +124,24 @@ public class GenericVariableDeclarationGeneratorTest { 
    public String RealExpectedOutputWithNameChange;



    @Parameter(value = 3)

    public String SignedFixedPointExpectedOutput;

    public String RealWithPredicateSubtypeExpectedOutput;



    @Parameter(value = 4)

    public String UnsignedFixedPointExpectedOutput;

    public String BooleanExpectedOutput;



    @Parameter(value = 5)

    public String SingleVariableSingleEnumerationExpectedOutput;

    public String SignedFixedPointExpectedOutput;



    @Parameter(value = 6)

    public String SingleVariableSingleEnumerationExpectedWithNameChangeOutput;

    public String UnsignedFixedPointExpectedOutput;



    @Parameter(value = 7)

    public String SingleVariableSingleEnumerationExpectedOutput;



    @Parameter(value = 8)

    public String SingleVariableSingleEnumerationExpectedWithNameChangeOutput;



    @Parameter(value = 9)

    public String MultipleVariableSingleEnumerationExpectedOutput;



    @Test
@@ -149,6 +161,22 @@ public class GenericVariableDeclarationGeneratorTest { 
        }

    }



    @Test

    public void RealWithPredicateSubtypeTest() {

        if (RealWithPredicateSubtypeExpectedOutput != null) {

            VariableCollection vars = variableParser.parseVariables("x:{p:REAL|p > 0}");

            assertEquals(RealWithPredicateSubtypeExpectedOutput, generator.GenerateVariablesDeclaration(vars));

        }

    }



    @Test

    public void BooleanTest() {

        if (BooleanExpectedOutput != null) {

            VariableCollection vars = variableParser.parseVariables("x:bool");

            assertEquals(BooleanExpectedOutput, generator.GenerateVariablesDeclaration(vars));

        }

    }



    @Test

    public void SignedFixedPointTest() {

        if (SignedFixedPointExpectedOutput != null) {