Package: ProofObligationGenerator

ProofObligationGenerator

nameinstructionbranchcomplexitylinemethod
ProofObligationGenerator()
M: 3 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 1 C: 0
0%
M: 1 C: 0
0%
generateProofObligations(INode)
M: 14 C: 0
0%
M: 0 C: 0
100%
M: 1 C: 0
0%
M: 3 C: 0
0%
M: 1 C: 0
0%
generateProofObligations(List)
M: 0 C: 29
100%
M: 0 C: 2
100%
M: 0 C: 2
100%
M: 0 C: 5
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.pog.pub;
2:
3: import java.util.List;
4:
5: import org.overture.ast.analysis.AnalysisException;
6: import org.overture.ast.node.INode;
7: import org.overture.pog.contexts.POContextStack;
8: import org.overture.pog.obligation.ProofObligationList;
9: import org.overture.pog.visitors.PogVisitor;
10:
11: public class ProofObligationGenerator
12: {
13:         public static IProofObligationList generateProofObligations(INode root)
14:                         throws AnalysisException
15:         {
16:                 PogVisitor pog = new PogVisitor();
17:                 IProofObligationList r = root.apply(pog, new POContextStack());
18:                 return r;
19:         }
20:
21:         public static IProofObligationList generateProofObligations(
22:                         List<INode> sources) throws AnalysisException
23:         {
24:                 IProofObligationList r = new ProofObligationList();
25:•                for (INode node : sources)
26:                 {
27:                         r.addAll(node.apply(new PogVisitor(), new POContextStack()));
28:                 }
29:
30:                 return r;
31:         }
32:
33: }