Commit 8f926aa5 authored by Ludwig Dickmanns's avatar Ludwig Dickmanns
Browse files

MCDC: Corrections

* Corrections discussed in the meeting

Issue-Ref: 3465
Issue-Url: https://af3-developer.fortiss.org/issues/3465

Signed-off-by: Ludwig Dickmanns's avatarLudwig Dickmanns <dickmanns@fortiss.org>
parent a5b63b9c
......@@ -23,7 +23,6 @@ import java.util.stream.Collectors;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.ecore.EObject;
import org.fortiss.af3.expression.model.terms.BoolConst;
import org.fortiss.af3.expression.model.terms.Const;
import org.fortiss.af3.expression.model.terms.DoubleConst;
import org.fortiss.af3.expression.model.terms.EOperator;
import org.fortiss.af3.expression.model.terms.FunctionCall;
......@@ -73,20 +72,16 @@ public final class MCDCUtils {
// The highlevel checks were there to identify the lowest level unmatched case (e.g. unmatched
// IExpressionTerm as print instead of only saying unmatched)
public static Expr toZ3(String prefix, Context ctx, ITerm term, EObject context) {
if(term instanceof Const) {
if(term instanceof BoolConst) {
return ctx.mkBool(((BoolConst)term).getValue());
}
if(term instanceof IntConst) {
return ctx.mkInt(((IntConst)term).getValue());
}
if(term instanceof DoubleConst) {
return ctx.mkReal(Double.toString(((DoubleConst)term).getValue()));
}
return null;
if(term instanceof BoolConst) {
return ctx.mkBool(((BoolConst)term).getValue());
}
if(term instanceof IntConst) {
return ctx.mkInt(((IntConst)term).getValue());
}
if(term instanceof DoubleConst) {
return ctx.mkReal(Double.toString(((DoubleConst)term).getValue()));
}
if(term instanceof Var) {
// TODO: just use an empty prefix for the null case?
IType type = getVarType((VarBase)term, context);
if(type instanceof TBool) {
return ctx.mkBoolConst(prefix + ((Var)term).getIdentifier());
......@@ -97,7 +92,6 @@ public final class MCDCUtils {
if(type instanceof TDouble) {
return ctx.mkRealConst(prefix + ((Var)term).getIdentifier());
}
return null;
}
if(term instanceof FunctionCall) {
IFunction function = ((FunctionCall)term).getFunction();
......@@ -118,7 +112,6 @@ public final class MCDCUtils {
}
return multipleOperator(prefix, ctx, context, operator, arguments);
}
return null;
}
if(term instanceof Assignment) {
Expr lhs;
......@@ -137,7 +130,6 @@ public final class MCDCUtils {
lhs = ctx.mkRealConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
return null;
}
// TODO: uncomment when merged in mcdc-master
// if(term instanceof FormalRequirementMCDC) {
......@@ -175,7 +167,6 @@ public final class MCDCUtils {
case AND:
return ctx.mkAnd((BoolExpr)arg0);
default:
System.out.println("Not an unary operator: " + operator.toString());
return null;
}
} catch(Z3Exception e) {
......@@ -188,7 +179,6 @@ public final class MCDCUtils {
private static Expr binaryOperator(Context ctx, EOperator operator, Expr arg0, Expr arg1) {
try {
switch(operator) {
// TODO use mulOp for bin case of add, sub, mul, or, and??
case ADD:
return ctx.mkAdd((ArithExpr)arg0, (ArithExpr)arg1);
case SUBTRACT:
......@@ -216,7 +206,6 @@ public final class MCDCUtils {
case AND:
return ctx.mkAnd((BoolExpr)arg0, (BoolExpr)arg1);
default:
System.out.println("Not a binary operator: " + operator.toString());
return null;
}
} catch(Z3Exception e) {
......@@ -255,7 +244,6 @@ public final class MCDCUtils {
return ctx.mkAnd(tmp.toArray(new BoolExpr[tmp.size()]));
}
}
System.out.println("Not a multiple operator: " + operator.toString());
return null;
} catch(Z3Exception e) {
System.out.println(e.toString());
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment