Package: RecModUtil

RecModUtil

nameinstructionbranchcomplexitylinemethod
RecModUtil(RecModHandler)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
assertRec(SExpIR)
M: 3 C: 30
91%
M: 3 C: 3
50%
M: 3 C: 1
25%
M: 1 C: 5
83%
M: 0 C: 1
100%
consValidRecCheck(SExpIR, String, ARecordTypeIR)
M: 0 C: 95
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 21
100%
M: 0 C: 1
100%
handleRecAssert(SExpIR, String, ARecordTypeIR)
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
simpleRecSetCallOutsideAtomic(ACallObjectExpStmIR)
M: 4 C: 34
89%
M: 3 C: 7
70%
M: 3 C: 3
50%
M: 2 C: 9
82%
M: 0 C: 1
100%

Coverage

1: package org.overture.codegen.vdm2jml.predgen;
2:
3: import org.overture.codegen.ir.IRInfo;
4: import org.overture.codegen.ir.SExpIR;
5: import org.overture.codegen.ir.declarations.ARecordDeclIR;
6: import org.overture.codegen.ir.expressions.ACastUnaryExpIR;
7: import org.overture.codegen.ir.expressions.SVarExpIR;
8: import org.overture.codegen.ir.statements.ACallObjectExpStmIR;
9: import org.overture.codegen.ir.statements.AMetaStmIR;
10: import org.overture.codegen.ir.types.ARecordTypeIR;
11: import org.overture.codegen.vdm2jml.JmlGenerator;
12:
13: public class RecModUtil
14: {
15:         private RecModHandler handler;
16:
17:         public RecModUtil(RecModHandler handler)
18:         {
19:                 this.handler = handler;
20:         }
21:
22:         public boolean simpleRecSetCallOutsideAtomic(ACallObjectExpStmIR node)
23:         {
24:•                if (handler.getInvTrans().getJmlGen().getJavaGen().getInfo().getStmAssistant().inAtomic(node))
25:                 {
26:                         return false;
27:                 }
28:
29:                 SExpIR obj = node.getObj();
30:
31:•                if (!(obj.getType() instanceof ARecordTypeIR))
32:                 {
33:                         return false;
34:                 }
35:
36:•                if (obj instanceof SVarExpIR)
37:                 {
38:                         return true;
39:                 }
40:
41:•                if (obj instanceof ACastUnaryExpIR
42:•                                && ((ACastUnaryExpIR) obj).getExp() instanceof SVarExpIR)
43:                 {
44:                         return true;
45:                 }
46:
47:                 return false;
48:         }
49:
50:         public AMetaStmIR handleRecAssert(SExpIR var, String varName,
51:                         ARecordTypeIR recType)
52:         {
53:                 return handler.getInvTrans().consMetaStm(consValidRecCheck(var, varName, recType));
54:         }
55:
56:         public String consValidRecCheck(SExpIR subject, String varName,
57:                         ARecordTypeIR recType)
58:         {
59:                 StringBuilder as = new StringBuilder();
60:                 as.append("//@ assert ");
61:
62:                 String subjectStr;
63:•                if (subject instanceof ACastUnaryExpIR)
64:                 {
65:                         String fullRecType = handler.getInvTrans().getTypePredUtil().fullyQualifiedRecType(recType);
66:                         as.append(varName);
67:                         as.append(JmlGenerator.JAVA_INSTANCEOF);
68:                         as.append(fullRecType);
69:                         as.append(JmlGenerator.JML_IMPLIES);
70:
71:                         subjectStr = "((" + fullRecType + ") " + varName + ")";
72:                 } else
73:                 {
74:                         subjectStr = varName;
75:                 }
76:
77:•                if (handler.getInvTrans().getJmlGen().getJmlSettings().genInvariantFor())
78:                 {
79:                         as.append(JmlGenerator.JML_INVARIANT_FOR);
80:                         as.append('(');
81:                         as.append(subjectStr);
82:                         as.append(')');
83:                 } else
84:                 {
85:                         as.append(subjectStr);
86:                         as.append('.');
87:                         as.append(JmlGenerator.REC_VALID_METHOD_CALL);
88:                 }
89:
90:                 as.append(';');
91:
92:                 return as.toString();
93:         }
94:
95:         public boolean assertRec(SExpIR exp)
96:         {
97:•                if (exp.getType().getNamedInvType() != null
98:•                                || !(exp.getType() instanceof ARecordTypeIR))
99:                 {
100:                         return false;
101:                 }
102:
103:                 IRInfo info = handler.getInvTrans().getJmlGen().getJavaGen().getInfo();
104:                 ARecordDeclIR rec = info.getDeclAssistant().findRecord(info.getClasses(), (ARecordTypeIR) exp.getType());
105:
106:•                return rec.getInvariant() != null;
107:         }
108: }