Package: OperationCallObligation

OperationCallObligation

nameinstructionbranchcomplexitylinemethod
OperationCallObligation(ACallStm, SOperationDefinitionBase, IPOContextStack, IPogAssistantFactory)
M: 0 C: 90
100%
M: 0 C: 4
100%
M: 0 C: 3
100%
M: 0 C: 14
100%
M: 0 C: 1
100%

Coverage

1: package org.overture.pog.obligation;
2:
3: import java.util.LinkedList;
4: import java.util.List;
5:
6: import org.overture.ast.analysis.AnalysisException;
7: import org.overture.ast.definitions.SOperationDefinitionBase;
8: import org.overture.ast.expressions.PExp;
9: import org.overture.ast.intf.lex.ILexNameToken;
10: import org.overture.ast.patterns.PPattern;
11: import org.overture.ast.statements.ACallStm;
12: import org.overture.pog.pub.IPOContextStack;
13: import org.overture.pog.pub.IPogAssistantFactory;
14: import org.overture.pog.pub.POType;
15: import org.overture.pog.utility.Substitution;
16:
17: public class OperationCallObligation extends ProofObligation
18: {
19:
20:         public OperationCallObligation(ACallStm stm, SOperationDefinitionBase def,
21:                         IPOContextStack ctxt, IPogAssistantFactory af)
22:                         throws AnalysisException
23:         {
24:                 super(stm, POType.OP_CALL, ctxt, stm.getLocation(), af);
25:
26:                 // cannot quote pre-cond so we spell it out with rewritten arguments
27:                 List<Substitution> subs = new LinkedList<Substitution>();
28:
29:•                for (int i = 0; i < stm.getArgs().size(); i++)
30:                 {
31:                         PPattern orig = def.getPredef().getParamPatternList().get(0).get(i);
32:                         ILexNameToken origName = af.createPPatternAssistant(def.getLocation().getModule()).getAllVariableNames(orig).get(0).clone();
33:                         PExp new_exp = stm.getArgs().get(0);
34:                         subs.add(new Substitution(origName, new_exp));
35:
36:                 }
37:                 PExp pre_exp = def.getPrecondition().clone();
38:
39:•                for (Substitution sub : subs)
40:                 {
41:                         pre_exp = pre_exp.clone().apply(af.getVarSubVisitor(), sub);
42:
43:                 }
44:
45:                 stitch = pre_exp;
46:                 valuetree.setPredicate(ctxt.getPredWithContext(pre_exp));
47:         }
48:
49:         /**
50:          *
51:          */
52:         private static final long serialVersionUID = 1L;
53:
54: }