de.uka.ilkd.key.informationflow.po

Class IFProofObligationVars

java.lang.Object

de.uka.ilkd.key.informationflow.po.IFProofObligationVars

public class IFProofObligationVars
extends java.lang.Object

This class contains the set of four sets of ProofObligationVars necessary for information flow proofs.

Author:

christoph

Field Summary

Fields

Modifier and Type	Field and Description
ProofObligationVars	c1
ProofObligationVars	c2
private java.util.Map<ProofObligationVars,java.util.Map<Term,Term>>	infFlowToSymbExecVarsMaps
ProofObligationVars	symbExecVars

Constructor Summary

Constructors

Constructor and Description
IFProofObligationVars(ProofObligationVars c1, ProofObligationVars c2, ProofObligationVars symbExecVars)
IFProofObligationVars(ProofObligationVars symbExecVars, Services services)

Method Summary

Modifier and Type	Method and Description
java.util.Map<Term,Term>	getMapFor(ProofObligationVars vars)
IFProofObligationVars	labelHeapAtPreAsAnonHeapFunc()
private void	linkStateVarsToCopies(StateVars ifVars, StateVars seVars, java.util.Map<Term,Term> map)
private void	linkSymbExecVarsToCopies()
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

c1

public final ProofObligationVars c1

c2

public final ProofObligationVars c2

symbExecVars

public final ProofObligationVars symbExecVars

infFlowToSymbExecVarsMaps

private final java.util.Map<ProofObligationVars,java.util.Map<Term,Term>> infFlowToSymbExecVarsMaps

Constructor Detail

IFProofObligationVars

public IFProofObligationVars(ProofObligationVars symbExecVars,
                             Services services)

IFProofObligationVars

public IFProofObligationVars(ProofObligationVars c1,
                             ProofObligationVars c2,
                             ProofObligationVars symbExecVars)

Method Detail

labelHeapAtPreAsAnonHeapFunc

public IFProofObligationVars labelHeapAtPreAsAnonHeapFunc()

linkSymbExecVarsToCopies

private void linkSymbExecVarsToCopies()

linkStateVarsToCopies

private void linkStateVarsToCopies(StateVars ifVars,
                                   StateVars seVars,
                                   java.util.Map<Term,Term> map)

getMapFor

public java.util.Map<Term,Term> getMapFor(ProofObligationVars vars)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object