Package: AtomicAssertTrans

AtomicAssertTrans

nameinstructionbranchcomplexitylinemethod
AtomicAssertTrans(JmlGenerator)
M: 0 C: 9
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 4
100%
M: 0 C: 1
100%
addPostAtomicCheck(AMetaStmIR)
M: 0 C: 10
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 3
100%
M: 0 C: 1
100%
caseAAtomicStmIR(AAtomicStmIR)
M: 0 C: 61
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 12
100%
M: 0 C: 1
100%
consInvChecksStm(boolean, ADefaultClassDeclIR)
M: 0 C: 36
100%
M: 0 C: 0
100%
M: 0 C: 1
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
consMetaStm(String)
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%
contains(AMetaStmIR)
M: 0 C: 25
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 5
100%
M: 0 C: 1
100%
getJmlGen()
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%
inAtomic()
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%

Coverage

1: package org.overture.codegen.vdm2jml.predgen;
2:
3: import java.util.LinkedList;
4: import java.util.List;
5:
6: import org.overture.ast.util.ClonableString;
7: import org.overture.codegen.ir.SStmIR;
8: import org.overture.codegen.ir.analysis.AnalysisException;
9: import org.overture.codegen.ir.analysis.DepthFirstAnalysisAdaptor;
10: import org.overture.codegen.ir.declarations.ADefaultClassDeclIR;
11: import org.overture.codegen.ir.statements.AAtomicStmIR;
12: import org.overture.codegen.ir.statements.AMetaStmIR;
13: import org.overture.codegen.vdm2jml.JmlGenerator;
14:
15: public abstract class AtomicAssertTrans extends DepthFirstAnalysisAdaptor
16: {
17:         protected JmlGenerator jmlGen;
18:         private List<AMetaStmIR> recVarChecks = null;
19:
20:         public AtomicAssertTrans(JmlGenerator jmlGen)
21:         {
22:                 this.jmlGen = jmlGen;
23:         }
24:
25:         @Override
26:         public void caseAAtomicStmIR(AAtomicStmIR node) throws AnalysisException
27:         {
28:                 recVarChecks = new LinkedList<AMetaStmIR>();
29:
30:•                for (SStmIR stm : node.getStatements())
31:                 {
32:                         stm.apply(this);
33:                 }
34:
35:                 ADefaultClassDeclIR encClass = node.getAncestor(ADefaultClassDeclIR.class);
36:
37:                 node.getStatements().addFirst(consInvChecksStm(false, encClass));
38:                 node.getStatements().add(consInvChecksStm(true, encClass));
39:
40:•                for (AMetaStmIR as : recVarChecks)
41:                 {
42:                         node.getStatements().add(as);
43:                 }
44:
45:                 recVarChecks = null;
46:         }
47:
48:         public AMetaStmIR consMetaStm(String str)
49:         {
50:                 AMetaStmIR assertion = new AMetaStmIR();
51:                 jmlGen.getAnnotator().appendMetaData(assertion, jmlGen.getAnnotator().consMetaData(str));
52:
53:                 return assertion;
54:         }
55:
56:         protected AMetaStmIR consInvChecksStm(boolean val,
57:                         ADefaultClassDeclIR encClass)
58:         {
59:                 AMetaStmIR setStm = new AMetaStmIR();
60:
61:                 String setStmStr = String.format(JmlGenerator.JML_SET_INV_CHECKS, this.jmlGen.getAnnotator().consInvChecksOnNameEncClass(encClass), val);
62:                 List<ClonableString> setMetaData = jmlGen.getAnnotator().consMetaData(setStmStr);
63:                 jmlGen.getAnnotator().appendMetaData(setStm, setMetaData);
64:
65:                 return setStm;
66:         }
67:
68:         public JmlGenerator getJmlGen()
69:         {
70:                 return jmlGen;
71:         }
72:
73:         public void addPostAtomicCheck(AMetaStmIR check)
74:         {
75:•                if (!contains(check))
76:                 {
77:                         recVarChecks.add(check);
78:                 }
79:         }
80:
81:         private boolean contains(AMetaStmIR check)
82:         {
83:•                for (AMetaStmIR as : recVarChecks)
84:                 {
85:•                        if (jmlGen.getJavaGen().getInfo().getStmAssistant().equal(as, check))
86:                         {
87:                                 return true;
88:                         }
89:                 }
90:
91:                 return false;
92:         }
93:
94:         public boolean inAtomic()
95:         {
96:•                return recVarChecks != null;
97:         }
98: }