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

SAL requires all IF expressions to have an else clause. 

As SAL doesn't verify the completeness of IF expressions, it requires an ELSE
statement so that non-deterministic behaviour does not creep in.  Fix the grid
generator to always give an ELSE clause.  A single cell is always used for any
IF expression, as it is assumed that the ELSE branch is never taken.
parent 8c3baa54

src/main/java/ca/mcscert/jtet/salgenerator/HierarchicalGridSALGenerator.java

+14 −3
Original line number Diff line number Diff line
@@ -59,7 +59,8 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridCheckerGene 
    @Override

    public void ascendFromGrid()

    {

        result.append("ENDIF ");

        handleEndIf();

        result.append(" ");

        m_firstCell = false;

    }
@@ -80,7 +81,7 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridCheckerGene 
    public void handleLeafCell(Cell cell)

    {

        outputCellPrelude(cell);

        result.append(MatlabParser.parseMatlabCode(variableDefinitions, outputGrid.get(0, m_rightMostGridIndex++).contents()).getCheckerOutput(m_generator, RealVariableType.Type));

        result.append(getOutputCellAsSALCode(m_rightMostGridIndex++));

        result.append(" ");

    }
@@ -93,12 +94,22 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridCheckerGene 
    public String getFinalString()

    {

        if (m_currentlyRunning && result.length() != 0) {

            result.append("ENDIF");

            handleEndIf();

            m_currentlyRunning = false;

        }

        return result.toString();

    }



    private void handleEndIf() {

        result.append("ELSE ")

                .append(getOutputCellAsSALCode(0))

                .append(" ENDIF");

    }



    private String getOutputCellAsSALCode(int yIndex) {

        return MatlabParser.parseMatlabCode(variableDefinitions, outputGrid.get(0, yIndex).contents()).getCheckerOutput(m_generator, RealVariableType.Type);

    }



    final private StringBuilder result = new StringBuilder();



    private boolean m_currentlyRunning = false;

src/test/java/ca/mcscert/jtet/salgenerator/HierarchicalGridSALGeneratorTest.java

+1 −1
Original line number Diff line number Diff line
@@ -69,7 +69,7 @@ public class HierarchicalGridSALGeneratorTest { 


        String out = HierarchicalGridCheckerWalkerGeneratorV2.GenerateCheckerFromGrid(grid, new HierarchicalGridSALGenerator(variableParser.parseVariables("x,z"), outputGrid));



        String expected = "IF (x > 0) THEN 1 ELSIF (x = 0) THEN IF (z > 0) THEN 2 ELSIF (z = 0) THEN IF (z = 0) THEN 3 ENDIF ELSIF (0 > z) THEN 4 ENDIF ELSIF (0 > x) THEN 5 ENDIF";

        String expected = "IF (x > 0) THEN 1 ELSIF (x = 0) THEN IF (z > 0) THEN 2 ELSIF (z = 0) THEN IF (z = 0) THEN 3 ELSE 1 ENDIF ELSIF (0 > z) THEN 4 ELSE 1 ENDIF ELSIF (0 > x) THEN 5 ELSE 1 ENDIF";

        assertEquals(expected, out);

    }