Skip to content

Better ImmutableList #3816

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wadoon wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Better ImmutableList #3816

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
06545b7
better and faster ImmutableList
wadoon Apr 25, 2026
3e92daf
added test cases
wadoon May 16, 2026
818f148
fix rebasing
wadoon May 16, 2026
7928a90
fix wrong usage of take()
wadoon May 17, 2026
00c9abe
spotless
wadoon May 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
3 changes: 1 addition & 2 deletions key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/ProofObligationVars.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@
import org.key_project.logic.op.Function;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import org.jspecify.annotations.Nullable;

Expand Down Expand Up @@ -135,7 +134,7 @@ private JTerm buildExceptionParameter(Services services) {
*/
private ImmutableList<JTerm> buildFormalParamVars(Services services)
throws IllegalArgumentException {
ImmutableList<JTerm> formalParamVars = ImmutableSLList.nil();
ImmutableList<JTerm> formalParamVars = ImmutableList.nil();
for (JTerm param : pre.localVars) {
ProgramVariable paramVar = param.op(ProgramVariable.class);
ProgramElementName pen = new ProgramElementName("_" + paramVar.name());
Expand Down
7 changes: 3 additions & 4 deletions ...re.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/ExhaustiveProofMacro.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@
import org.key_project.prover.sequent.PosInOccurrence;
import org.key_project.prover.sequent.Sequent;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
* The abstract class ExhaustiveProofMacro can be used to create compound macros which either apply
Expand All @@ -40,7 +39,7 @@ private PosInOccurrence getApplicablePosInOcc(Proof proof,
ProofMacro macro) {
if (posInOcc == null || posInOcc.subTerm() == null) {
return null;
} else if (macro.canApplyTo(proof, ImmutableSLList.<Goal>nil().prepend(goal), posInOcc)) {
} else if (macro.canApplyTo(proof, ImmutableList.<Goal>nil().prepend(goal), posInOcc)) {
return posInOcc;
} else {
final var subTerm = posInOcc.subTerm();
Expand Down Expand Up @@ -124,7 +123,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
if (!isCached) {
// node has not been checked before, so do it
boolean canBeApplied =
canApplyTo(proof, ImmutableSLList.<Goal>nil().prepend(goal), posInOcc);
canApplyTo(proof, ImmutableList.<Goal>nil().prepend(goal), posInOcc);
if (!canBeApplied) {
// canApplyTo checks all open goals. thus, if it returns
// false, then this macro is not applicable at all and
Expand All @@ -143,7 +142,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
pml.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, getName(), 0));
synchronized (macro) {
// wait for macro to terminate
info = macro.applyTo(uic, proof, ImmutableSLList.<Goal>nil().prepend(goal),
info = macro.applyTo(uic, proof, ImmutableList.<Goal>nil().prepend(goal),
applicableAt, pml);
}
pml.taskFinished(info);
Expand Down
3 changes: 1 addition & 2 deletions .../src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicBlockExecutionSnippet.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;


/**
Expand All @@ -33,7 +32,7 @@ class BasicBlockExecutionSnippet extends ReplaceAndRegisterMethod implements Fac
@Override
public JTerm produce(BasicSnippetData d, ProofObligationVars poVars)
throws UnsupportedOperationException {
ImmutableList<JTerm> posts = ImmutableSLList.nil();
ImmutableList<JTerm> posts = ImmutableList.nil();
if (poVars.post.self != null) {
posts = posts.append(d.tb.equals(poVars.post.self, poVars.pre.self));
}
Expand Down
3 changes: 1 addition & 2 deletions ...w/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopExecutionSnippet.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,15 +20,14 @@
import de.uka.ilkd.key.speclang.LoopSpecification;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.collection.Pair;

public class BasicLoopExecutionSnippet extends ReplaceAndRegisterMethod implements FactoryMethod {

@Override
public JTerm produce(BasicSnippetData d, ProofObligationVars poVars)
throws UnsupportedOperationException {
ImmutableList<JTerm> posts = ImmutableSLList.nil();
ImmutableList<JTerm> posts = ImmutableList.nil();
if (poVars.post.self != null) {
posts = posts.append(d.tb.equals(poVars.post.self, poVars.pre.self));
}
Expand Down
5 changes: 2 additions & 3 deletions ...re.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@
import de.uka.ilkd.key.util.MiscTools;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.collection.ImmutableSet;


Expand Down Expand Up @@ -150,7 +149,7 @@ public Class<?> getType() {
// add guard term to information flow specs (necessary for soundness)
// and add the modified specs to the table
ImmutableList<InfFlowSpec> infFlowSpecs = invariant.getInfFlowSpecs(services);
ImmutableList<InfFlowSpec> modifiedSpecs = ImmutableSLList.nil();
ImmutableList<InfFlowSpec> modifiedSpecs = ImmutableList.nil();
for (InfFlowSpec infFlowSpec : infFlowSpecs) {
ImmutableList<JTerm> modifiedPreExps = infFlowSpec.preExpressions.append(guardTerm);
ImmutableList<JTerm> modifiedPostExps = infFlowSpec.postExpressions.append(guardTerm);
Expand Down Expand Up @@ -234,7 +233,7 @@ public Class<?> getType() {


private ImmutableList<JTerm> toTermList(ImmutableSet<LocationVariable> vars) {
ImmutableList<JTerm> result = ImmutableSLList.nil();
ImmutableList<JTerm> result = ImmutableList.nil();
for (ProgramVariable v : vars) {
result = result.append(tb.var(v));
}
Expand Down
3 changes: 1 addition & 2 deletions ...c/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSymbolicExecutionSnippet.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,6 @@

import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
*
Expand All @@ -47,7 +46,7 @@ public JTerm produce(BasicSnippetData d, ProofObligationVars poVars)
assert poVars.exceptionParameter.op() instanceof LocationVariable
: "Something is wrong with the catch variable";

ImmutableList<JTerm> posts = ImmutableSLList.nil();
ImmutableList<JTerm> posts = ImmutableList.nil();
if (poVars.post.self != null) {
posts = posts.append(d.tb.equals(poVars.post.self, poVars.pre.self));
}
Expand Down
3 changes: 1 addition & 2 deletions ...va/de/uka/ilkd/key/informationflow/po/snippet/InfFlowContractAppInOutRelationSnippet.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
import de.uka.ilkd.key.util.InfFlowSpec;

import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
*
Expand All @@ -27,7 +26,7 @@ protected JTerm buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1,
InfFlowSpec infFlowSpec2, BasicSnippetData d, ProofObligationVars vs1,
ProofObligationVars vs2, JTerm eqAtLocsTerm) {
// build equalities for newObjects terms
ImmutableList<JTerm> newObjEqs = ImmutableSLList.nil();
ImmutableList<JTerm> newObjEqs = ImmutableList.nil();
Iterator<JTerm> newObjects1It = infFlowSpec1.newObjects.iterator();
Iterator<JTerm> newObjects2It = infFlowSpec2.newObjects.iterator();
for (int i = 0; i < infFlowSpec1.newObjects.size(); i++) {
Expand Down
5 changes: 2 additions & 3 deletions ...in/java/de/uka/ilkd/key/informationflow/po/snippet/InfFlowInputOutputRelationSnippet.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@
import org.key_project.logic.Term;
import org.key_project.logic.op.Function;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
* Generate term "self != null".
Expand Down Expand Up @@ -97,7 +96,7 @@ private JTerm buildInputRelation(BasicSnippetData d, ProofObligationVars vs1,
private JTerm buildOutputRelation(BasicSnippetData d, ProofObligationVars vs1,
ProofObligationVars vs2, InfFlowSpec infFlowSpec1, InfFlowSpec infFlowSpec2) {
// build equalities for post expressions
ImmutableList<JTerm> eqAtLocs = ImmutableSLList.nil();
ImmutableList<JTerm> eqAtLocs = ImmutableList.nil();

Iterator<JTerm> postExp1It = infFlowSpec1.postExpressions.iterator();
Iterator<JTerm> postExp2It = infFlowSpec2.postExpressions.iterator();
Expand All @@ -123,7 +122,7 @@ protected JTerm buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1,
InfFlowSpec infFlowSpec2, BasicSnippetData d, ProofObligationVars vs1,
ProofObligationVars vs2, JTerm eqAtLocsTerm) {
// build equalities for newObjects terms
ImmutableList<JTerm> newObjEqs = ImmutableSLList.nil();
ImmutableList<JTerm> newObjEqs = ImmutableList.nil();
Iterator<JTerm> newObjects1It = infFlowSpec1.newObjects.iterator();
Iterator<JTerm> newObjects2It = infFlowSpec2.newObjects.iterator();
for (int i = 0; i < infFlowSpec1.newObjects.size(); i++) {
Expand Down
7 changes: 3 additions & 4 deletions ...ow/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/ReplaceAndRegisterMethod.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@
import org.key_project.logic.op.Function;
import org.key_project.logic.op.QuantifiableVariable;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;


/**
Expand Down Expand Up @@ -78,15 +77,15 @@ final JTerm[] replace(JTerm[] terms, StateVars origVars, StateVars poVars, TermB

final InfFlowSpec replace(InfFlowSpec terms, StateVars origVars, StateVars poVars,
TermBuilder tb) {
ImmutableList<JTerm> resultPreExps = ImmutableSLList.nil();
ImmutableList<JTerm> resultPreExps = ImmutableList.nil();
for (JTerm t : terms.preExpressions) {
resultPreExps = resultPreExps.append(replace(t, origVars, poVars, tb));
}
ImmutableList<JTerm> resultPostExps = ImmutableSLList.nil();
ImmutableList<JTerm> resultPostExps = ImmutableList.nil();
for (JTerm t : terms.postExpressions) {
resultPostExps = resultPostExps.append(replace(t, origVars, poVars, tb));
}
ImmutableList<JTerm> resultNewObjecs = ImmutableSLList.nil();
ImmutableList<JTerm> resultNewObjecs = ImmutableList.nil();
for (JTerm t : terms.newObjects) {
resultNewObjecs = resultNewObjecs.append(replace(t, origVars, poVars, tb));
}
Expand Down
5 changes: 2 additions & 3 deletions .../main/java/de/uka/ilkd/key/informationflow/po/snippet/TwoStateMethodPredicateSnippet.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@
import org.key_project.logic.op.Function;
import org.key_project.logic.sort.Sort;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;


/**
Expand Down Expand Up @@ -118,8 +117,8 @@ abstract String generatePredicateName(IProgramMethod pm, StatementBlock block,
*/
private ImmutableList<JTerm> extractTermListForPredicate(IProgramMethod pm,
ProofObligationVars poVars, boolean hasMby) {
ImmutableList<JTerm> relevantPreVars = ImmutableSLList.nil();
ImmutableList<JTerm> relevantPostVars = ImmutableSLList.nil();
ImmutableList<JTerm> relevantPreVars = ImmutableList.nil();
ImmutableList<JTerm> relevantPostVars = ImmutableList.nil();

if (!pm.isStatic()) {
// self is relevant in the pre and post state for constructors
Expand Down
11 changes: 5 additions & 6 deletions key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@
import org.key_project.logic.sort.Sort;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import org.jspecify.annotations.Nullable;

Expand Down Expand Up @@ -65,7 +64,7 @@ public StateVars(JTerm self, JTerm guard, ImmutableList<JTerm> localVars, JTerm
this.heap = heap;
this.mbyAtPre = mbyAtPre;

ImmutableList<JTerm> terms = ImmutableSLList.nil();
ImmutableList<JTerm> terms = ImmutableList.nil();
terms = appendIfNotNull(terms, heap);
terms = appendIfNotNull(terms, self);
terms = appendIfNotNull(terms, guard);
Expand All @@ -75,7 +74,7 @@ public StateVars(JTerm self, JTerm guard, ImmutableList<JTerm> localVars, JTerm
terms = appendIfNotNull(terms, mbyAtPre);
termList = terms;

ImmutableList<JTerm> allTerms = ImmutableSLList.nil();
ImmutableList<JTerm> allTerms = ImmutableList.nil();
allTerms = allTerms.append(heap);
allTerms = allTerms.append(self);
allTerms = allTerms.append(guard);
Expand Down Expand Up @@ -148,7 +147,7 @@ public StateVars(StateVars orig, String postfix, Services services) {

private static ImmutableList<JTerm> copyVariables(ImmutableList<JTerm> ts, String postfix,
Services services) {
ImmutableList<JTerm> result = ImmutableSLList.nil();
ImmutableList<JTerm> result = ImmutableList.nil();
for (JTerm t : ts) {
result = result.append(copyVariable(t, postfix, services));
}
Expand Down Expand Up @@ -284,7 +283,7 @@ public static StateVars buildInfFlowPostVars(StateVars origPreVars, StateVars or
JTerm mbyAtPre = (origPreVars.mbyAtPre == origPostVars.mbyAtPre) ? preVars.mbyAtPre
: copyVariable(origPostVars.mbyAtPre, postfix, services);

ImmutableList<JTerm> localPostVars = ImmutableSLList.nil();
ImmutableList<JTerm> localPostVars = ImmutableList.nil();
Iterator<JTerm> origPreVarsIt = origPreVars.localVars.iterator();
Iterator<JTerm> localPreVarsIt = preVars.localVars.iterator();
for (JTerm origPostVar : origPostVars.localVars) {
Expand Down Expand Up @@ -390,7 +389,7 @@ static void register(Function f, Services services) {

static <T> ImmutableList<T> ops(ImmutableList<JTerm> terms, Class<T> opClass)
throws IllegalArgumentException {
ImmutableList<T> ops = ImmutableSLList.nil();
ImmutableList<T> ops = ImmutableList.nil();
for (JTerm t : terms) {
ops = ops.append(t.op(opClass));
}
Expand Down
5 changes: 2 additions & 3 deletions .../src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,6 @@
import org.key_project.prover.sequent.SequentFormula;
import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.collection.ImmutableSet;

import org.jspecify.annotations.Nullable;
Expand Down Expand Up @@ -422,7 +421,7 @@ protected static ImmutableList<JTerm> buildLocalOutsAtPre(ImmutableList<JTerm> v
return varTerms;
}
final TermBuilder tb = services.getTermBuilder();
ImmutableList<JTerm> renamedLocalOuts = ImmutableSLList.nil();
ImmutableList<JTerm> renamedLocalOuts = ImmutableList.nil();
for (JTerm varTerm : varTerms) {
assert varTerm.op() instanceof LocationVariable;

Expand All @@ -444,7 +443,7 @@ protected static ImmutableList<JTerm> buildLocalOutsAtPost(ImmutableList<JTerm>
return varTerms;
}
final TermBuilder tb = services.getTermBuilder();
ImmutableList<JTerm> renamedLocalOuts = ImmutableSLList.nil();
ImmutableList<JTerm> renamedLocalOuts = ImmutableList.nil();
for (JTerm varTerm : varTerms) {
assert varTerm.op() instanceof LocationVariable;

Expand Down
5 changes: 2 additions & 3 deletions ...infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,6 @@
import org.key_project.prover.sequent.PosInOccurrence;
import org.key_project.prover.sequent.SequentFormula;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import org.key_project.util.collection.ImmutableSet;
import org.key_project.util.collection.Pair;

Expand Down Expand Up @@ -298,7 +297,7 @@ private static ImmutableList<JTerm> buildLocalOutsAtPre(ImmutableList<JTerm> var
return varTerms;
}
final TermBuilder tb = services.getTermBuilder();
ImmutableList<JTerm> localOuts = ImmutableSLList.nil();
ImmutableList<JTerm> localOuts = ImmutableList.nil();
for (final JTerm varTerm : varTerms) {
assert varTerm.op() instanceof LocationVariable;

Expand All @@ -320,7 +319,7 @@ private static ImmutableList<JTerm> buildLocalOutsAtPost(ImmutableList<JTerm> va
return varTerms;
}
final TermBuilder tb = services.getTermBuilder();
ImmutableList<JTerm> localOuts = ImmutableSLList.nil();
ImmutableList<JTerm> localOuts = ImmutableList.nil();
for (final JTerm varTerm : varTerms) {
assert varTerm.op() instanceof LocationVariable;

Expand Down
3 changes: 1 addition & 2 deletions .../java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,6 @@
import org.key_project.prover.sequent.SequentChangeInfo;
import org.key_project.prover.sequent.SequentFormula;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import org.jspecify.annotations.NonNull;

Expand Down Expand Up @@ -92,7 +91,7 @@ protected void addToAntec(Semisequent semi, SequentChangeInfo currentSequent,
private void updateStrategyInfo(Goal goal, final JTerm applFormula) {
ImmutableList<JTerm> applFormulas = goal.getStrategyInfo(INF_FLOW_CONTRACT_APPL_PROPERTY);
if (applFormulas == null) {
applFormulas = ImmutableSLList.nil();
applFormulas = ImmutableList.nil();
}
applFormulas = applFormulas.append(applFormula);
StrategyInfoUndoMethod undo = strategyInfos -> {
Expand Down
9 changes: 4 additions & 5 deletions .../ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,6 @@
import org.key_project.prover.sequent.Sequent;
import org.key_project.prover.sequent.SequentFormula;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

/**
* Builds the rule which inserts information flow contract applications.
Expand Down Expand Up @@ -198,7 +197,7 @@ ProofObligationVars generateApplicationDataSVs(String schemaPrefix, ProofObligat
JTerm selfAtPostSV = (appData.pre.self == appData.post.self ? selfAtPreSV
: createTermSV(appData.post.self, schemaPrefix, services));

ImmutableList<JTerm> localVarsAtPostSVs = ImmutableSLList.nil();
ImmutableList<JTerm> localVarsAtPostSVs = ImmutableList.nil();
Iterator<JTerm> appDataPreLocalVarsIt = appData.pre.localVars.iterator();
Iterator<JTerm> schemaLocalVarsAtPreIt = localVarsAtPreSVs.iterator();
for (JTerm appDataPostLocalVar : appData.post.localVars) {
Expand Down Expand Up @@ -262,10 +261,10 @@ private Taclet genInfFlowContractApplTaclet(Goal goal, ProofObligationVars appDa
// create sequents
Sequent assumesSeq =
JavaDLSequentKit.createAnteSequent(
ImmutableSLList.singleton(new SequentFormula(schemaAssumes)));
ImmutableList.singleton(new SequentFormula(schemaAssumes)));
Sequent replaceWithSeq =
JavaDLSequentKit.createAnteSequent(
ImmutableSLList.singleton(new SequentFormula(replaceWithTerm)));
ImmutableList.singleton(new SequentFormula(replaceWithTerm)));

// create taclet
InfFlowContractAppRewriteTacletBuilder tacletBuilder =
Expand All @@ -276,7 +275,7 @@ private Taclet genInfFlowContractApplTaclet(Goal goal, ProofObligationVars appDa
new ApplicationRestriction(ApplicationRestriction.ANTECEDENT_POLARITY));
tacletBuilder.setIfSequent(assumesSeq);
RewriteTacletGoalTemplate goalTemplate = new RewriteTacletGoalTemplate(replaceWithSeq,
ImmutableSLList.nil(), schemaFind);
ImmutableList.nil(), schemaFind);
tacletBuilder.addTacletGoalTemplate(goalTemplate);
tacletBuilder.addRuleSet(new RuleSet(new Name(IF_CONTRACT_APPLICATION)));
tacletBuilder.setSurviveSmbExec(true);
Expand Down
3 changes: 1 addition & 2 deletions ...java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@
import org.key_project.logic.op.sv.SchemaVariable;
import org.key_project.logic.sort.Sort;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

import org.jspecify.annotations.NonNull;

Expand Down Expand Up @@ -53,7 +52,7 @@ protected AbstractInfFlowTacletBuilder(final Services services) {

ImmutableList<JTerm> createTermSV(ImmutableList<JTerm> ts, String schemaPrefix,
Services services) {
ImmutableList<JTerm> result = ImmutableSLList.nil();
ImmutableList<JTerm> result = ImmutableList.nil();
for (JTerm t : ts) {
result = result.append(createTermSV(t, schemaPrefix, services));
}
Expand Down
Loading
Loading