Package: JmlAnnotationHelper

JmlAnnotationHelper

nameinstructionbranchcomplexitylinemethod
JmlAnnotationHelper(JmlGenerator)
M: 0 C: 12
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
addInvCheckGhostVarDecl(ADefaultClassDeclIR)
M: 0 C: 16
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
addMetaData(PIR, List, boolean)
M: 0 C: 10
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
addRecInv(ARecordDeclIR)
M: 0 C: 40
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 9
100%
M: 0 C: 1
100%
appendFieldNames(List, StringBuilder)
M: 0 C: 30
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
appendMetaData(PIR, List)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
consAnno(String, String, List)
M: 0 C: 27
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
consInvChecksOnName(ADefaultClassDeclIR)
M: 0 C: 33
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 8
100%
M: 0 C: 1
100%
consInvChecksOnNameEncClass()
M: 0 C: 4
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
consInvChecksOnNameEncClass(ADefaultClassDeclIR)
M: 0 C: 15
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
consMetaData(String)
M: 0 C: 13
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
consMetaData(StringBuilder)
M: 0 C: 5
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
makeCondPublic(SDeclIR)
M: 11 C: 9
45%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 1 C: 3
75%
M: 0 C: 1
100%
makeHelper(SDeclIR)
M: 0 C: 9
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 3
100%
M: 0 C: 1
100%
makeNamedTypeInvFuncsPublic(ADefaultClassDeclIR)
M: 0 C: 21
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
makeNullableByDefault(ADefaultClassDeclIR)
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
makePure(SDeclIR)
M: 0 C: 9
100%
M: 1 C: 1
50%
M: 1 C: 1
50%
M: 0 C: 3
100%
M: 0 C: 1
100%
makeRecMethodsPure(List)
M: 0 C: 37
100%
M: 0 C: 6
100%
M: 0 C: 4
100%
M: 0 C: 8
100%
M: 0 C: 1
100%
makeSpecPublic(AFieldDeclIR)
M: 0 C: 7
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 2
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.codegen.vdm2jml;
2:
3: import java.util.LinkedList;
4: import java.util.List;
5:
6: import org.apache.log4j.Logger;
7: import org.overture.ast.util.ClonableString;
8: import org.overture.codegen.ir.IRConstants;
9: import org.overture.codegen.ir.IRStatus;
10: import org.overture.codegen.ir.PIR;
11: import org.overture.codegen.ir.SDeclIR;
12: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
13: import org.overture.codegen.ir.declarations.AFieldDeclIR;
14: import org.overture.codegen.ir.declarations.AMethodDeclIR;
15: import org.overture.codegen.ir.declarations.ARecordDeclIR;
16: import org.overture.codegen.vdm2java.JavaCodeGenUtil;
17:
18: public class JmlAnnotationHelper
19: {
20:         private JmlGenerator jmlGen;
21:
22:         private Logger log = Logger.getLogger(this.getClass().getName());
23:
24:         public JmlAnnotationHelper(JmlGenerator jmlGen)
25:         {
26:                 this.jmlGen = jmlGen;
27:         }
28:
29:         public void makeNullableByDefault(ADefaultClassDeclIR clazz)
30:         {
31:                 clazz.setGlobalMetaData(consMetaData(JmlGenerator.JML_NULLABLE_BY_DEFAULT));
32:         }
33:
34:         public void makeNamedTypeInvFuncsPublic(ADefaultClassDeclIR clazz)
35:         {
36:                 List<AMethodDeclIR> nameInvMethods = jmlGen.getUtil().getNamedTypeInvMethods(clazz);
37:
38:•                for (AMethodDeclIR method : nameInvMethods)
39:                 {
40:                         makeCondPublic(method);
41:                 }
42:         }
43:
44:         public void makeRecMethodsPure(List<IRStatus<PIR>> ast)
45:         {
46:                 List<ARecordDeclIR> records = jmlGen.getUtil().getRecords(ast);
47:
48:•                for (ARecordDeclIR rec : records)
49:                 {
50:•                        for (AMethodDeclIR method : rec.getMethods())
51:                         {
52:•                                if (!method.getIsConstructor())
53:                                 {
54:                                         makePure(method);
55:                                 }
56:                         }
57:                 }
58:         }
59:
60:         public List<ClonableString> consAnno(String jmlAnno, String pred,
61:                         List<String> fieldNames)
62:         {
63:                 StringBuilder sb = new StringBuilder();
64:                 sb.append(String.format("//@ %s %s", jmlAnno, pred));
65:
66:                 appendFieldNames(fieldNames, sb);
67:
68:                 return consMetaData(sb);
69:         }
70:
71:         private void appendFieldNames(List<String> fieldNames, StringBuilder sb)
72:         {
73:
74:                 sb.append("(");
75:
76:                 String sep = "";
77:•                for (String fName : fieldNames)
78:                 {
79:                         sb.append(sep).append(fName);
80:                         sep = ",";
81:                 }
82:
83:                 sb.append(");");
84:         }
85:
86:         public void addInvCheckGhostVarDecl(ADefaultClassDeclIR owner)
87:         {
88:                 String metaStr = String.format(JmlGenerator.JML_INV_CHECKS_ON_DECL, JmlGenerator.INV_CHECKS_ON_GHOST_VAR_NAME);
89:
90:                 appendMetaData(owner, consMetaData(metaStr));
91:         }
92:
93:         private String consInvChecksOnName(ADefaultClassDeclIR owner)
94:         {
95:                 StringBuilder prefix = new StringBuilder();
96:
97:•                if (JavaCodeGenUtil.isValidJavaPackage(owner.getPackage()))
98:                 {
99:                         prefix.append(owner.getPackage());
100:                         prefix.append(".");
101:                 }
102:
103:                 prefix.append(owner.getName());
104:                 prefix.append(".");
105:                 prefix.append(JmlGenerator.INV_CHECKS_ON_GHOST_VAR_NAME);
106:
107:                 return prefix.toString();
108:         }
109:
110:         public void addRecInv(ARecordDeclIR r)
111:         {
112:
113:                 List<String> args = jmlGen.getUtil().getRecFieldNames(r);
114:
115:                 String jmlAnno = "public " + JmlGenerator.JML_INSTANCE_INV_ANNOTATION;
116:
117:                 StringBuilder pred = new StringBuilder();
118:                 pred.append(consInvChecksOnNameEncClass());
119:                 pred.append(JmlGenerator.JML_IMPLIES);
120:                 pred.append(JmlGenerator.INV_PREFIX);
121:                 pred.append(r.getName());
122:
123:                 appendMetaData(r, consAnno(jmlAnno, pred.toString(), args));
124:         }
125:
126:         public String consInvChecksOnNameEncClass()
127:         {
128:                 return consInvChecksOnNameEncClass(null);
129:         }
130:
131:         public String consInvChecksOnNameEncClass(
132:                         ADefaultClassDeclIR enclosingClass)
133:         {
134:•                if (enclosingClass != null
135:•                                && enclosingClass == jmlGen.getInvChecksFlagOwner())
136:                 {
137:                         return JmlGenerator.INV_CHECKS_ON_GHOST_VAR_NAME;
138:                 } else
139:                 {
140:                         return consInvChecksOnName(jmlGen.getInvChecksFlagOwner());
141:                 }
142:         }
143:
144:         public void makePure(SDeclIR cond)
145:         {
146:•                if (cond != null)
147:                 {
148:                         appendMetaData(cond, consMetaData(JmlGenerator.JML_PURE));
149:                 }
150:         }
151:
152:         public void makeHelper(SDeclIR cond)
153:         {
154:•                if (cond != null)
155:                 {
156:                         appendMetaData(cond, consMetaData(JmlGenerator.JML_HELPER));
157:                 }
158:         }
159:
160:         public void makeCondPublic(SDeclIR cond)
161:         {
162:•                if (cond instanceof AMethodDeclIR)
163:                 {
164:                         ((AMethodDeclIR) cond).setAccess(IRConstants.PUBLIC);
165:                 } else
166:                 {
167:                         log.error("Expected method declaration but got: " + cond);
168:                 }
169:         }
170:
171:         public void addMetaData(PIR node, List<ClonableString> extraMetaData,
172:                         boolean prepend)
173:         {
174:                 this.jmlGen.getJavaGen().getInfo().getNodeAssistant().addMetaData(node, extraMetaData, prepend);
175:         }
176:
177:         public void appendMetaData(PIR node, List<ClonableString> extraMetaData)
178:         {
179:                 addMetaData(node, extraMetaData, false);
180:         }
181:
182:         public void makeSpecPublic(AFieldDeclIR f)
183:         {
184:                 appendMetaData(f, consMetaData(JmlGenerator.JML_SPEC_PUBLIC));
185:         }
186:
187:         public List<ClonableString> consMetaData(StringBuilder sb)
188:         {
189:                 return consMetaData(sb.toString());
190:         }
191:
192:         public List<ClonableString> consMetaData(String str)
193:         {
194:                 List<ClonableString> inv = new LinkedList<ClonableString>();
195:
196:                 inv.add(new ClonableString(str));
197:
198:                 return inv;
199:         }
200: }