Commit 918579a0 authored by Yanjun Jiang's avatar Yanjun Jiang Committed by Matthew Dawson
Browse files

Rename SALGenerator to SALExpressionGenerator. 

This commit is used to keep the changes history clean so that the
modification is easy to see.
parent 16d392a1

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

+1 −2
Original line number Diff line number Diff line
@@ -31,7 +31,6 @@ package ca.mcscert.jtet.salgenerator; 


import ca.mcscert.jtet.expression.BooleanVariableType;

import ca.mcscert.jtet.expression.RealVariableType;

import ca.mcscert.jtet.expression.SALGenerator;

import ca.mcscert.jtet.expression.VariableCollection;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.Cell;
@@ -119,5 +118,5 @@ public class HierarchicalGridSALGenerator implements HierarchicalGridCheckerGene 
    final private VariableCollection variableDefinitions;

    final private TwoDimensionalGrid outputGrid;



    final private SALGenerator m_generator = new SALGenerator();

    final private SALExpressionGenerator m_generator = new SALExpressionGenerator();

}

src/main/java/ca/mcscert/jtet/expression/SALGenerator.java→src/main/java/ca/mcscert/jtet/salgenerator/SALExpressionGenerator.java

+4 −2
Original line number Diff line number Diff line
@@ -26,14 +26,16 @@ 
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE

 * POSSIBILITY OF SUCH DAMAGE.

 */

package ca.mcscert.jtet.expression;

package ca.mcscert.jtet.salgenerator;



import ca.mcscert.jtet.expression.*;



import java.util.Map;



/**

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

public class SALGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {

public class SALExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {



    private static String GetInfixSymbolFor(BinaryOperation op) {

        switch (op) {

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

+2 −1
Original line number Diff line number Diff line
@@ -29,6 +29,7 @@ 
package ca.mcscert.jtet.expression;



import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;

import ca.mcscert.jtet.salgenerator.SALExpressionGenerator;

import ca.mcscert.jtet.smtlibchecker.SMTLIBExpressionGenerator;

import ca.mcscert.jtet.parsers.PVSSimpleParser;

import ca.mcscert.jtet.parsers.VariableParser;
@@ -60,7 +61,7 @@ public class GenericOperationGeneratorTest { 
                        "(((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVSGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVSLT(0bin00100100,BVSUB(8,x,0bin00001000))) OR (BVSGE(x,0bin00110000) OR ((NOT BVSLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))",

                        "(((BVMULT(8,x,0bin00010100) = BVUDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVLT(0bin00100100,BVSUB(8,x,0bin00001000))) OR (BVGE(x,0bin00110000) OR ((NOT BVLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))"

                },

                {new SALGenerator(),

                {new SALExpressionGenerator(),

                        "((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",

                        null,

                        null

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

+2 −1
Original line number Diff line number Diff line
@@ -30,6 +30,7 @@ package ca.mcscert.jtet.expression; 


import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;

import ca.mcscert.jtet.parsers.VariableParser;

import ca.mcscert.jtet.salgenerator.SALExpressionGenerator;

import ca.mcscert.jtet.smtlibchecker.SMTLIBVariablesDeclarationGenerator;

import org.junit.Before;

import org.junit.Test;
@@ -96,7 +97,7 @@ public class GenericVariablesDeclarationGeneratorTest { 
                        null,

                        null

                },

                {new SALGenerator(),

                {new SALExpressionGenerator(),

                        "x:REAL\n",

                        "new_x_name:REAL\n",

                        "x:{x:REAL|(x > 0)}\n",