Commit 6f6038a9 authored by Hernan Ponce de Leon's avatar Hernan Ponce de Leon
Browse files

Merge branch '3465-IStatementTerm_toZ3' of https://git.fortiss.org/af3/af3.git...

Merge branch '3465-IStatementTerm_toZ3' of https://git.fortiss.org/af3/af3.git into 3465-IStatementTerm_toZ3
parents 96d1fb81 c2a9f852
MCDCUtils.java 75c28048c3f2dd98608c4662735f462a53f3d3bb RED
MCDCUtils.java abe06c5b4e2404c19a67fceb1a022712c6ac883f YELLOW
......@@ -95,11 +95,6 @@ public final class MCDCUtils {
PredefinedFunction predefinedFunction = (PredefinedFunction)function;
EOperator operator = predefinedFunction.getOperator();
EList<ITerm> arguments = ((FunctionCall)term).getArguments();
if(arguments.size() == 1) {
// The if clause assures that the list contains exactly one argument.
Expr arg0 = toZ3(prefix, ctx, arguments.get(0), context);
return unaryOperator(ctx, operator, arg0);
}
if(arguments.size() == 2) {
// The if clause assures that the list contains exactly two arguments.
Expr arg0 = toZ3(prefix, ctx, arguments.get(0), context);
......@@ -110,52 +105,25 @@ public final class MCDCUtils {
}
}
if(term instanceof Assignment) {
Expr lhs;
Expr lhs = null;
Expr rhs = toZ3(prefix, ctx, ((Assignment)term).getValue(), context);
String identifier = ((Assignment)term).getVariable().getIdentifier();
IType type = getVarType(((Assignment)term).getVariable(), context);
// TODO(HP): the 3 ifs return the same. You can have only one return at the end.
if(type instanceof TBool) {
lhs = ctx.mkBoolConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
if(type instanceof TInt) {
lhs = ctx.mkIntConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
if(type instanceof TDouble) {
lhs = ctx.mkRealConst(prefix + identifier);
return ctx.mkEq(lhs, rhs);
}
}
return null;
}
/** Unary Operators of {@link PredefinedFunction}. */
private static Expr unaryOperator(Context ctx, EOperator operator, Expr arg0) {
try {
switch(operator) {
// TODO(HP): if it is an unary operation, is it possible to have all this operators?
// E.g. what the meaning of "or true"?
case ADD:
return ctx.mkAdd((ArithExpr)arg0);
case SUBTRACT:
return ctx.mkSub((ArithExpr)arg0);
case MULTIPLY:
return ctx.mkMul((ArithExpr)arg0);
case NOT:
return ctx.mkNot((BoolExpr)arg0);
case OR:
return ctx.mkOr((BoolExpr)arg0);
case AND:
return ctx.mkAnd((BoolExpr)arg0);
default:
return null;
if(lhs != null) {
return ctx.mkEq(lhs, rhs);
}
} catch(Z3Exception e) {
System.out.println(e.toString());
return null;
}
return null;
}
/** Binary Operators of {@link PredefinedFunction}. */
......@@ -266,8 +234,6 @@ public final class MCDCUtils {
PredefinedFunction predefinedFunction = (PredefinedFunction)function;
EOperator operator = predefinedFunction.getOperator();
switch(operator) {
// TODO(HP): I'm not familiar with the semantics of switch.
// Will the code above be executed if any of the cases match?
case LOWER_THAN:
case GREATER_THAN:
case LOWER_EQUAL:
......
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