summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/BitvectorAnalysis.cs2
-rw-r--r--Source/Core/LinearSets.cs51
-rw-r--r--Source/Core/OwickiGries.cs4
-rw-r--r--Source/Core/TypeAmbiguitySeeker.cs1
-rw-r--r--Source/Predication/SmartBlockPredicator.cs2
5 files changed, 33 insertions, 27 deletions
diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs
index 0bd3123b..a555352b 100644
--- a/Source/Core/BitvectorAnalysis.cs
+++ b/Source/Core/BitvectorAnalysis.cs
@@ -528,7 +528,7 @@ namespace Microsoft.Boogie {
DiscoverIntAndBv32Functions(program);
BvType bv32Type = new BvType(32);
- List<Variable> bv32In = new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true));
+ List<Variable> bv32In = new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true) };
Formal bv32Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv32Type), false);
bv32Id = new Function(Token.NoToken, "bv32Id", bv32In, bv32Out);
bv32Id.Body = new IdentifierExpr(Token.NoToken, bv32In[0]);
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 8d0faf2b..957718fa 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -400,7 +400,12 @@ namespace Microsoft.Boogie
foreach (string domainName in linearDomains.Keys)
{
var domain = linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);
+ Formal f = new Formal(
+ Token.NoToken,
+ new TypedIdent(Token.NoToken,
+ domainName + "_in",
+ new MapType(Token.NoToken, new TypeVariableSeq(),
+ new List<Type> { domain.elementType }, Type.Bool)), true);
impl.InParams.Add(f);
domainNameToInputVar[domainName] = f;
}
@@ -518,7 +523,7 @@ namespace Microsoft.Boogie
{
proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName])));
var domain = linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);
proc.InParams.Add(f);
domainNameToOutputScope[domainName].Add(f);
proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName])));
@@ -568,7 +573,7 @@ namespace Microsoft.Boogie
public Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)
{
LinearDomain domain = linearDomains[domainName];
- BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Microsoft.Boogie.Type.Int)));
+ BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));
Expr disjointExpr = Expr.True;
int count = 0;
foreach (Variable v in scope)
@@ -580,7 +585,7 @@ namespace Microsoft.Boogie
e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.True)));
disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);
}
- return new ExistsExpr(Token.NoToken, new List<Variable>(partition), disjointExpr);
+ return new ExistsExpr(Token.NoToken, new List<Variable> { partition }, disjointExpr);
}
}
@@ -599,11 +604,11 @@ namespace Microsoft.Boogie
this.elementType = elementType;
this.axioms = new List<Axiom>();
- MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(this.elementType), Type.Bool);
- MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(this.elementType), Type.Int);
+ MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { this.elementType }, Type.Bool);
+ MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { this.elementType }, Type.Int);
this.mapOrBool = new Function(Token.NoToken, domainName + "_linear_MapOr",
- new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
- new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
+ new List<Variable> { 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));
if (CommandLineOptions.Clo.UseArrayTheory)
{
@@ -622,16 +627,16 @@ namespace Microsoft.Boogie
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 TypeVariableSeq(), new List<Variable>(a, b), null,
+ var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null,
new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)),
- new ForallExpr(Token.NoToken, new List<Variable>(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ new ForallExpr(Token.NoToken, new List<Variable> { 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, domainName + "_linear_MapImp",
- new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
- new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
+ new List<Variable> { 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));
if (CommandLineOptions.Clo.UseArrayTheory)
{
@@ -650,15 +655,15 @@ namespace Microsoft.Boogie
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 TypeVariableSeq(), new List<Variable>(a, b), null,
+ var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null,
new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)),
- new ForallExpr(Token.NoToken, new List<Variable>(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ new ForallExpr(Token.NoToken, new List<Variable> { 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, domainName + "_linear_MapConstBool",
- new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),
+ new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true) },
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
if (CommandLineOptions.Clo.UseArrayTheory)
{
@@ -670,19 +675,19 @@ namespace Microsoft.Boogie
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 List<Variable>(x), trueTerm);
+ var trueAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { 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 List<Variable>(x), Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));
+ var falseAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { 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, domainName + "_linear_MapEq",
- new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),
- new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true)),
+ new List<Variable> { 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));
if (CommandLineOptions.Clo.UseArrayTheory)
{
@@ -701,15 +706,15 @@ namespace Microsoft.Boogie
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 TypeVariableSeq(), new List<Variable>(a, b), null,
+ var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List<Variable> { a, b }, null,
new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)),
- new ForallExpr(Token.NoToken, new List<Variable>(x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ new ForallExpr(Token.NoToken, new List<Variable> { 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, domainName + "_linear_MapConstInt",
- new List<Variable>(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),
+ new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true) },
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));
if (CommandLineOptions.Clo.UseArrayTheory)
{
@@ -722,7 +727,7 @@ namespace Microsoft.Boogie
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 List<Variable>(a, x), Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));
+ var axiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { 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/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 2df7b3ba..cbaff3ef 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -168,7 +168,7 @@ namespace Microsoft.Boogie
foreach (string domainName in linearTypechecker.linearDomains.Keys)
{
var domain = linearTypechecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);
inputs.Add(f);
}
foreach (IdentifierExpr ie in globalMods)
@@ -727,7 +727,7 @@ namespace Microsoft.Boogie
foreach (string domainName in linearTypechecker.linearDomains.Keys)
{
var domain = linearTypechecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type>(domain.elementType), Type.Bool)), true);
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new List<Type> { domain.elementType }, Type.Bool)), true);
inputs.Add(f);
}
foreach (IdentifierExpr ie in globalMods)
diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs
index 1293dd1b..ecb1e418 100644
--- a/Source/Core/TypeAmbiguitySeeker.cs
+++ b/Source/Core/TypeAmbiguitySeeker.cs
@@ -5,6 +5,7 @@
//-----------------------------------------------------------------------------
using System;
using System.Diagnostics.Contracts;
+using System.Collections.Generic;
// Visitor to search for types proxies that could not completely be
// determined by type inference. If this happens, a warning is
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 484a866d..28005186 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -115,7 +115,7 @@ public class SmartBlockPredicator {
new IdentifierExpr(Token.NoToken, havocVar);
}
cmdSeq.Add(new HavocCmd(Token.NoToken,
- new List<IdentifierExpr>(havocTempExpr)));
+ new List<IdentifierExpr> { havocTempExpr }));
cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 22:49:46 +0000