Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
af3
AF3
Commits
4b410adf
Commit
4b410adf
authored
Sep 11, 2018
by
Hernan Ponce de Leon
Browse files
MCDC: review [RED]
parent
1d85f4eb
Changes
2
Hide whitespace changes
Inline
Side-by-side
org.fortiss.af3.testing/src/org/fortiss/af3/testing/mcdc/.ratings
View file @
4b410adf
MCDCUtils.java
a974fd3e2b293acab8807c098ea83e94376e2cd6 YELLOW
MCDCUtils.java
75c28048c3f2dd98608c4662735f462a53f3d3bb RED
org.fortiss.af3.testing/src/org/fortiss/af3/testing/mcdc/MCDCUtils.java
View file @
4b410adf
...
...
@@ -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:
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment