summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/LinearSets.cs108
-rw-r--r--Source/Model/Model.cs83
-rw-r--r--Source/Predication/SmartBlockPredicator.cs37
-rw-r--r--Source/Predication/UniformityAnalyser.cs80
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs14
5 files changed, 268 insertions, 54 deletions
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index c092139d..63a76eb2 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -414,6 +414,10 @@ namespace Microsoft.Boogie
foreach (LinearDomain domain in linearDomains.Values)
{
program.TopLevelDeclarations.Add(domain.allocator);
+ foreach (Axiom axiom in domain.axioms)
+ {
+ program.TopLevelDeclarations.Add(axiom);
+ }
}
}
@@ -596,6 +600,7 @@ namespace Microsoft.Boogie
public Function mapOrBool;
public Function mapImpBool;
public Function mapConstBool;
+ public List<Axiom> axioms;
public LinearDomain(Program program, Variable var, string domainName)
{
@@ -606,6 +611,7 @@ namespace Microsoft.Boogie
this.elementType = mapType.Arguments[0];
}
this.allocator = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("allocator_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool)));
+ this.axioms = new List<Axiom>();
MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool);
MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Int);
@@ -613,29 +619,121 @@ namespace Microsoft.Boogie
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapOrBool.AddAttribute("builtin", "MapOr");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapOrBool.AddAttribute("builtin", "MapOr");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new ExprSeq(aie, bie)), xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, b, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapImpBool = new Function(Token.NoToken, "linear@MapImp",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapImpBool.AddAttribute("builtin", "MapImp");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapImpBool.AddAttribute("builtin", "MapImp");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new ExprSeq(aie, bie)), xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, b, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapConstBool = new Function(Token.NoToken, "linear@MapConstBool",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapConstBool.AddAttribute("builtin", "MapConst");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstBool.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.True)), xie));
+ var trueAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), trueTerm);
+ trueAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr));
+ var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.False)), xie));
+ var falseAxiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(x), Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));
+ falseAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));
+ }
this.mapEqInt = new Function(Token.NoToken, "linear@MapEq",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
- this.mapEqInt.AddAttribute("builtin", "MapEq");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapEqInt.AddAttribute("builtin", "MapEq");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new ExprSeq(aie, bie)), xie));
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie)));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, b, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
this.mapConstInt = new Function(Token.NoToken, "linear@MapConstInt",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));
- this.mapConstInt.AddAttribute("builtin", "MapConst");
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstInt.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new ExprSeq(aie)), xie));
+ var axiomExpr = new ForallExpr(Token.NoToken, new VariableSeq(a, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
}
}
}
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 23bbb1f9..b2bc0410 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -748,27 +748,25 @@ namespace Microsoft.Boogie
line = line.Replace("(", " ( ");
line = line.Replace(")", " ) ");
+ line = line.Replace(",", " ");
var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
List<object> newTuple = new List<object>();
- Stack<List<object>> wordStack = new Stack<List<object>>();
+ Stack<int> wordStack = new Stack<int>();
for (int i = 0; i < tuple.Length; i++) {
string elem = tuple[i];
if (elem == "(") {
- List<object> ls = new List<object>();
- wordStack.Push(ls);
+ wordStack.Push(newTuple.Count - 1);
}
else if (elem == ")") {
- List<object> ls = wordStack.Pop();
- if (wordStack.Count > 0) {
- wordStack.Peek().Add(ls);
- }
- else {
- newTuple.Add(ls);
+ int openParenIndex = wordStack.Pop();
+ List<object> ls = new List<object>();
+ for (int j = openParenIndex; j < newTuple.Count; j++)
+ {
+ ls.Add(newTuple[j]);
}
- }
- else if (wordStack.Count > 0) {
- wordStack.Peek().Add(elem);
+ newTuple.RemoveRange(openParenIndex, newTuple.Count - openParenIndex);
+ newTuple.Add(ls);
}
else {
newTuple.Add(elem);
@@ -777,6 +775,67 @@ namespace Microsoft.Boogie
return newTuple;
}
+ /*
+ List<object> GetFunctionTuple(string newLine)
+ {
+ if (newLine == null)
+ return null;
+ newLine = bv.Replace(newLine, "bv${1}");
+ string line = newLine;
+ int openParenCounter = CountOpenParentheses(newLine, 0);
+ if (!newLine.Contains("}"))
+ {
+ while (openParenCounter > 0)
+ {
+ newLine = ReadLine();
+ if (newLine == null)
+ {
+ return null;
+ }
+ line += newLine;
+ openParenCounter = CountOpenParentheses(newLine, openParenCounter);
+ }
+ }
+
+ line = line.Replace("(", " ( ");
+ line = line.Replace(")", " ) ");
+ var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
+
+ List<object> newTuple = new List<object>();
+ Stack<List<object>> wordStack = new Stack<List<object>>();
+ for (int i = 0; i < tuple.Length; i++)
+ {
+ string elem = tuple[i];
+ if (elem == "(")
+ {
+ List<object> ls = new List<object>();
+ wordStack.Push(ls);
+ }
+ else if (elem == ")")
+ {
+ List<object> ls = wordStack.Pop();
+ if (wordStack.Count > 0)
+ {
+ wordStack.Peek().Add(ls);
+ }
+ else
+ {
+ newTuple.Add(ls);
+ }
+ }
+ else if (wordStack.Count > 0)
+ {
+ wordStack.Peek().Add(elem);
+ }
+ else
+ {
+ newTuple.Add(elem);
+ }
+ }
+ return newTuple;
+ }
+ */
+
string[] GetWords(string line)
{
if (line == null)
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 9478595b..55e73161 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -94,7 +94,9 @@ public class SmartBlockPredicator {
cmdSeq.Add(aCmd);
} else if (cmd is AssumeCmd) {
var aCmd = (AssumeCmd)cmd;
- cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+ Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
+ aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr);
+ cmdSeq.Add(aCmd);
} else if (cmd is HavocCmd) {
var hCmd = (HavocCmd)cmd;
foreach (IdentifierExpr v in hCmd.Vars) {
@@ -216,12 +218,22 @@ public class SmartBlockPredicator {
while (i.MoveNext()) {
var block = i.Current;
- if (uni != null && uni.IsUniform(impl.Name, block.Item1))
- continue;
+
if (block.Item2) {
- if (block.Item1 == header)
+ if (block.Item1 == header) {
return;
- } else {
+ }
+ }
+
+ if (uni != null && uni.IsUniform(impl.Name, block.Item1)) {
+ if (blockGraph.Headers.Contains(block.Item1)) {
+ parentMap[block.Item1] = header;
+ AssignPredicates(blockGraph, dom, pdom, i, headPredicate, ref predCount);
+ }
+ continue;
+ }
+
+ if (!block.Item2) {
if (blockGraph.Headers.Contains(block.Item1)) {
parentMap[block.Item1] = header;
var loopPred = FreshPredicate(ref predCount);
@@ -494,15 +506,18 @@ public class SmartBlockPredicator {
.ToArray());
if (impl == null) {
- var newRequires = new RequiresSeq();
+ var fpIdentifierExpr = new IdentifierExpr(Token.NoToken, fpVar);
foreach (Requires r in proc.Requires) {
- newRequires.Add(new Requires(r.Free,
- new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
+ new EnabledReplacementVisitor(fpIdentifierExpr).VisitExpr(r.Condition);
+ if (!QKeyValue.FindBoolAttribute(r.Attributes, "do_not_predicate")) {
+ r.Condition = Expr.Imp(fpIdentifierExpr, r.Condition);
+ }
}
- var newEnsures = new EnsuresSeq();
foreach (Ensures e in proc.Ensures) {
- newEnsures.Add(new Ensures(e.Free,
- new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));
+ new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition);
+ if (!QKeyValue.FindBoolAttribute(e.Attributes, "do_not_predicate")) {
+ e.Condition = Expr.Imp(fpIdentifierExpr, e.Condition);
+ }
}
}
}
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index 3408d88b..6365d974 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -149,6 +149,44 @@ namespace Microsoft.Boogie
ProcedureChanged = true;
}
+ var procs = prog.TopLevelDeclarations.OfType<Procedure>();
+
+ foreach (var Proc in procs) {
+
+ if (uniformityInfo.ContainsKey(Proc.Name)) {
+ continue;
+ }
+
+ bool uniformProcedure = doAnalysis;
+
+ uniformityInfo.Add(Proc.Name, new KeyValuePair<bool, Dictionary<string, bool>>
+ (uniformProcedure, new Dictionary<string, bool>()));
+
+ inParameters[Proc.Name] = new List<string>();
+
+ foreach (Variable v in Proc.InParams) {
+ inParameters[Proc.Name].Add(v.Name);
+ if (doAnalysis) {
+ SetUniform(Proc.Name, v.Name);
+ }
+ else {
+ SetNonUniform(Proc.Name, v.Name);
+ }
+ }
+
+ outParameters[Proc.Name] = new List<string>();
+ foreach (Variable v in Proc.OutParams) {
+ outParameters[Proc.Name].Add(v.Name);
+ // We do not have a body for the procedure,
+ // so we must assume it produces non-uniform
+ // results
+ SetNonUniform(Proc.Name, v.Name);
+ }
+
+ ProcedureChanged = true;
+ }
+
+
if (doAnalysis)
{
while (ProcedureChanged)
@@ -163,17 +201,17 @@ namespace Microsoft.Boogie
}
}
- foreach (var Impl in impls)
+ foreach (var Proc in procs)
{
- if (!IsUniform (Impl.Name))
+ if (!IsUniform (Proc.Name))
{
List<string> newIns = new List<String>();
newIns.Add("_P");
- foreach (string s in inParameters[Impl.Name])
+ foreach (string s in inParameters[Proc.Name])
{
newIns.Add(s);
}
- inParameters[Impl.Name] = newIns;
+ inParameters[Proc.Name] = newIns;
}
}
}
@@ -265,15 +303,16 @@ namespace Microsoft.Boogie
}
}
- private Implementation GetImplementation(string procedureName)
+ private Procedure GetProcedure(string procedureName)
{
foreach (Declaration D in prog.TopLevelDeclarations)
{
- if (D is Implementation && ((D as Implementation).Name == procedureName))
+ if (D is Procedure && ((D as Procedure).Name == procedureName))
{
- return D as Implementation;
+ return D as Procedure;
}
}
+ Debug.Assert(false);
return null;
}
@@ -357,10 +396,8 @@ namespace Microsoft.Boogie
else if (c is CallCmd)
{
CallCmd callCmd = c as CallCmd;
- Implementation CalleeImplementation = GetImplementation(callCmd.callee);
-
- if (CalleeImplementation != null)
- {
+ DeclWithFormals Callee = GetProcedure(callCmd.callee);
+ Debug.Assert(Callee != null);
if (!ControlFlowIsUniform)
{
@@ -369,26 +406,25 @@ namespace Microsoft.Boogie
SetNonUniform(callCmd.callee);
}
}
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
+ for (int i = 0; i < Callee.InParams.Length; i++)
{
- if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name)
+ if (IsUniform(callCmd.callee, Callee.InParams[i].Name)
&& !IsUniform(impl.Name, callCmd.Ins[i]))
{
- SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name);
+ SetNonUniform(callCmd.callee, Callee.InParams[i].Name);
}
}
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
+ for (int i = 0; i < Callee.OutParams.Length; i++)
{
if (IsUniform(impl.Name, callCmd.Outs[i].Name)
- && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name))
+ && !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
{
SetNonUniform(impl.Name, callCmd.Outs[i].Name);
}
}
}
- }
else if (c is AssumeCmd)
{
var ac = (AssumeCmd)c;
@@ -526,20 +562,22 @@ namespace Microsoft.Boogie
Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]);
}
Console.WriteLine("]");
+ if (nonUniformLoops.ContainsKey(p)) {
Console.Write("Non-uniform loops:");
- foreach (int l in nonUniformLoops[p])
- {
+ foreach (int l in nonUniformLoops[p]) {
Console.Write(" " + l);
}
Console.WriteLine();
+ }
+ if (nonUniformBlocks.ContainsKey(p)) {
Console.Write("Non-uniform blocks:");
- foreach (Block b in nonUniformBlocks[p])
- {
+ foreach (Block b in nonUniformBlocks[p]) {
Console.Write(" " + b.Label);
}
Console.WriteLine();
}
}
+ }
public string GetInParameter(string procName, int i)
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index cf125c76..da73dea1 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -709,15 +709,19 @@ namespace Microsoft.Boogie.SMTLib
var builtin = ExtractBuiltin(op.Func);
var datatype = ExtractDatatype(op.Func);
if (builtin != null)
- printedName = builtin;
+ {
+ printedName = CheckMapApply(builtin, node);
+ }
else if (datatype != null)
- printedName = datatype;
+ {
+ printedName = datatype;
+ }
else
- printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ {
+ printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ }
Contract.Assert(printedName != null);
- printedName = CheckMapApply(printedName, node);
-
WriteApplication(printedName, node, options);
return true;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 11:44:06 +0000