summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Doomed/DoomCheck.cs18
-rw-r--r--Source/Doomed/DoomErrorHandler.cs4
-rw-r--r--Source/Houdini/AbstractHoudini.cs4
-rw-r--r--Source/Houdini/Checker.cs2
-rw-r--r--Source/VCGeneration/FixedpointVC.cs6
-rw-r--r--Source/VCGeneration/StratifiedVC.cs16
-rw-r--r--Source/VCGeneration/VC.cs34
-rw-r--r--Source/VCGeneration/Wlp.cs6
8 files changed, 45 insertions, 45 deletions
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs
index b317dc71..6b9f91cf 100644
--- a/Source/Doomed/DoomCheck.cs
+++ b/Source/Doomed/DoomCheck.cs
@@ -151,7 +151,7 @@ void ObjectInvariant()
}
#region Attributes
- public Hashtable Label2Absy;
+ public Dictionary<int, Absy> Label2Absy;
public DoomErrorHandler ErrorHandler {
set {
m_ErrHandler = value;
@@ -219,9 +219,9 @@ void ObjectInvariant()
}
- Label2Absy = new Hashtable(); // This is only a dummy
+ Label2Absy = new Dictionary<int, Absy>(); // This is only a dummy
m_Evc = new Evc(check);
- Hashtable l2a = null;
+ Dictionary<int, Absy> l2a = null;
VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
Contract.Assert(vce != null);
Contract.Assert( l2a!=null);
@@ -235,9 +235,9 @@ void ObjectInvariant()
{
Contract.Requires(check != null);
m_Check = check;
- Label2Absy = new Hashtable(); // This is only a dummy
+ Label2Absy = new Dictionary<int, Absy>(); // This is only a dummy
m_Evc = new Evc(check);
- Hashtable l2a = null;
+ Dictionary<int, Absy> l2a = null;
int assertionCount; // compute and then ignore
VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount);
Contract.Assert(vce != null);
@@ -301,14 +301,14 @@ void ObjectInvariant()
*/
- VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch, out int assertionCount) {
+ VCExpr GenerateEVC(Implementation impl, out Dictionary<int, Absy> label2absy, Checker ch, out int assertionCount) {
Contract.Requires(impl != null);
Contract.Requires(ch != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
TypecheckingContext tc = new TypecheckingContext(null);
impl.Typecheck(tc);
- label2absy = new Hashtable/*<int, Absy!>*/();
+ label2absy = new Dictionary<int, Absy>();
VCExpr vc;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Doomed:
@@ -322,7 +322,7 @@ void ObjectInvariant()
}
public VCExpr LetVC(Block startBlock,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount)
{
@@ -342,7 +342,7 @@ void ObjectInvariant()
}
VCExpr LetVC(Block block,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
Hashtable/*<Block, VCExprVar!>*/ blockVariables,
List<VCExprLetBinding> bindings,
ProverContext proverCtxt,
diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs
index 33d8b68e..a85adbe1 100644
--- a/Source/Doomed/DoomErrorHandler.cs
+++ b/Source/Doomed/DoomErrorHandler.cs
@@ -15,7 +15,7 @@ namespace VC
internal class DoomErrorHandler : ProverInterface.ErrorHandler
{
- protected Hashtable label2Absy;
+ protected Dictionary<int, Absy> label2Absy;
protected VerifierCallback callback;
private List<Block> m_CurrentTrace = new List<Block>();
@@ -28,7 +28,7 @@ namespace VC
}
- public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback)
+ public DoomErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback)
{
Contract.Requires(label2Absy != null);
Contract.Requires(callback != null);
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 24a3c708..157571f3 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -565,7 +565,7 @@ namespace Microsoft.Boogie.Houdini {
private void GenVC(Implementation impl)
{
ModelViewInfo mvInfo;
- System.Collections.Hashtable label2absy;
+ Dictionary<int, Absy> label2absy;
var collector = new AbsHoudiniCounterexampleCollector(this);
collector.OnProgress("HdnVCGen", 0, 0, 0.0);
@@ -2792,7 +2792,7 @@ namespace Microsoft.Boogie.Houdini {
private void GenVC(Implementation impl)
{
ModelViewInfo mvInfo;
- System.Collections.Hashtable label2absy;
+ Dictionary<int, Absy> label2absy;
if (CommandLineOptions.Clo.Trace)
{
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index b29aa933..ce46f20b 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -155,7 +155,7 @@ namespace Microsoft.Boogie.Houdini {
var exprGen = proverInterface.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- Hashtable/*<int, Absy!>*/ label2absy;
+ Dictionary<int, Absy> label2absy;
conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context);
if (!CommandLineOptions.Clo.UseLabels) {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 3299ef76..cf33c53e 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -395,7 +395,7 @@ namespace Microsoft.Boogie
public Dictionary<Incarnation, Absy> incarnationOriginMap;
public Hashtable /*Variable->Expr*/ exitIncarnationMap;
public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins;
- public Hashtable/*<int, Absy!>*/ label2absy;
+ public Dictionary<int, Absy> label2absy;
public VC.ModelViewInfo mvInfo;
public Dictionary<Block, VCExprVar> reachVars;
@@ -514,7 +514,7 @@ namespace Microsoft.Boogie
//public VCExpr vcexpr;
//public List<VCExprVar> interfaceExprVars;
//public List<VCExprVar> privateExprVars;
- //public Hashtable/*<int, Absy!>*/ label2absy;
+ //public Dictionary<int, Absy> label2absy;
//public VC.ModelViewInfo mvInfo;
//public Dictionary<Block, List<CallSite>> callSites;
//public Dictionary<Block, List<CallSite>> recordProcCallSites;
@@ -1007,7 +1007,7 @@ namespace Microsoft.Boogie
ConvertCFG2DAG(impl,edgesCut);
VC.ModelViewInfo mvInfo;
PassifyImpl(impl, out mvInfo);
- Hashtable/*<int, Absy!>*/ label2absy = null;
+ Dictionary<int, Absy> label2absy = null;
VCExpressionGenerator gen = checker.VCExprGen;
Contract.Assert(gen != null);
VCExpr vcexpr;
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index b4db817f..4078b43e 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -185,7 +185,7 @@ namespace VC {
public VCExpr vcexpr;
public List<VCExprVar> interfaceExprVars;
public List<VCExprVar> privateExprVars;
- public Hashtable/*<int, Absy!>*/ label2absy;
+ public Dictionary<int, Absy> label2absy;
public ModelViewInfo mvInfo;
public Dictionary<Block, List<CallSite>> callSites;
public Dictionary<Block, List<CallSite>> recordProcCallSites;
@@ -1151,7 +1151,7 @@ namespace VC {
// Get the VC of the current procedure
VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr;
- Hashtable/*<int, Absy!>*/ mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;
+ Dictionary<int, Absy> mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;
// Find all procedure calls in vc and put labels on them
FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
@@ -1349,7 +1349,7 @@ namespace VC {
StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];
info.GenerateVC();
VCExpr vc = info.vcexpr;
- Hashtable mainLabel2absy = info.label2absy;
+ Dictionary<int, Absy> mainLabel2absy = info.label2absy;
var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info);
// Find all procedure calls in vc and put labels on them
@@ -1851,7 +1851,7 @@ namespace VC {
// VCs with different labels each time)
public class FCallHandler : MutatingVCExprVisitor<bool> {
Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
- public readonly Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy;
+ public readonly Dictionary<int, Absy>/*!*/ mainLabel2absy;
public Dictionary<BoogieCallExpr/*!*/, int>/*!*/ boogieExpr2Id;
public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
@@ -1910,7 +1910,7 @@ namespace VC {
public FCallHandler(VCExpressionGenerator/*!*/ gen,
Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
- string mainProcName, Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy)
+ string mainProcName, Dictionary<int, Absy>/*!*/ mainLabel2absy)
: base(gen) {
Contract.Requires(gen != null);
Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
@@ -2116,7 +2116,7 @@ namespace VC {
return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]);
}
- public Hashtable/*<int,absy>*/ getLabel2absy() {
+ public Dictionary<int, Absy> getLabel2absy() {
Contract.Ensures(Contract.Result<Hashtable>() != null);
Contract.Assert(currProc != null);
@@ -2158,7 +2158,7 @@ namespace VC {
string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)
if (lop.label.Substring(1).StartsWith(prefix)) {
int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
- Hashtable label2absy = getLabel2absy();
+ Dictionary<int, Absy> label2absy = getLabel2absy();
Absy cmd = label2absy[id] as Absy;
//label2absy.Remove(id);
@@ -2718,7 +2718,7 @@ namespace VC {
Contract.Ensures(Contract.Result<Absy>() != null);
int id = int.Parse(label);
- Hashtable l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
+ Dictionary<int, Absy> l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
return cce.NonNull((Absy)l2a[id]);
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 80ffa072..af3454f5 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -290,7 +290,7 @@ namespace VC {
parent.CurrentLocalVariables = impl.LocVars;
ModelViewInfo mvInfo;
parent.PassifyImpl(impl, out mvInfo);
- Hashtable label2Absy;
+ Dictionary<int, Absy> label2Absy;
Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
@@ -441,7 +441,7 @@ namespace VC {
}
class ErrorHandler : ProverInterface.ErrorHandler {
- Hashtable label2Absy;
+ Dictionary<int, Absy> label2Absy;
VerifierCallback callback;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -450,7 +450,7 @@ namespace VC {
}
- public ErrorHandler(Hashtable label2Absy, VerifierCallback callback) {
+ public ErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback) {
Contract.Requires(label2Absy != null);
Contract.Requires(callback != null);
this.label2Absy = label2Absy;
@@ -1219,7 +1219,7 @@ namespace VC {
this.checker = checker;
- Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
+ Dictionary<int, Absy> label2absy = new Dictionary<int, Absy>();
ProverContext ctx = checker.TheoremProver.Context;
Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
@@ -1350,18 +1350,18 @@ namespace VC {
}
#endregion
- public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext)
+ public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
{
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- label2absy = new Hashtable/*<int, Absy!>*/();
+ label2absy = new Dictionary<int, Absy>();
return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
}
- protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/*<int, Absy!>*//*!*/ label2absy, ProverContext proverContext) {
+ protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1654,7 +1654,7 @@ namespace VC {
public class ErrorReporter : ProverInterface.ErrorHandler {
Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;
- Hashtable/*<int, Absy!>*//*!*/ label2absy;
+ Dictionary<int, Absy>/*!*/ label2absy;
List<Block/*!*/>/*!*/ blocks;
protected Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap;
protected VerifierCallback/*!*/ callback;
@@ -1687,7 +1687,7 @@ namespace VC {
Program/*!*/ program;
public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
- Hashtable/*<int, Absy!>*//*!*/ label2absy,
+ Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
VerifierCallback/*!*/ callback,
@@ -1783,7 +1783,7 @@ namespace VC {
public class ErrorReporterLocal : ErrorReporter {
public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
- Hashtable/*<int, Absy!>*//*!*/ label2absy,
+ Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
VerifierCallback/*!*/ callback,
@@ -2530,7 +2530,7 @@ namespace VC {
static VCExpr LetVC(Block startBlock,
VCExpr controlFlowVariableExpr,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount) {
Contract.Requires(startBlock != null);
@@ -2546,7 +2546,7 @@ namespace VC {
static VCExpr LetVCIterative(List<Block> blocks,
VCExpr controlFlowVariableExpr,
- Hashtable label2absy,
+ Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount) {
Contract.Requires(blocks != null);
@@ -2616,7 +2616,7 @@ namespace VC {
static VCExpr LetVC(Block block,
VCExpr controlFlowVariableExpr,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
Hashtable/*<Block, VCExprVar!>*/ blockVariables,
List<VCExprLetBinding/*!*/>/*!*/ bindings,
ProverContext proverCtxt,
@@ -2683,7 +2683,7 @@ namespace VC {
static VCExpr DagVC(Block block,
VCExpr controlFlowVariableExpr,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
Hashtable/*<Block, VCExpr!>*/ blockEquations,
ProverContext proverCtxt,
out int assertionCount)
@@ -2738,7 +2738,7 @@ namespace VC {
}
static VCExpr FlatBlockVC(Implementation impl,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
bool local, bool reach, bool doomed,
ProverContext proverCtxt,
out int assertionCount)
@@ -2874,7 +2874,7 @@ namespace VC {
}
static VCExpr NestedBlockVC(Implementation impl,
- Hashtable/*<int, Absy!>*/ label2absy,
+ Dictionary<int, Absy> label2absy,
bool reach,
ProverContext proverCtxt,
out int assertionCount){
@@ -2997,7 +2997,7 @@ namespace VC {
}
static VCExpr VCViaStructuredProgram
- (Implementation impl, Hashtable/*<int, Absy!>*/ label2absy,
+ (Implementation impl, Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
out int assertionCount)
{
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index d82310ee..eed4e2a5 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -20,19 +20,19 @@ namespace VC {
Contract.Invariant(Ctxt != null);
}
- [Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;
+ [Rep] public readonly Dictionary<int, Absy> Label2absy;
[Rep] public readonly ProverContext Ctxt;
public readonly VCExpr ControlFlowVariableExpr;
public int AssertionCount; // counts the number of assertions for which Wlp has been computed
- public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt)
+ public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt)
{
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
this.Ctxt = ctxt;
}
- public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)
+ public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)
{
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 02:39:51 +0000