Package: TypePredHandler

TypePredHandler

nameinstructionbranchcomplexitylinemethod
TypePredHandler(TypePredDecorator)
M: 0 C: 18
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
addAssert(AAssignToExpStmIR, AMetaStmIR)
M: 0 C: 22
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
consAsserts(AIdentifierVarExpIR)
M: 4 C: 29
88%
M: 2 C: 2
50%
M: 2 C: 1
33%
M: 2 C: 5
71%
M: 0 C: 1
100%
getAnnotator()
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%
getDecorator()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getEncBlockStm(AVarDeclIR)
M: 31 C: 22
42%
M: 5 C: 3
38%
M: 4 C: 1
20%
M: 9 C: 6
40%
M: 0 C: 1
100%
getInfo()
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getJmlGen()
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%
getTransAssist()
M: 0 C: 6
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
getTypePredUtil()
M: 0 C: 3
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
handleAssign(AAssignToExpStmIR)
M: 13 C: 56
81%
M: 2 C: 6
75%
M: 2 C: 3
60%
M: 3 C: 12
80%
M: 0 C: 1
100%
handleBlock(ABlockStmIR)
M: 0 C: 83
100%
M: 0 C: 10
100%
M: 0 C: 6
100%
M: 0 C: 17
100%
M: 0 C: 1
100%
handleCallObj(ACallObjectExpStmIR)
M: 46 C: 48
51%
M: 6 C: 4
40%
M: 4 C: 2
33%
M: 9 C: 12
57%
M: 0 C: 1
100%
handleClass(ADefaultClassDeclIR)
M: 0 C: 33
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
handleField(AFieldDeclIR)
M: 1 C: 74
99%
M: 2 C: 8
80%
M: 2 C: 4
67%
M: 1 C: 12
92%
M: 0 C: 1
100%
handleMapSeq(AMapSeqUpdateStmIR)
M: 17 C: 72
81%
M: 5 C: 5
50%
M: 5 C: 1
17%
M: 4 C: 15
79%
M: 0 C: 1
100%
handleMethod(AMethodDeclIR)
M: 2 C: 104
98%
M: 3 C: 9
75%
M: 3 C: 4
57%
M: 2 C: 21
91%
M: 0 C: 1
100%
handleReturn(AReturnStmIR)
M: 1 C: 85
99%
M: 1 C: 3
75%
M: 1 C: 2
67%
M: 1 C: 18
95%
M: 0 C: 1
100%
handleVarDecl(AVarDeclIR)
M: 4 C: 60
94%
M: 2 C: 6
75%
M: 2 C: 3
60%
M: 2 C: 11
85%
M: 0 C: 1
100%
inModuleToStringMethod(INode)
M: 2 C: 20
91%
M: 2 C: 4
67%
M: 2 C: 2
50%
M: 1 C: 6
86%
M: 0 C: 1
100%
proceed(AbstractTypeInfo)
M: 0 C: 7
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 1
100%
M: 0 C: 1
100%
rightHandSideMayBeNull(SExpIR)
M: 19 C: 0
0%
M: 2 C: 0
0%
M: 2 C: 0
0%
M: 5 C: 0
0%
M: 1 C: 0
0%
treatMethod(INode)
M: 0 C: 28
100%
M: 0 C: 8
100%
M: 0 C: 5
100%
M: 0 C: 7
100%
M: 0 C: 1
100%
varMayBeNull(STypeIR)
M: 1 C: 13
93%
M: 2 C: 2
50%
M: 2 C: 1
33%
M: 0 C: 2
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.codegen.vdm2jml.predgen;
2:
3: import java.util.LinkedList;
4: import java.util.List;
5:
6: import org.apache.log4j.Logger;
7: import org.overture.codegen.ir.INode;
8: import org.overture.codegen.ir.IRGeneratedTag;
9: import org.overture.codegen.ir.IRInfo;
10: import org.overture.codegen.ir.SExpIR;
11: import org.overture.codegen.ir.SStmIR;
12: import org.overture.codegen.ir.STypeIR;
13: import org.overture.codegen.ir.analysis.AnalysisException;
14: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
15: import org.overture.codegen.ir.declarations.AFieldDeclIR;
16: import org.overture.codegen.ir.declarations.AFormalParamLocalParamIR;
17: import org.overture.codegen.ir.declarations.AMethodDeclIR;
18: import org.overture.codegen.ir.declarations.AVarDeclIR;
19: import org.overture.codegen.ir.expressions.ACastUnaryExpIR;
20: import org.overture.codegen.ir.expressions.AIdentifierVarExpIR;
21: import org.overture.codegen.ir.expressions.SVarExpIR;
22: import org.overture.codegen.ir.patterns.AIdentifierPatternIR;
23: import org.overture.codegen.ir.statements.AAssignToExpStmIR;
24: import org.overture.codegen.ir.statements.ABlockStmIR;
25: import org.overture.codegen.ir.statements.ACallObjectExpStmIR;
26: import org.overture.codegen.ir.statements.AForLoopStmIR;
27: import org.overture.codegen.ir.statements.AMapSeqUpdateStmIR;
28: import org.overture.codegen.ir.statements.AMetaStmIR;
29: import org.overture.codegen.ir.statements.AReturnStmIR;
30: import org.overture.codegen.trans.assistants.TransAssistantIR;
31: import org.overture.codegen.vdm2jml.JmlAnnotationHelper;
32: import org.overture.codegen.vdm2jml.JmlGenerator;
33: import org.overture.codegen.vdm2jml.predgen.info.AbstractTypeInfo;
34: import org.overture.codegen.vdm2jml.predgen.info.UnknownLeaf;
35: import org.overture.codegen.vdm2jml.util.IsValChecker;
36:
37: public class TypePredHandler
38: {
39:         public static final String RET_VAR_NAME_PREFIX = "ret_";
40:         public static final String MAP_SEQ_NAME_PREFIX = "col_";
41:
42:         private TypePredDecorator decorator;
43:         private TypePredUtil util;
44:
45:         private Logger log = Logger.getLogger(this.getClass().getName());
46:
47:         public TypePredDecorator getDecorator()
48:         {
49:                 return decorator;
50:         }
51:
52:         public TypePredHandler(TypePredDecorator decorator)
53:         {
54:                 this.decorator = decorator;
55:                 this.util = new TypePredUtil(this);
56:         }
57:
58:         public void handleClass(ADefaultClassDeclIR node) throws AnalysisException
59:         {
60:                 // We want only to treat fields and methods specified by the user.
61:                 // This case helps us avoiding visiting invariant methods
62:
63:•                for (AFieldDeclIR f : node.getFields())
64:                 {
65:                         f.apply(decorator);
66:                 }
67:
68:•                for (AMethodDeclIR m : node.getMethods())
69:                 {
70:                         m.apply(decorator);
71:                 }
72:         }
73:
74:         public void handleField(AFieldDeclIR node)
75:         {
76:                 /**
77:                  * Values and record fields will be handled by this handler (not the state component field since its type is a
78:                  * record type) Example: val : char | Even = 5;
79:                  */
80:                 ADefaultClassDeclIR encClass = decorator.getJmlGen().getUtil().getEnclosingClass(node);
81:
82:•                if (encClass == null)
83:                 {
84:                         return;
85:                 }
86:
87:•                if (!decorator.getRecInfo().isRecField(node) && node.getFinal())
88:                 {
89:                         /**
90:                          * So at this point it must be a value defined in a module. No need to check if invariant checks are
91:                          * enabled.
92:                          */
93:
94:                         AbstractTypeInfo typeInfo = util.findTypeInfo(node.getType());
95:
96:                         /**
97:                          * Since we only allow value definitions to be initialized using literals they must be different from
98:                          * 'null'. However, there is a bug in OpenJML that sometimes cause the invariant check for a field to
99:                          * trigger before the field is properly initialized. As a work-around for this OpenJML bug, this trick
100:                          * guards against this bug, i.e. the static invariant check triggering pre-maturely. Since </br>
101:                          * fieldInitialised ==> invariant</br>
102:                          * =</br>
103:                          * !fieldInitialized || invariant</br>
104:                          * =</br>
105:                          * !(field != null) || invariant</br>
106:                          * =</br>
107:                          * field == null || invariant</br>
108:                          * </br>
109:                          * .. it suffices to simply consider the type as being optional.
110:                          */
111:                         typeInfo.setOptional(true);
112:
113:•                        if (proceed(typeInfo))
114:                         {
115:                                 AIdentifierVarExpIR var = getJmlGen().getJavaGen().getInfo().getExpAssistant().consIdVar(node.getName(), node.getType().clone());
116:
117:                                 List<String> invStrings = util.consJmlCheck(encClass, JmlGenerator.JML_PUBLIC, JmlGenerator.JML_STATIC_INV_ANNOTATION, false, typeInfo, var);
118:•                                for (String invStr : invStrings)
119:                                 {
120:                                         getAnnotator().appendMetaData(node, getAnnotator().consMetaData(invStr));
121:                                 }
122:                         } else
123:                         {
124:                                 // Since value definitions can only be initialised with literals there is no
125:                                 // need to guard against null (see JmlGenerator.initialIRConstructed)
126:                                 // if(varMayBeNull(node.getType()) && rightHandSideMayBeNull(node.getInitial()))
127:                                 // {
128:                                 // getAnnotator().appendMetaData(node, util.consValNotNullInvariant(node.getName()));
129:                                 // }
130:                         }
131:
132:                 }
133:                 /**
134:                  * No need to assert type consistency of record fields since this is handled by the record setter
135:                  */
136:         }
137:
138:         private JmlAnnotationHelper getAnnotator()
139:         {
140:                 return decorator.getJmlGen().getAnnotator();
141:         }
142:
143:         public void handleBlock(ABlockStmIR node) throws AnalysisException
144:         {
145:•                if (node.getLocalDefs().size() > 1)
146:                 {
147:                         LinkedList<AVarDeclIR> origDecls = new LinkedList<AVarDeclIR>(node.getLocalDefs());
148:
149:•                        for (int i = origDecls.size() - 1; i >= 0; i--)
150:                         {
151:                                 AVarDeclIR nextDecl = origDecls.get(i);
152:
153:                                 ABlockStmIR block = new ABlockStmIR();
154:                                 block.getLocalDefs().add(nextDecl);
155:
156:                                 node.getStatements().addFirst(block);
157:                         }
158:
159:•                        for (SStmIR stm : node.getStatements())
160:                         {
161:                                 stm.apply(decorator);
162:                         }
163:
164:                 } else
165:                 {
166:•                        if (!node.getLocalDefs().isEmpty())
167:                         {
168:                                 node.getLocalDefs().getFirst().apply(decorator);
169:                         }
170:
171:•                        for (SStmIR stm : node.getStatements())
172:                         {
173:                                 stm.apply(decorator);
174:                         }
175:                 }
176:         }
177:
178:         public void handleReturn(AReturnStmIR node) throws AnalysisException
179:         {
180:                 /**
181:                  * The idea is to extract the return value to variable and return that variable. Then it becomes the
182:                  * responsibility of the variable declaration case to assert if the named invariant type is violated.
183:                  */
184:                 SExpIR exp = node.getExp();
185:
186:                 AMethodDeclIR encMethod = decorator.getJmlGen().getUtil().getEnclosingMethod(node);
187:
188:•                if (encMethod == null)
189:                 {
190:                         return;
191:                 }
192:
193:                 STypeIR returnType = encMethod.getMethodType().getResult();
194:
195:                 AbstractTypeInfo typeInfo = util.findTypeInfo(returnType);
196:
197:•                if (!proceed(typeInfo))
198:                 {
199:                         return;
200:                 }
201:
202:                 String name = getInfo().getTempVarNameGen().nextVarName(RET_VAR_NAME_PREFIX);
203:                 AIdentifierPatternIR id = getInfo().getPatternAssistant().consIdPattern(name);
204:
205:                 AIdentifierVarExpIR varExp = getInfo().getExpAssistant().consIdVar(name, returnType.clone());
206:                 getTransAssist().replaceNodeWith(exp, varExp);
207:
208:                 AVarDeclIR varDecl = getInfo().getDeclAssistant().consLocalVarDecl(returnType.clone(), id, exp.clone());
209:                 ABlockStmIR replBlock = new ABlockStmIR();
210:                 replBlock.getLocalDefs().add(varDecl);
211:
212:                 getTransAssist().replaceNodeWith(node, replBlock);
213:
214:                 replBlock.getStatements().add(node);
215:                 varDecl.apply(decorator);
216:         }
217:
218:         public void handleMethod(AMethodDeclIR node) throws AnalysisException
219:         {
220:•                if (!treatMethod(node))
221:                 {
222:                         return;
223:                 }
224:
225:                 // Upon entering the method, assert that the parameters are valid wrt. their named invariant types.
226:
227:                 ABlockStmIR replBody = new ABlockStmIR();
228:•                for (AFormalParamLocalParamIR param : node.getFormalParams())
229:                 {
230:                         AbstractTypeInfo typeInfo = util.findTypeInfo(param.getType());
231:
232:•                        if (proceed(typeInfo))
233:                         {
234:                                 ADefaultClassDeclIR encClass = decorator.getJmlGen().getUtil().getEnclosingClass(node);
235:
236:•                                if (encClass == null)
237:                                 {
238:                                         continue;
239:                                 }
240:
241:                                 String varNameStr = decorator.getJmlGen().getUtil().getName(param.getPattern());
242:
243:•                                if (varNameStr == null)
244:                                 {
245:                                         continue;
246:                                 }
247:
248:                                 SVarExpIR var = getInfo().getExpAssistant().consIdVar(varNameStr, param.getType().clone());
249:
250:                                 /**
251:                                  * Upon entering a record setter it is necessary to check if invariants checks are enabled before
252:                                  * checking the parameter
253:                                  */
254:                                 List<AMetaStmIR> as = util.consAssertStm(typeInfo, encClass, var, node, decorator.getRecInfo());
255:•                                for (AMetaStmIR a : as)
256:                                 {
257:                                         replBody.getStatements().add(a);
258:                                 }
259:                         }
260:                 }
261:
262:                 SStmIR body = node.getBody();
263:                 getTransAssist().replaceNodeWith(body, replBody);
264:                 replBody.getStatements().add(body);
265:                 body.apply(decorator);
266:         }
267:
268:         public List<AMetaStmIR> handleMapSeq(AMapSeqUpdateStmIR node)
269:         {
270:                 // TODO: Consider this for the atomic statement
271:
272:                 SExpIR col = node.getCol();
273:
274:•                if (!(col instanceof SVarExpIR))
275:                 {
276:                         log.error("Expected collection to be a variable expression at this point. Got: "
277:                                         + col);
278:                         return null;
279:                 }
280:
281:                 SVarExpIR var = (SVarExpIR) col;
282:
283:•                if (varMayBeNull(var.getType()))
284:                 {
285:                         // The best we can do is to assert that the map/seq subject to modification is
286:                         // not null although we eventually get the null pointer exception, e.g.
287:                         //
288:                         // //@ azzert m != null
289:                         // Utils.mapSeqUpdate(m,1L,1L);
290:                         AMetaStmIR assertNotNull = util.consVarNotNullAssert(var.getName());
291:
292:                         ABlockStmIR replStm = new ABlockStmIR();
293:                         getTransAssist().replaceNodeWith(node, replStm);
294:                         replStm.getStatements().add(assertNotNull);
295:                         replStm.getStatements().add(node);
296:                 }
297:
298:                 AbstractTypeInfo typeInfo = util.findTypeInfo(var.getType());
299:
300:•                if (proceed(typeInfo))
301:                 {
302:                         ADefaultClassDeclIR enclosingClass = decorator.getJmlGen().getUtil().getEnclosingClass(node);
303:
304:•                        if (enclosingClass == null)
305:                         {
306:                                 return null;
307:                         }
308:
309:•                        if (col instanceof SVarExpIR)
310:                         {
311:                                 /**
312:                                  * Updates to fields in record setters need to check if invariants checks are enabled
313:                                  */
314:                                 return util.consAssertStm(typeInfo, enclosingClass, var, node, decorator.getRecInfo());
315:                         }
316:                 }
317:
318:                 return null;
319:         }
320:
321:         public List<AMetaStmIR> handleVarDecl(AVarDeclIR node)
322:         {
323:                 // Examples:
324:                 // let x : Even = 1 in ...
325:                 // (dcl y : Even | nat := 2; ...)
326:
327:•                if (getInfo().getExpAssistant().isUndefined(node.getExp()))
328:                 {
329:                         return null;
330:                 }
331:
332:                 AbstractTypeInfo typeInfo = util.findTypeInfo(node.getType());
333:
334:•                if (proceed(typeInfo))
335:                 {
336:                         String name = decorator.getJmlGen().getUtil().getName(node.getPattern());
337:
338:•                        if (name == null)
339:                         {
340:                                 return null;
341:                         }
342:
343:                         ADefaultClassDeclIR enclosingClass = node.getAncestor(ADefaultClassDeclIR.class);
344:
345:•                        if (enclosingClass == null)
346:                         {
347:                                 return null;
348:                         }
349:
350:                         AIdentifierVarExpIR var = getJmlGen().getJavaGen().getInfo().getExpAssistant().consIdVar(name, node.getType().clone());
351:
352:                         /**
353:                          * We do not really need to check if invariant checks are enabled because local variable declarations are
354:                          * not expected to be found inside record accessors
355:                          */
356:                         return util.consAssertStm(typeInfo, enclosingClass, var, node, decorator.getRecInfo());
357:                 }
358:
359:                 return null;
360:         }
361:
362:         public List<AMetaStmIR> handleCallObj(ACallObjectExpStmIR node)
363:         {
364:                 /**
365:                  * Handling of setter calls to masked records. This will happen for cases like T = R ... ; R :: x : int;
366:                  */
367:                 SExpIR recObj = node.getObj();
368:
369:•                if (recObj instanceof ACastUnaryExpIR)
370:                 {
371:                         recObj = ((ACastUnaryExpIR) recObj).getExp();
372:                 }
373:
374:•                if (recObj instanceof SVarExpIR)
375:                 {
376:                         SVarExpIR recObjVar = (SVarExpIR) recObj;
377:
378:•                        if (varMayBeNull(recObj.getType()))
379:                         {
380:                                 // The best we can do is to assert that the record subject to modification is
381:                                 // not null although we eventually get the null pointer exception, e.g.
382:                                 //
383:                                 // //@ azzert rec != null
384:                                 // rec.set_x(5);
385:                                 AMetaStmIR assertNotNull = util.consVarNotNullAssert(recObjVar.getName());
386:
387:                                 ABlockStmIR replStm = new ABlockStmIR();
388:                                 getTransAssist().replaceNodeWith(node, replStm);
389:                                 replStm.getStatements().add(assertNotNull);
390:                                 replStm.getStatements().add(node);
391:
392:                                 return null;
393:                         }
394:
395:                         AbstractTypeInfo typeInfo = util.findTypeInfo(recObj.getType());
396:
397:•                        if (proceed(typeInfo))
398:                         {
399:                                 ADefaultClassDeclIR encClass = decorator.getJmlGen().getUtil().getEnclosingClass(node);
400:
401:•                                if (encClass == null)
402:                                 {
403:                                         return null;
404:                                 }
405:
406:                                 /**
407:                                  * Since setter calls can occur inside a record in the context of an atomic statement blocks we need to
408:                                  * check if invariant checks are enabled
409:                                  */
410:                                 return util.consAssertStm(typeInfo, encClass, recObjVar, node, decorator.getRecInfo());
411:                         }
412:                 } else
413:                 {
414:                         log.error("Found unexpected record object of call expression statement inside atomic statement block. Target found: "
415:                                         + recObj);
416:                 }
417:
418:                 return null;
419:         }
420:
421:         public void handleAssign(AAssignToExpStmIR node)
422:         {
423:                 // <target> := atomic_tmp;
424:
425:                 /*
426:                  * Note that assignment to targets that are of type AFieldNumberExpIR, i.e. tuples (e.g. tup.#1 := 5) is not
427:                  * allowed in VDM.
428:                  */
429:
430:                 SExpIR target = node.getTarget();
431:
432:•                if (!(target instanceof SVarExpIR))
433:                 {
434:                         log.error("By now all assignments should have simple variable expression as target. Got: "
435:                                         + target);
436:                         return;
437:                 }
438:
439:                 SVarExpIR var = (SVarExpIR) target;
440:
441:                 AbstractTypeInfo typeInfo = util.findTypeInfo(node.getTarget().getType());
442:
443:•                if (proceed(typeInfo))
444:                 {
445:                         ADefaultClassDeclIR encClass = decorator.getJmlGen().getUtil().getEnclosingClass(node);
446:
447:•                        if (encClass == null)
448:                         {
449:                                 return;
450:                         }
451:
452:                         /**
453:                          * Since assignments can occur inside record setters in the context of an atomic statement block we need to
454:                          * check if invariant checks are enabled
455:                          */
456:                         List<AMetaStmIR> asserts = util.consAssertStm(typeInfo, encClass, var, node, decorator.getRecInfo());
457:
458:•                        for (AMetaStmIR a : asserts)
459:                         {
460:                                 addAssert(node, a);
461:                         }
462:                 }
463:         }
464:
465:         public ABlockStmIR getEncBlockStm(AVarDeclIR varDecl)
466:         {
467:                 INode parent = varDecl.parent();
468:
469:•                if (parent instanceof ABlockStmIR)
470:                 {
471:                         ABlockStmIR parentBlock = (ABlockStmIR) varDecl.parent();
472:
473:•                        if (!parentBlock.getLocalDefs().contains(varDecl))
474:                         {
475:                                 log.error("Expected local variable declaration to be "
476:                                                 + "one of the local variable declarations of "
477:                                                 + "the parent statement block");
478:                                 return null;
479:                         }
480:
481:•                        if (parentBlock.getLocalDefs().size() > 1)
482:                         {
483:                                 // The block statement case method should have ensured that the size == 1
484:                                 log.error("Expected only a single local declaration in "
485:                                                 + "the parent block at this point");
486:                                 return null;
487:                         }
488:
489:                         return parentBlock;
490:•                } else if (parent instanceof AForLoopStmIR)
491:                 {
492:                         // Do nothing
493:                         return null;
494:                 } else
495:                 {
496:                         log.error("Expected parent of local variable "
497:                                         + "declaration to be a statement block. Got: "
498:                                         + varDecl.parent());
499:                         return null;
500:                 }
501:         }
502:
503:         private TransAssistantIR getTransAssist()
504:         {
505:                 return decorator.getJmlGen().getJavaGen().getTransAssistant();
506:         }
507:
508:         private IRInfo getInfo()
509:         {
510:                 return decorator.getJmlGen().getJavaGen().getInfo();
511:         }
512:
513:         public JmlGenerator getJmlGen()
514:         {
515:                 return decorator.getJmlGen();
516:         }
517:
518:         public List<AMetaStmIR> consAsserts(AIdentifierVarExpIR var)
519:         {
520:                 AbstractTypeInfo typeInfo = util.findTypeInfo(var.getType());
521:
522:•                if (!proceed(typeInfo))
523:                 {
524:                         return null;
525:                 }
526:
527:                 ADefaultClassDeclIR encClass = decorator.getStateDesInfo().getEnclosingClass(var);
528:
529:•                if (encClass == null)
530:                 {
531:                         return null;
532:                 }
533:
534:                 /**
535:                  * Normalisation of state designators will never occur inside record classes so really there is no need to check
536:                  * if invariant checks are enabled
537:                  */
538:                 return util.consAssertStm(typeInfo, encClass, var, var, decorator.getRecInfo());
539:         }
540:
541:         public boolean rightHandSideMayBeNull(SExpIR exp)
542:         {
543:                 IsValChecker checker = new IsValChecker();
544:
545:                 try
546:                 {
547:•                        return !exp.apply(checker);
548:                 } catch (AnalysisException e)
549:                 {
550:                         e.printStackTrace();
551:                         return false;
552:                 }
553:         }
554:
555:         private boolean varMayBeNull(STypeIR type)
556:         {
557:•                return treatMethod(type)
558:•                                && !getInfo().getTypeAssistant().allowsNull(type);
559:         }
560:
561:         private boolean treatMethod(INode node)
562:         {
563:•                if (inModuleToStringMethod(node))
564:                 {
565:                         return false;
566:                 }
567:
568:                 // Some of the record methods inherited from object use native java type that can never be null
569:
570:•                if (decorator.getRecInfo().inRec(node))
571:                 {
572:•                        if (!(decorator.getRecInfo().inAccessor(node)
573:•                                        || decorator.getRecInfo().inRecConstructor(node)))
574:                         {
575:                                 return false;
576:                         }
577:                 }
578:
579:                 return true;
580:         }
581:
582:         private boolean inModuleToStringMethod(INode type)
583:         {
584:                 AMethodDeclIR m = type.getAncestor(AMethodDeclIR.class);
585:
586:•                if (m == null)
587:                 {
588:                         return false;
589:                 }
590:
591:•                if (m.getTag() instanceof IRGeneratedTag
592:•                                && m.getName().equals("toString"))
593:                 {
594:                         return true;
595:                 }
596:
597:                 return false;
598:         }
599:
600:         private void addAssert(AAssignToExpStmIR node, AMetaStmIR assertStm)
601:         {
602:                 ABlockStmIR replStm = new ABlockStmIR();
603:                 getJmlGen().getJavaGen().getTransAssistant().replaceNodeWith(node, replStm);
604:                 replStm.getStatements().add(node);
605:                 replStm.getStatements().add(assertStm);
606:         }
607:
608:         public TypePredUtil getTypePredUtil()
609:         {
610:                 return util;
611:         }
612:
613:         private boolean proceed(AbstractTypeInfo typeInfo)
614:         {
615:•                return !(typeInfo instanceof UnknownLeaf);
616:         }
617: }