Commit 698d3001 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Finally, move the subtype predicate storage to the Variable. 

Since the predicate subtype can be set per variable, move that logic to the
Variable class, away from the Type class.  Before, Type disagreed on whether
two instances could be equal, and whether they could be easily duplicated.
This makes the distinction unimportant.  It does neuter the custom type
functionality in VariableParser some, but that can be added back later.
parent 64345eb1

src/main/java/ca/mcscert/jtet/cvc3generator/CVC3VariablesDeclarationGenerator.java

+2 −2
Original line number Diff line number Diff line
@@ -55,9 +55,9 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara 


        // Then generate the variable predicates.  This ensures any dependent variables are declared.

        for(Variable var : variables) {

            if (var.type().subtypePredicate() != null) {

            if (var.subtypePredicate() != null) {

                ret.append("ASSERT ")

                   .append(var.type().subtypePredicate().getCheckerOutput(CVC3ExpressionGenerator.Generator, BooleanType.Type))

                   .append(var.subtypePredicate().getCheckerOutput(CVC3ExpressionGenerator.Generator, BooleanType.Type))

                   .append(";\n");

            }

        }

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

+0 −10
Original line number Diff line number Diff line
@@ -25,14 +25,4 @@ public abstract class Type implements TypeMarker { 
    public boolean isMarkerFor(Type m_type) {

        return this.equals(m_type);

    }



    public Expression subtypePredicate() {

        return m_subtypePredicate;

    }



    public void setSubtypePredicate(Expression subtypePredicate) {

        m_subtypePredicate = subtypePredicate;

    }



    private Expression m_subtypePredicate;

}

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

+17 −0
Original line number Diff line number Diff line
@@ -80,8 +80,25 @@ public class Variable implements Expression, ExpressionValue { 
        return null;

    }



    /**

     * Returns the expression representing the subtype predicate for this variable.

     * @return Expression representing the predicate.

     */

    public Expression subtypePredicate() {

        return m_subtypePredicate;

    }



    /**

     * Sets the expression to represent the subtype predicate for this variable.

     * @param subtypePredicate The expression to use as the subtype predicate.

     */

    public void setSubtypePredicate(Expression subtypePredicate) {

        m_subtypePredicate = subtypePredicate;

    }



    final private String m_name;

    private String m_outputName;

    private Expression m_subtypePredicate;

    final private Type m_type;



    /**

src/main/java/ca/mcscert/jtet/parsers/VariableParser.java

+1 −1
Original line number Diff line number Diff line
@@ -172,7 +172,7 @@ final public class VariableParser { 
                m_variables.put(subtypeVar, m_variables.get(limitingExpression.getKey()));



                VariableCollection variableCollection = new VariableCollection(new PartialVariableCollection(m_variables, m_usedEnumerationTypes));

                m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(variableCollection, subtypeExpression));

                m_variables.get(limitingExpression.getKey()).setSubtypePredicate(PVSSimpleParser.parsePVSCode(variableCollection, subtypeExpression));



                // Undo the variables hack, to avoid having unused variables bleed into the verification scripts!

                m_variables.remove(subtypeVar);

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

+4 −5
Original line number Diff line number Diff line
@@ -45,16 +45,15 @@ public class SALVariablesDeclarationGenerator implements VariablesDeclarationGen 
        // Generate all the variables.

        for(Variable var : variables) {

            ret.append(var.outputName()).append(":");

            Type type = var.type();

            if (type.subtypePredicate() == null) {

                ret.append(GenerateType(type));

            if (var.subtypePredicate() == null) {

                ret.append(GenerateType(var.type()));

            } else {

                ret.append("{")

                        .append(var.outputName())

                        .append(":")

                        .append(GenerateType(type))

                        .append(GenerateType(var.type()))

                        .append("|")

                        .append(type.subtypePredicate().getCheckerOutput(SALExpressionGenerator.Generator, BooleanType.Type))

                        .append(var.subtypePredicate().getCheckerOutput(SALExpressionGenerator.Generator, BooleanType.Type))

                        .append("}");

            }

            ret.append("\n");