Commit 20151657 authored by Ludwig Dickmanns's avatar Ludwig Dickmanns
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 d5995cd7 4b410adf
MCDCUtils.java a974fd3e2b293acab8807c098ea83e94376e2cd6 YELLOW
MCDCUtils.java 75c28048c3f2dd98608c4662735f462a53f3d3bb RED
......@@ -42,6 +42,7 @@ import org.fortiss.af3.project.model.typesystem.IFunction;
import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.project.model.typesystem.VarBase;
import org.fortiss.af3.testing.model.mcdc.FormalRequirementMCDC;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
......@@ -113,6 +114,7 @@ public final class MCDCUtils {
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);
......@@ -133,6 +135,8 @@ public final class MCDCUtils {
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:
......@@ -262,6 +266,8 @@ 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