diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 8 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomCheck.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/OrderingAxioms.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 22 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 50 | ||||
| -rw-r--r-- | Source/VCGeneration/VCDoomed.cs | 18 |
7 files changed, 55 insertions, 55 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 5618fafa..119218a1 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -336,22 +336,22 @@ namespace Microsoft.Boogie { [ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(identifierToPartition));
+ Contract.Invariant(identifierToPartition != null);
Contract.Invariant(partitionToIdentifiers != null);
Contract.Invariant(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
Contract.Invariant(partitionToValue != null);
Contract.Invariant(valueToPartition != null);
- Contract.Invariant(cce.NonNullElements(definedFunctions));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(definedFunctions));
}
public ErrorModel(Dictionary<string, int> identifierToPartition, List<List<string>> partitionToIdentifiers, List<Object> partitionToValue, Dictionary<object, int> valueToPartition, Dictionary<string, List<List<int>>> definedFunctions) {
- Contract.Requires(cce.NonNullElements(identifierToPartition));
+ Contract.Requires(identifierToPartition != null);
Contract.Requires(partitionToIdentifiers != null);
Contract.Requires(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
Contract.Requires(partitionToValue != null);
Contract.Requires(valueToPartition != null);
- Contract.Requires(cce.NonNullElements(definedFunctions));
+ Contract.Requires(cce.NonNullDictionaryAndValues(definedFunctions));
this.identifierToPartition = identifierToPartition;
this.partitionToIdentifiers = partitionToIdentifiers;
this.partitionToValue = partitionToValue;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 20b17e6b..6400aaf2 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -71,7 +71,7 @@ namespace Microsoft.Boogie { Contract.Invariant(Trace != null);
Contract.Invariant(Context != null);
Contract.Invariant(cce.NonNullElements(relatedInformation));
- Contract.Invariant(cce.NonNullElements(calleeCounterexamples));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(calleeCounterexamples));
}
[Peer]
@@ -112,7 +112,7 @@ namespace Microsoft.Boogie { public void AddCalleeCounterexample(Dictionary<TraceLocation, CalleeCounterexampleInfo> cs)
{
- Contract.Requires(cce.NonNullElements(cs));
+ Contract.Requires(cce.NonNullDictionaryAndValues(cs));
foreach (TraceLocation loc in cs.Keys)
{
AddCalleeCounterexample(loc, cs[loc]);
@@ -474,7 +474,7 @@ namespace VC { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(checkers));
- Contract.Invariant(cce.NonNullElements(incarnationOriginMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Invariant(program != null);
}
diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs index 8a9f808c..03f0af8f 100644 --- a/Source/VCGeneration/DoomCheck.cs +++ b/Source/VCGeneration/DoomCheck.cs @@ -717,7 +717,7 @@ void ObjectInvariant() #region Collect Unavoidable Blocks
private Block BreadthFirst(Block start, Dictionary<Block, TraceNode> blockmap) {
Contract.Requires(start != null);
- Contract.Requires(cce.NonNullElements(blockmap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(blockmap));
Contract.Ensures(Contract.Result<Block>() != null);
List<Block> JobList = new List<Block>();
@@ -800,7 +800,7 @@ void ObjectInvariant() // it should be implemented using one function later on.
private void BreadthFirstBwd(Block start, Dictionary<Block, TraceNode> blockmap) {
Contract.Requires(start != null);
- Contract.Requires(cce.NonNullElements(blockmap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(blockmap));
List<Block> JobList = new List<Block>();
List<Block> DoneList = new List<Block>();
diff --git a/Source/VCGeneration/OrderingAxioms.cs b/Source/VCGeneration/OrderingAxioms.cs index 877fba13..4fbc80da 100644 --- a/Source/VCGeneration/OrderingAxioms.cs +++ b/Source/VCGeneration/OrderingAxioms.cs @@ -24,7 +24,7 @@ namespace Microsoft.Boogie { void ObjectInvariant() {
Contract.Invariant(Gen != null);
Contract.Invariant(Translator != null);
- Contract.Invariant(cce.NonNullElements(OneStepFuns));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(OneStepFuns));
Contract.Invariant(cce.NonNullElements(Constants));
Contract.Invariant(cce.NonNullElements(CompleteConstantsOpen));
Contract.Invariant(cce.NonNullElements(AllAxioms));
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index c418f828..48029154 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -26,7 +26,7 @@ namespace VC [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
}
/// <summary>
@@ -1675,12 +1675,12 @@ namespace VC [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
Contract.Invariant(mainLabel2absy != null);
- Contract.Invariant(cce.NonNullElements(boogieExpr2Id));
- Contract.Invariant(cce.NonNullElements(id2Candidate));
- Contract.Invariant(cce.NonNullElements(id2ControlVar));
- Contract.Invariant(cce.NonNullElements(label2Id));
+ Contract.Invariant(boogieExpr2Id != null);
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2Candidate));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2ControlVar));
+ Contract.Invariant(label2Id != null);
}
// Name of the procedure whose VC we're mutating
@@ -1696,7 +1696,7 @@ namespace VC : base(gen)
{
Contract.Requires(gen != null);
- Contract.Requires(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
Contract.Requires(mainLabel2absy != null);
this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
this.mainProcName = mainProcName;
@@ -2023,7 +2023,7 @@ namespace VC [ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(cce.NonNullElements(subst));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
}
@@ -2105,7 +2105,7 @@ namespace VC Contract.Invariant(program != null);
Contract.Invariant(callback != null);
Contract.Invariant(theoremProver != null);
- Contract.Invariant(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
}
@@ -2114,7 +2114,7 @@ namespace VC Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,
Program/*!*/ program, Implementation/*!*/ mainImpl)
{
- Contract.Requires(cce.NonNullElements(implName2StratifiedInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
Contract.Requires(theoremProver != null);
Contract.Requires(callback != null);
Contract.Requires(context != null);
@@ -2268,7 +2268,7 @@ namespace VC Contract.Requires(b != null);
Contract.Requires(traceNodes != null);
Contract.Requires(trace != null);
- Contract.Requires(cce.NonNullElements(calleeCounterexamples));
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
// After translation, all potential errors come from asserts.
while (true)
{
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 0215784b..1062767c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -73,7 +73,7 @@ namespace VC { Contract.Invariant(controlFlowVariable != null);
Contract.Invariant(assertExpr != null);
Contract.Invariant(cce.NonNullElements(interfaceVars));
- Contract.Invariant(incarnationOriginMap == null || cce.NonNullElements(incarnationOriginMap));
+ Contract.Invariant(incarnationOriginMap == null || cce.NonNullDictionaryAndValues(incarnationOriginMap));
}
public Implementation impl;
@@ -145,7 +145,7 @@ namespace VC { }
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
}
private Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;
@@ -283,8 +283,8 @@ namespace VC { Contract.Invariant(impl != null);
Contract.Invariant(initial != null);
Contract.Invariant(program != null);
- Contract.Invariant(cce.NonNullElements(copies));
- Contract.Invariant(cce.NonNullElements(visited));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(copies));
+ Contract.Invariant(visited != null);
Contract.Invariant(callback != null);
}
@@ -690,14 +690,14 @@ namespace VC { void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(blocks));
Contract.Invariant(cce.NonNullElements(big_blocks));
- Contract.Invariant(cce.NonNullElements(stats));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(stats));
Contract.Invariant(cce.NonNullElements(assumized_branches));
Contract.Invariant(gotoCmdOrigins != null);
Contract.Invariant(parent != null);
Contract.Invariant(impl != null);
Contract.Invariant(copies != null);
- Contract.Invariant(cce.NonNullElements(protected_from_assert_to_assume));
- Contract.Invariant(cce.NonNullElements(keep_at_all));
+ Contract.Invariant(protected_from_assert_to_assume != null);
+ Contract.Invariant(keep_at_all != null);
}
@@ -863,7 +863,7 @@ namespace VC { Dictionary<Block/*!*/, bool>/*!*/ ComputeReachableNodes(Block/*!*/ b) {
Contract.Requires(b != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<Block, bool>>()));
+ Contract.Ensures(Contract.Result<Dictionary<Block, bool>>() != null);
BlockStats s = GetBlockStats(b);
if (s.reachable_blocks != null) {
return s.reachable_blocks;
@@ -1462,7 +1462,7 @@ namespace VC { }
private void SoundnessCheck(Dictionary<PureCollections.Tuple/*!*/, bool>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {
- Contract.Requires(cce.NonNullElements(cache));
+ Contract.Requires(cache != null);
Contract.Requires(orig != null);
Contract.Requires(copies != null);
{
@@ -1758,9 +1758,9 @@ namespace VC { Contract.Invariant(gotoCmdOrigins != null);
Contract.Invariant(label2absy != null);
Contract.Invariant(cce.NonNullElements(blocks));
- Contract.Invariant(cce.NonNullElements(incarnationOriginMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Invariant(callback != null);
- Contract.Invariant(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Invariant(context != null);
Contract.Invariant(program != null);
}
@@ -1792,9 +1792,9 @@ namespace VC { Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(label2absy != null);
Contract.Requires(cce.NonNullElements(blocks));
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(callback != null);
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context!=null);
Contract.Requires(program!=null);
this.gotoCmdOrigins = gotoCmdOrigins;
@@ -1893,9 +1893,9 @@ namespace VC { Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(label2absy != null);
Contract.Requires(cce.NonNullElements(blocks));
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(callback != null);
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context != null);
Contract.Requires(program != null);
}
@@ -2534,7 +2534,7 @@ namespace VC { string/*!*/ implName, List<int>/*!*/ values)
{
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context != null);
Contract.Requires(program != null);
Contract.Requires(implName != null);
@@ -2662,7 +2662,7 @@ namespace VC { Contract.Requires(b != null);
Contract.Requires(trace != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
// After translation, all potential errors come from asserts.
return null;
@@ -2678,11 +2678,11 @@ namespace VC { Contract.Requires(b != null);
Contract.Requires(traceNodes != null);
Contract.Requires(trace != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
- Contract.Requires(cce.NonNullElements(implName2LazyInliningInfo));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));
Contract.Requires(context != null);
Contract.Requires(program != null);
- Contract.Requires(cce.NonNullElements(calleeCounterexamples));
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
// After translation, all potential errors come from asserts.
CmdSeq cmds = b.Cmds;
Contract.Assert(cmds != null);
@@ -2762,9 +2762,9 @@ namespace VC { Contract.Requires(expr != null);
Contract.Requires(incarnationMap != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(exprToPrintableValue));
+ Contract.Requires(cce.NonNullDictionaryAndValues(exprToPrintableValue));
Contract.Requires(cce.NonNullElements(relatedInformation));
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
if (errorDataEnhanced is ListOfMiningStrategies) {
ListOfMiningStrategies loms = (ListOfMiningStrategies)errorDataEnhanced;
List < MiningStrategy > l = loms.msList;
@@ -2842,7 +2842,7 @@ namespace VC { Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap, List<string/*!*/>/*!*/ relatedInformation) {
Contract.Requires(incarnationMap != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(cce.NonNullElements(relatedInformation));
List<int> heapSuccList = ComputeHeapSuccessions(incarnationMap, errModel);
TreatHeapSuccessions(heapSuccList, incarnationMap, errModel, incarnationOriginMap, relatedInformation);
@@ -2971,7 +2971,7 @@ namespace VC { Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap, List<string/*!*/>/*!*/ relatedInformation) {
Contract.Requires(incarnationMap != null);
Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(cce.NonNullElements(relatedInformation));
if (heapSuccessionList == null) {
// empty list of heap successions, nothing we can do!
@@ -3469,7 +3469,7 @@ namespace VC { Contract.Requires(transferCmd != null);
Contract.Requires(trace != null);
Contract.Requires(context != null);
- Contract.Requires(cce.NonNullElements(incarnationOriginMap));
+ Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Ensures(Contract.Result<Counterexample>() != null);
List<string> relatedInformation = new List<string>();
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index c0d3ac68..950c0158 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -25,8 +25,8 @@ namespace VC { List<Cmd/*!*/>/*!*/ m_doomedCmds = new List<Cmd/*!*/>();
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(m_BlockReachabilityMap));
- Contract.Invariant(cce.NonNullElements(m_copiedBlocks));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(m_BlockReachabilityMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(m_copiedBlocks));
Contract.Invariant(cce.NonNullElements(m_doomedCmds));
Contract.Invariant(cce.NonNullElements(_copiedBlock));
}
@@ -95,10 +95,10 @@ namespace VC { private Block CopyImplBlocks(Block b, ref List<Block> blocklist, Block targetBlock, ref Dictionary<Block, Block> alreadySeen) {
Contract.Requires(b != null);
Contract.Requires(targetBlock != null);
- Contract.Requires(cce.NonNullElements(alreadySeen));
+ Contract.Requires(cce.NonNullDictionaryAndValues(alreadySeen));
Contract.Requires(blocklist != null);
Contract.Ensures(Contract.ValueAtReturn(out blocklist) != null);
- Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out alreadySeen)));
+ Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.ValueAtReturn(out alreadySeen)));
Contract.Ensures(Contract.Result<Block>() != null);
Block seen;
@@ -635,7 +635,7 @@ namespace VC { Contract.Requires(reachvar != null);
Contract.Requires(impl != null);
Contract.Requires(callback != null);
- Contract.Requires(cce.NonNullElements(cmdbackup));
+ Contract.Requires(cce.NonNullDictionaryAndValues(cmdbackup));
#region Modify implementation
for (int i = startidx; i <= endidx; i++) {
if (_copiedBlock.Contains(impl.Blocks[i]))
@@ -762,7 +762,7 @@ namespace VC { void UndoBlockModifications(Implementation impl, Dictionary<Block/*!*/, CmdSeq/*!*/>/*!*/ cmdbackup,
int startidx, int endidx) {
- Contract.Requires(cce.NonNullElements(cmdbackup));
+ Contract.Requires(cce.NonNullDictionaryAndValues(cmdbackup));
Contract.Requires(impl != null);
for (int i = startidx; i <= endidx; i++) {
CmdSeq cs = null;
@@ -832,7 +832,7 @@ namespace VC { void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Blocks));
Contract.Invariant(cce.NonNullElements(m_checkableBlocks));
- Contract.Invariant(cce.NonNullElements(m_copyMap));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(m_copyMap));
}
@@ -868,7 +868,7 @@ namespace VC { private Block AbstractLoopUnrolling(GraphNode node, Dictionary<GraphNode, Block> visited, bool unrollable, String prefix)
{
Contract.Requires(node != null);
- Contract.Requires(cce.NonNullElements(visited));
+ Contract.Requires(cce.NonNullDictionaryAndValues(visited));
Contract.Requires(prefix != null);
Contract.Ensures(Contract.Result<Block>() != null);
Block newb;
@@ -1207,7 +1207,7 @@ namespace VC { public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary<Block, GraphNode> gd, Set /*Block*/ beingVisited) {
Contract.Requires(b != null);
Contract.Requires(beingVisited != null);
- Contract.Requires(cce.NonNullElements(gd));
+ Contract.Requires(cce.NonNullDictionaryAndValues(gd));
Contract.Ensures(Contract.Result<GraphNode>() != null);
|