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

Fix CVC3 fixed point subtraction. 

CVC3 subtraction works similarly to addition, which requires a parameter
telling CVC3 where to cut off digits in the computed result.  jTET missed that,
so fix it.
parent 098446c5

src/main/java/ca/mcscert/jtet/expression/CVC3Generator.java

+1 −1
Original line number Diff line number Diff line
@@ -104,7 +104,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
                if (!((FixedPointVariableType) type).isSigned()) {

                    func = GetUnsignedFixedPointFunctionFor(op);

                }

                if (op == BinaryOperation.Addition || op == BinaryOperation.Multiplication) {

                if (op == BinaryOperation.Addition || op == BinaryOperation.Minus || op == BinaryOperation.Multiplication) {

                    FixedPointVariableType typeF = (FixedPointVariableType) type;

                    return func + typeF.digits() + ",";

                } else {

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

+2 −2
Original line number Diff line number Diff line
@@ -55,8 +55,8 @@ public class GenericOperationGeneratorTest { 
                        null},

                {new CVC3Generator(),

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

                        "(((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVSGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVSLT(0bin00100100,BVSUB(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(x,0bin00001000))) OR (BVGE(x,0bin00110000) OR ((NOT BVLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))"

                        "(((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(),

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