diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-07 14:12:08 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-07 14:12:08 -0800 |
| commit | 27c1f51bf703cf1c1ebedec761219761e035b5c0 (patch) | |
| tree | 204d00f1f81d56633c9c08abe6d47e81e2fced9d /Source | |
| parent | 5212d1a82598c56d5c330ed68d1bd6c5d443084e (diff) | |
| parent | 93ac6ee9dff39a8ae70bf2bafa3333685773d04b (diff) | |
Merge
Diffstat (limited to 'Source')
22 files changed, 249 insertions, 251 deletions
diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs index 005c9b17..ab10be9a 100644 --- a/Source/AIFramework/Lattice.cs +++ b/Source/AIFramework/Lattice.cs @@ -11,11 +11,12 @@ namespace Microsoft.AbstractInterpretationFramework { using System.Diagnostics;
using Microsoft.AbstractInterpretationFramework.Collections;
using Microsoft.Boogie;
- using IMutableSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ArraySet = Microsoft.Boogie.Set;
+ using ArraySet = Microsoft.Boogie.GSet<object>; + using IMutableSet = Microsoft.Boogie.GSet<object>;
+ using HashSet = Microsoft.Boogie.GSet<object>;
+ using ISet = Microsoft.Boogie.GSet<object>;
+ using Set = Microsoft.Boogie.GSet<object>;
/// <summary>
diff --git a/Source/AIFramework/MultiLattice.cs b/Source/AIFramework/MultiLattice.cs index 9071bd4c..ba9aa752 100644 --- a/Source/AIFramework/MultiLattice.cs +++ b/Source/AIFramework/MultiLattice.cs @@ -11,7 +11,9 @@ namespace Microsoft.AbstractInterpretationFramework { using Microsoft.AbstractInterpretationFramework.Collections;
using Microsoft.Boogie;
- using ISet = Microsoft.Boogie.Set;
+
+ using ISet = Microsoft.Boogie.GSet<object>;
+ using Set = Microsoft.Boogie.GSet<object>;
/// <summary>
diff --git a/Source/AIFramework/Mutable.cs b/Source/AIFramework/Mutable.cs index 232909e4..7592aa6a 100644 --- a/Source/AIFramework/Mutable.cs +++ b/Source/AIFramework/Mutable.cs @@ -11,7 +11,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections { /// <summary>
/// Extend sets for using as a IWorkList.
/// </summary>
- public class WorkSet : Microsoft.Boogie.Set, Microsoft.Boogie.IWorkList {
+ public class WorkSet : Microsoft.Boogie.GSet<object>, Microsoft.Boogie.IWorkList {
// See Bug #148 for an explanation of why this is here.
// Without it, the contract inheritance rules will complain since it
diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.cs b/Source/AIFramework/Polyhedra/LinearConstraint.cs index 5d1cabd5..ab5e14f8 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraint.cs +++ b/Source/AIFramework/Polyhedra/LinearConstraint.cs @@ -9,9 +9,10 @@ namespace Microsoft.AbstractInterpretationFramework { //using System.Compiler;
using System.Collections;
using Microsoft.Basetypes;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
+ using Set = Microsoft.Boogie.GSet<object>; + using IMutableSet = Microsoft.Boogie.GSet<object>;
+ using HashSet = Microsoft.Boogie.GSet<object>;
+ using ISet = Microsoft.Boogie.GSet<object>;
/// <summary>
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs index 299d49cf..74e36eae 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs @@ -11,9 +11,10 @@ namespace Microsoft.AbstractInterpretationFramework { //using Microsoft.SpecSharp.Collections;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
+
+ using IMutableSet = Microsoft.Boogie.GSet<object>;
+ using ISet = Microsoft.Boogie.GSet<object>;
+ using HashSet = Microsoft.Boogie.GSet<object>;
/// <summary>
/// Represents a system of linear constraints (constraint/frame representations).
diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs index 44abfed6..06c0f483 100644 --- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs +++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs @@ -11,9 +11,8 @@ namespace Microsoft.AbstractInterpretationFramework { using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
- using ISet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
-
+ using ISet = Microsoft.Boogie.GSet<object>;
+ using HashSet = Microsoft.Boogie.GSet<object>;
/// <summary>
/// Represents an invariant over linear variable constraints, represented by a polyhedron.
diff --git a/Source/AIFramework/Polyhedra/SimplexTableau.cs b/Source/AIFramework/Polyhedra/SimplexTableau.cs index 4c37e980..4d734c27 100644 --- a/Source/AIFramework/Polyhedra/SimplexTableau.cs +++ b/Source/AIFramework/Polyhedra/SimplexTableau.cs @@ -8,8 +8,8 @@ namespace Microsoft.AbstractInterpretationFramework { using System;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
+ using IMutableSet = Microsoft.Boogie.GSet<object>;
+ using HashSet = Microsoft.Boogie.GSet<object>;
/// <summary>
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index b60d318b..172cef01 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -13,9 +13,11 @@ namespace Microsoft.AbstractInterpretationFramework { using Microsoft.AbstractInterpretationFramework.Collections;
using Microsoft.Boogie;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
+
+ using IMutableSet = Microsoft.Boogie.GSet<object>;
+ using ISet = Microsoft.Boogie.GSet<object>;
+ using Set = Microsoft.Boogie.GSet<object>;
+ using HashSet = Microsoft.Boogie.GSet<object>;
/// <summary>
/// Creates a lattice that works for several variables given a MicroLattice. Assumes
diff --git a/Source/Basetypes/Set.cs b/Source/Basetypes/Set.cs index e31e5399..dfd65b4b 100644 --- a/Source/Basetypes/Set.cs +++ b/Source/Basetypes/Set.cs @@ -7,41 +7,51 @@ namespace Microsoft.Boogie { using System;
using System.IO;
using System.Collections;
+ using System.Collections.Generic;
using System.Diagnostics.Contracts;
/// <summary>
/// A class representing a mathematical set.
/// </summary>
- public class Set : ICloneable, IEnumerable {
+ public class GSet<T> : ICloneable, IEnumerable, IEnumerable<T> {
/*[Own]*/
- Hashtable ht;
+ Dictionary<T, int> ht;
+ List<T> arr; // keep elements in a well-defined order; otherwise iteration is non-deterministic
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(ht != null);
+ Contract.Invariant(arr != null);
+ Contract.Invariant(ht.Count == arr.Count);
}
- public Set() {
- ht = new Hashtable();
+ public GSet() {
+ ht = new Dictionary<T, int>();
+ arr = new List<T>();
//:base();
}
- private Set(Hashtable/*!*/ ht) {
+ private GSet(Dictionary<T,int>/*!*/ ht, List<T> arr) {
Contract.Requires(ht != null);
+ Contract.Requires(arr != null);
this.ht = ht;
+ this.arr = arr;
//:base();
}
- public Set(int capacity) {
- ht = new Hashtable(capacity);
+ public GSet(int capacity) {
+ ht = new Dictionary<T, int>(capacity);
+ arr = new List<T>(capacity);
//:base();
}
- public readonly static Set/*!*/ Empty = new Set();
+ public readonly static GSet<T>/*!*/ Empty = new GSet<T>();
public void Clear() {
ht.Clear();
+ arr.Clear();
}
/// <summary>
@@ -49,18 +59,18 @@ namespace Microsoft.Boogie { /// In notation:
/// this.SetElements = this.SetElements_old \union {o};
/// </summary>
- public void Add(object/*!*/ o) {
- Contract.Requires(o != null);
- ht[o] = o;
+ public void Add(T o) {
+ if (!ht.ContainsKey(o)) {
+ ht[o] = arr.Count;
+ arr.Add(o);
+ }
}
/// <summary>
- /// this.SetElements = this.SetElements_old \union s.SetElements;
+ /// this.SetElements = this.SetElements_old \union s.GSet<T>Elements;
/// </summary>
- public void AddRange(Set/*!*/ s) {
- Contract.Requires(s != null);
- foreach (object/*!*/ o in s) {
- Contract.Assert(o != null);
+ public void AddRange(IEnumerable<T> s) {
+ foreach (T o in s) {
Add(o);
}
}
@@ -68,22 +78,30 @@ namespace Microsoft.Boogie { /// <summary>
/// this.SetElements = this.SetElements_old \setminus {o};
/// </summary>
- public void Remove(object/*!*/ o) {
- Contract.Requires(o != null);
- ht.Remove(o);
+ public void Remove(T o) {
+ int idx;
+ if (ht.TryGetValue(o, out idx)) {
+ var last = arr[arr.Count - 1];
+ arr.RemoveAt(arr.Count - 1);
+ if (idx != arr.Count) {
+ arr[idx] = last;
+ ht[last] = idx;
+ }
+ ht.Remove(o);
+ }
}
/// <summary>
/// this.SetElements = this.SetElements_old \setminus s.SetElements;
/// </summary>
- public void RemoveRange(Set/*!*/ s) {
+ public void RemoveRange(IEnumerable<T> s) {
Contract.Requires(s != null);
if (s == this) {
ht.Clear();
+ arr.Clear();
} else {
- foreach (object/*!*/ o in s) {
- Contract.Assert(o != null);
- ht.Remove(o);
+ foreach (T o in s) {
+ Remove(o);
}
}
}
@@ -91,45 +109,44 @@ namespace Microsoft.Boogie { /// <summary>
/// Returns an arbitrary element from the set.
/// </summary>
- public object/*!*/ Choose() {
+ public T Choose() {
Contract.Requires((Count > 0));
- Contract.Ensures(Contract.Result<object>() != null);
- IEnumerator iter = GetEnumerator();
- iter.MoveNext();
- return cce.NonNull(iter.Current);
+ foreach(var e in this)
+ return e;
+ return default(T);
}
/// <summary>
/// Picks an arbitrary element from the set, removes it, and returns it.
/// </summary>
- public object/*!*/ Take() {
+ public T Take() {
Contract.Requires((Count > 0));
- Contract.Ensures(Contract.Result<object>() != null);
Contract.Ensures(Count == Contract.OldValue(Count) - 1);
- object r = Choose();
+ T r = Choose();
Remove(r);
return r;
}
- public void Intersect(Set/*!*/ s) {
+ public void Intersect(GSet<T>/*!*/ s) {
Contract.Requires(s != null);
- Hashtable h = new Hashtable(ht.Count);
- foreach (object/*!*/ key in ht.Keys) {
- Contract.Assert(key != null);
+ if (s == this) return;
+ ht.Clear();
+ var newArr = new List<T>();
+ foreach (T key in arr) {
if (s.ht.ContainsKey(key)) {
- h.Add(key, key);
+ ht[key] = newArr.Count;
+ newArr.Add(key);
}
}
- ht = h;
+ arr = newArr;
}
/// <summary>
/// The getter returns true iff "o" is in the set.
/// The setter adds the value "o" (for "true") or removes "o" (for "false")
/// </summary>
- public bool this[object/*!*/ o] {
+ public bool this[T o] {
get {
- Contract.Requires(o != null);
return ht.ContainsKey(o);
}
set {
@@ -147,12 +164,8 @@ namespace Microsoft.Boogie { /// <param name="o"></param>
/// <returns></returns>
[Pure]
- public bool Contains(object/*!*/ o) {
- Contract.Requires(o != null);
- if (!this.ht.ContainsKey(o)) {
- return false;
- }
- return true;
+ public bool Contains(T o) {
+ return this.ht.ContainsKey(o);
}
/// <summary>
@@ -161,11 +174,10 @@ namespace Microsoft.Boogie { /// </summary>
/// <param name="s"></param>
/// <returns></returns>
- public bool ContainsRange(Set/*!*/ s) {
+ public bool ContainsRange(IEnumerable<T> s) {
Contract.Requires(s != null);
if (s != this) {
- foreach (object/*!*/ key in s.ht.Keys) {
- Contract.Assert(key != null);
+ foreach (T key in s) {
if (!this.ht.ContainsKey(key)) {
return false;
}
@@ -176,7 +188,7 @@ namespace Microsoft.Boogie { public object/*!*/ Clone() {
Contract.Ensures(Contract.Result<object>() != null);
- return new Set((Hashtable/*!*/)cce.NonNull(ht.Clone()));
+ return new GSet<T>(new Dictionary<T,int>(ht), new List<T>(arr));
}
public virtual int Count {
@@ -186,12 +198,6 @@ namespace Microsoft.Boogie { }
[Pure]
- public IEnumerator/*!*/ GetEnumerator() {
- Contract.Ensures(Contract.Result<IEnumerator>() != null);
- return ht.Keys.GetEnumerator();
- }
-
- [Pure]
public override string/*!*/ ToString() {
Contract.Ensures(Contract.Result<string>() != null);
string s = null;
@@ -211,46 +217,38 @@ namespace Microsoft.Boogie { }
}
- public bool AddAll(IEnumerable/*!*/ objs) {
- Contract.Requires(objs != null);
- foreach (object/*!*/ o in objs) {
- Contract.Assert(o != null);
- this.Add(o);
- }
- return true;
- }
//----------------------------- Static Methods ---------------------------------
// Functional Intersect
- public static Set/*!*/ Intersect(Set/*!*/ a, Set/*!*/ b) {
+ public static GSet<T>/*!*/ Intersect(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
Contract.Requires(b != null);
Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<Set>() != null);
+ Contract.Ensures(Contract.Result<GSet<T>>() != null);
//Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
- Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());
+ GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
res.Intersect(b);
return res;
}
// Functional Union
- public static Set/*!*/ Union(Set/*!*/ a, Set/*!*/ b) {
+ public static GSet<T>/*!*/ Union(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
- Contract.Ensures(Contract.Result<Set>() != null);
+ Contract.Ensures(Contract.Result<GSet<T>>() != null);
// Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
- Set/*!*/ res = (Set/*!*/)cce.NonNull(a.Clone());
+ GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
res.AddRange(b);
return res;
}
public delegate bool SetFilter(object/*!*/ obj);
- public static Set/*!*/ Filter(Set/*!*/ a, SetFilter/*!*/ filter) {
+ public static GSet<T>/*!*/ Filter(GSet<T>/*!*/ a, Func<T,bool> filter) {
Contract.Requires(filter != null);
Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<Set>() != null);
- Set inter = new Set();
+ Contract.Ensures(Contract.Result<GSet<T>>() != null);
+ GSet<T> inter = new GSet<T>();
- foreach (object/*!*/ elem in a) {
+ foreach (T elem in a) {
Contract.Assert(elem != null);
if (filter(elem)) {
inter.Add(elem);
@@ -259,8 +257,24 @@ namespace Microsoft.Boogie { return inter;
}
+ public IEnumerator<T> GetEnumerator()
+ {
+ return arr.GetEnumerator();
+ }
+
+ IEnumerator IEnumerable.GetEnumerator()
+ {
+ return ((IEnumerable)arr).GetEnumerator();
+ }
+
+ public bool AddAll(IEnumerable s)
+ {
+ foreach (T e in s) Add(e);
+ return true;
+ }
}
+
public interface IWorkList : ICollection {
bool Add(object o);
bool AddAll(IEnumerable objs);
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 5f7328d1..fc28100e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -95,6 +95,7 @@ namespace Microsoft.Boogie { using Microsoft.Boogie.AbstractInterpretation;
using AI = Microsoft.AbstractInterpretationFramework;
using Graphing;
+ using Set = GSet<object>;
[ContractClass(typeof(AbsyContracts))]
public abstract class Absy {
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 06eb3ae5..e96c3fd1 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -15,6 +15,7 @@ namespace Microsoft.Boogie { using Microsoft.Boogie.AbstractInterpretation;
using AI = Microsoft.AbstractInterpretationFramework;
using System.Diagnostics.Contracts;
+ using Set = GSet<object>;
//---------------------------------------------------------------------
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index fe5f0621..02a2f762 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -18,6 +18,8 @@ namespace Microsoft.Boogie { using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
+ using Set = GSet<object>; // not that the set used is not a set of Variable only, as it also contains TypeVariables
+
//---------------------------------------------------------------------
// Expressions
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index cae8bd92..3f798fd2 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -17,6 +17,7 @@ namespace Microsoft.Boogie { using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
+ using Set = GSet<object>;
//---------------------------------------------------------------------
// Quantifiers and general binders
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index c7950c9a..33172e7f 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -97,7 +97,7 @@ private class BvBounds : Expr { Contract.Requires(stream != null);
{Contract.Assert(false);throw new cce.UnreachableException();}
}
- public override void ComputeFreeVariables(Set/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
+ public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }
}
diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index 04bf0222..b3b02724 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -11,6 +11,7 @@ namespace Microsoft.Boogie { using System.Collections.Generic;
using System.Diagnostics;
using System.Diagnostics.Contracts;
+ using Set = GSet<object>;
public static class LambdaHelper {
public static Absy Desugar(Absy node, out List<Expr/*!*/>/*!*/ axioms, out List<Function/*!*/>/*!*/ functions) {
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 5bfbbfc2..3602339e 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -116,7 +116,7 @@ private class BvBounds : Expr { Contract.Requires(stream != null);
{Contract.Assert(false);throw new cce.UnreachableException();}
}
- public override void ComputeFreeVariables(Set/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
+ public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }
public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 5e33e78d..f1d06590 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -37,29 +37,29 @@ namespace GPUVerify private const string _Y_name = "_Y";
private const string _Z_name = "_Z";
- private Constant _TILE_SIZE_X = null;
- private Constant _TILE_SIZE_Y = null;
- private Constant _TILE_SIZE_Z = null;
+ private Constant _GROUP_SIZE_X = null;
+ private Constant _GROUP_SIZE_Y = null;
+ private Constant _GROUP_SIZE_Z = null;
- private const string _TILE_SIZE_X_name = "_TILE_SIZE_X";
- private const string _TILE_SIZE_Y_name = "_TILE_SIZE_Y";
- private const string _TILE_SIZE_Z_name = "_TILE_SIZE_Z";
+ private const string _GROUP_SIZE_X_name = "_GROUP_SIZE_X";
+ private const string _GROUP_SIZE_Y_name = "_GROUP_SIZE_Y";
+ private const string _GROUP_SIZE_Z_name = "_GROUP_SIZE_Z";
- private Constant _TILE_X = null;
- private Constant _TILE_Y = null;
- private Constant _TILE_Z = null;
+ private Constant _GROUP_X = null;
+ private Constant _GROUP_Y = null;
+ private Constant _GROUP_Z = null;
- private const string _TILE_X_name = "_TILE_X";
- private const string _TILE_Y_name = "_TILE_Y";
- private const string _TILE_Z_name = "_TILE_Z";
+ private const string _GROUP_X_name = "_GROUP_X";
+ private const string _GROUP_Y_name = "_GROUP_Y";
+ private const string _GROUP_Z_name = "_GROUP_Z";
- private Constant _NUM_TILES_X = null;
- private Constant _NUM_TILES_Y = null;
- private Constant _NUM_TILES_Z = null;
+ private Constant _NUM_GROUPS_X = null;
+ private Constant _NUM_GROUPS_Y = null;
+ private Constant _NUM_GROUPS_Z = null;
- private const string _NUM_TILES_X_name = "_NUM_TILES_X";
- private const string _NUM_TILES_Y_name = "_NUM_TILES_Y";
- private const string _NUM_TILES_Z_name = "_NUM_TILES_Z";
+ private const string _NUM_GROUPS_X_name = "_NUM_GROUPS_X";
+ private const string _NUM_GROUPS_Y_name = "_NUM_GROUPS_Y";
+ private const string _NUM_GROUPS_Z_name = "_NUM_GROUPS_Z";
public IRaceInstrumenter RaceInstrumenter;
@@ -113,6 +113,11 @@ namespace GPUVerify continue;
}
+ if (decl is Implementation)
+ {
+ continue;
+ }
+
if (decl is Procedure)
{
if (attributedProcedure == null)
@@ -143,9 +148,9 @@ namespace GPUVerify {
foreach (LocalVariable LV in KernelImplementation.LocVars)
{
- if (QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))
+ if (QKeyValue.FindBoolAttribute(LV.Attributes, "group_shared"))
{
- Error(LV.tok, "Local variable must not be marked 'tile_static' -- promote the variable to global scope");
+ Error(LV.tok, "Local variable must not be marked 'group_shared' -- promote the variable to global scope");
}
}
}
@@ -158,11 +163,11 @@ namespace GPUVerify {
if (!ReservedNames.Contains((D as Variable).Name))
{
- if (QKeyValue.FindBoolAttribute(D.Attributes, "tile_static"))
+ if (QKeyValue.FindBoolAttribute(D.Attributes, "group_shared"))
{
- NonLocalState.getTileStaticVariables().Add(D as Variable);
+ NonLocalState.getGroupSharedVariables().Add(D as Variable);
}
- else
+ else if(QKeyValue.FindBoolAttribute(D.Attributes, "global"))
{
NonLocalState.getGlobalVariables().Add(D as Variable);
}
@@ -186,50 +191,50 @@ namespace GPUVerify CheckSpecialConstantType(C);
_Z = C;
}
- if (C.Name.Equals(_TILE_SIZE_X_name))
+ if (C.Name.Equals(_GROUP_SIZE_X_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_X = C;
+ _GROUP_SIZE_X = C;
}
- if (C.Name.Equals(_TILE_SIZE_Y_name))
+ if (C.Name.Equals(_GROUP_SIZE_Y_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_Y = C;
+ _GROUP_SIZE_Y = C;
}
- if (C.Name.Equals(_TILE_SIZE_Z_name))
+ if (C.Name.Equals(_GROUP_SIZE_Z_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_Z = C;
+ _GROUP_SIZE_Z = C;
}
- if (C.Name.Equals(_TILE_X_name))
+ if (C.Name.Equals(_GROUP_X_name))
{
CheckSpecialConstantType(C);
- _TILE_X = C;
+ _GROUP_X = C;
}
- if (C.Name.Equals(_TILE_Y_name))
+ if (C.Name.Equals(_GROUP_Y_name))
{
CheckSpecialConstantType(C);
- _TILE_Y = C;
+ _GROUP_Y = C;
}
- if (C.Name.Equals(_TILE_Z_name))
+ if (C.Name.Equals(_GROUP_Z_name))
{
CheckSpecialConstantType(C);
- _TILE_Z = C;
+ _GROUP_Z = C;
}
- if (C.Name.Equals(_NUM_TILES_X_name))
+ if (C.Name.Equals(_NUM_GROUPS_X_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_X = C;
+ _NUM_GROUPS_X = C;
}
- if (C.Name.Equals(_NUM_TILES_Y_name))
+ if (C.Name.Equals(_NUM_GROUPS_Y_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_Y = C;
+ _NUM_GROUPS_Y = C;
}
- if (C.Name.Equals(_NUM_TILES_Z_name))
+ if (C.Name.Equals(_NUM_GROUPS_Z_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_Z = C;
+ _NUM_GROUPS_Z = C;
}
}
@@ -866,49 +871,49 @@ namespace GPUVerify return _Z != null;
}
- public bool KernelHasTileIdX()
+ public bool KernelHasGroupIdX()
{
- return _TILE_X != null;
+ return _GROUP_X != null;
}
- public bool KernelHasTileIdY()
+ public bool KernelHasGroupIdY()
{
- return _TILE_Y != null;
+ return _GROUP_Y != null;
}
- public bool KernelHasTileIdZ()
+ public bool KernelHasGroupIdZ()
{
- return _TILE_Z != null;
+ return _GROUP_Z != null;
}
- public bool KernelHasNumTilesX()
+ public bool KernelHasNumGroupsX()
{
- return _NUM_TILES_X != null;
+ return _NUM_GROUPS_X != null;
}
- public bool KernelHasNumTilesY()
+ public bool KernelHasNumGroupsY()
{
- return _NUM_TILES_Y != null;
+ return _NUM_GROUPS_Y != null;
}
- public bool KernelHasNumTilesZ()
+ public bool KernelHasNumGroupsZ()
{
- return _NUM_TILES_Z != null;
+ return _NUM_GROUPS_Z != null;
}
- public bool KernelHasTileSizeX()
+ public bool KernelHasGroupSizeX()
{
- return _TILE_SIZE_X != null;
+ return _GROUP_SIZE_X != null;
}
- public bool KernelHasTileSizeY()
+ public bool KernelHasGroupSizeY()
{
- return _TILE_SIZE_Y != null;
+ return _GROUP_SIZE_Y != null;
}
- public bool KernelHasTileSizeZ()
+ public bool KernelHasGroupSizeZ()
{
- return _TILE_SIZE_Z != null;
+ return _GROUP_SIZE_Z != null;
}
public bool KernelHasId(string dimension)
@@ -1129,17 +1134,17 @@ namespace GPUVerify if (GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)))
{
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetTileSize(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetGroupSize(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumGroups(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetGroupId(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)))));
}
else
{
- Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetTileSize(dimension)), Zero(tok))));
- Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));
- Proc.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));
- Proc.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetGroupSize(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumGroups(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetGroupId(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)))));
}
}
@@ -1159,8 +1164,8 @@ namespace GPUVerify MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), ZeroBV(tok))
),
Expr.And(
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetTileSize(dimension))),
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetTileSize(dimension)))
+ MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
+ MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
))
:
Expr.And(
@@ -1169,8 +1174,8 @@ namespace GPUVerify Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), Zero(tok))
),
Expr.And(
- Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetTileSize(dimension))),
- Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetTileSize(dimension)))
+ Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
+ Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
));
AssumeThreadIdsInRange = (null == AssumeThreadIdsInRange) ? AssumeThreadIdsInRangeInDimension : Expr.And(AssumeThreadIdsInRange, AssumeThreadIdsInRangeInDimension);
@@ -1185,22 +1190,22 @@ namespace GPUVerify }), new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "result", Microsoft.Boogie.Type.Bool)))), new ExprSeq(new Expr[] { lhs, rhs }));
}
- private Constant GetTileSize(string dimension)
+ private Constant GetGroupSize(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _TILE_SIZE_X;
- if (dimension.Equals("Y")) return _TILE_SIZE_Y;
- if (dimension.Equals("Z")) return _TILE_SIZE_Z;
+ if (dimension.Equals("X")) return _GROUP_SIZE_X;
+ if (dimension.Equals("Y")) return _GROUP_SIZE_Y;
+ if (dimension.Equals("Z")) return _GROUP_SIZE_Z;
Debug.Assert(false);
return null;
}
- private Constant GetNumTiles(string dimension)
+ private Constant GetNumGroups(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _NUM_TILES_X;
- if (dimension.Equals("Y")) return _NUM_TILES_Y;
- if (dimension.Equals("Z")) return _NUM_TILES_Z;
+ if (dimension.Equals("X")) return _NUM_GROUPS_X;
+ if (dimension.Equals("Y")) return _NUM_GROUPS_Y;
+ if (dimension.Equals("Z")) return _NUM_GROUPS_Z;
Debug.Assert(false);
return null;
}
@@ -1217,12 +1222,12 @@ namespace GPUVerify return new Constant(tok, new TypedIdent(tok, "_" + dimension + "$" + number, GetTypeOfId(dimension)));
}
- private Constant GetTileId(string dimension)
+ private Constant GetGroupId(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _TILE_X;
- if (dimension.Equals("Y")) return _TILE_Y;
- if (dimension.Equals("Z")) return _TILE_Z;
+ if (dimension.Equals("X")) return _GROUP_X;
+ if (dimension.Equals("Y")) return _GROUP_Y;
+ if (dimension.Equals("Z")) return _GROUP_Z;
Debug.Assert(false);
return null;
}
@@ -1436,7 +1441,7 @@ namespace GPUVerify foreach (Variable v in impl.LocVars)
{
- Debug.Assert(!NonLocalState.getTileStaticVariables().Contains(v));
+ Debug.Assert(!NonLocalState.getGroupSharedVariables().Contains(v));
NewLocVars.Add(v);
}
@@ -2184,22 +2189,22 @@ namespace GPUVerify Error(KernelProcedure.tok, "Kernel must declare global constant '" + _X_name + "'");
}
- if (!KernelHasTileSizeX())
+ if (!KernelHasGroupSizeX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _TILE_SIZE_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _GROUP_SIZE_X_name + "'");
}
- if (!KernelHasNumTilesX())
+ if (!KernelHasNumGroupsX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _NUM_TILES_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _NUM_GROUPS_X_name + "'");
}
- if (!KernelHasTileIdX())
+ if (!KernelHasGroupIdX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _TILE_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _GROUP_X_name + "'");
}
- if (KernelHasIdY() || KernelHasTileSizeY() || KernelHasNumTilesY() || KernelHasTileIdY())
+ if (KernelHasIdY() || KernelHasGroupSizeY() || KernelHasNumGroupsY() || KernelHasGroupIdY())
{
if (!KernelHasIdY())
@@ -2207,24 +2212,24 @@ namespace GPUVerify Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _Y_name + "'");
}
- if (!KernelHasTileSizeY())
+ if (!KernelHasGroupSizeY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _TILE_SIZE_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _GROUP_SIZE_Y_name + "'");
}
- if (!KernelHasNumTilesY())
+ if (!KernelHasNumGroupsY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _NUM_TILES_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _NUM_GROUPS_Y_name + "'");
}
- if (!KernelHasTileIdY())
+ if (!KernelHasGroupIdY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _TILE_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _GROUP_Y_name + "'");
}
}
- if (KernelHasIdZ() || KernelHasTileSizeZ() || KernelHasNumTilesZ() || KernelHasTileIdZ())
+ if (KernelHasIdZ() || KernelHasGroupSizeZ() || KernelHasNumGroupsZ() || KernelHasGroupIdZ())
{
if (!KernelHasIdY())
@@ -2232,19 +2237,19 @@ namespace GPUVerify Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _Y_name + "'");
}
- if (!KernelHasTileSizeY())
+ if (!KernelHasGroupSizeY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_SIZE_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_SIZE_Y_name + "'");
}
- if (!KernelHasNumTilesY())
+ if (!KernelHasNumGroupsY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_TILES_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_GROUPS_Y_name + "'");
}
- if (!KernelHasTileIdY())
+ if (!KernelHasGroupIdY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_Y_name + "'");
}
if (!KernelHasIdZ())
@@ -2252,19 +2257,19 @@ namespace GPUVerify Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _Z_name + "'");
}
- if (!KernelHasTileSizeZ())
+ if (!KernelHasGroupSizeZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_SIZE_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_SIZE_Z_name + "'");
}
- if (!KernelHasNumTilesZ())
+ if (!KernelHasNumGroupsZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_TILES_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_GROUPS_Z_name + "'");
}
- if (!KernelHasTileIdZ())
+ if (!KernelHasGroupIdZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_Z_name + "'");
}
}
@@ -2272,41 +2277,6 @@ namespace GPUVerify return ErrorCount;
}
- private bool HasNamedConstant(string dimension, string Name)
- {
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (d is Variable && (d as Variable).Name.Equals(Name + dimension))
- {
- Variable v = d as Variable;
- if (v is Constant && IsIntOrBv32(v.TypedIdent.Type))
- {
- return true;
- }
- else
- {
- Error(v.tok, "Declaration '" + Name + dimension + "' must be a constant integer");
- }
- }
- }
- return false;
- }
-
- private bool HasTileId(string dimension)
- {
- return HasNamedConstant(dimension, "_tile_");
- }
-
- private bool HasNumTiles(string dimension)
- {
- return HasNamedConstant(dimension, "NUM_TILES_");
- }
-
- private bool HasTileSize(string dimension)
- {
- return HasNamedConstant(dimension, "TILE_SIZE_");
- }
-
public static bool IsThreadLocalIdConstant(Variable variable)
{
return variable is Constant && (variable.Name.Equals(_X_name) || variable.Name.Equals(_Y_name) || variable.Name.Equals(_Z_name));
diff --git a/Source/GPUVerify/INonLocalState.cs b/Source/GPUVerify/INonLocalState.cs index 0e03d685..c6211dab 100644 --- a/Source/GPUVerify/INonLocalState.cs +++ b/Source/GPUVerify/INonLocalState.cs @@ -11,7 +11,7 @@ namespace GPUVerify ICollection<Variable> getGlobalVariables();
- ICollection<Variable> getTileStaticVariables();
+ ICollection<Variable> getGroupSharedVariables();
ICollection<Variable> getAllNonLocalVariables();
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index e38aabea..1be30dc9 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -97,11 +97,11 @@ namespace GPUVerify Variable newG = findClonedVar(v, newGp.NonLocalState.getGlobalVariables());
- Variable newT = findClonedVar(v, newGp.NonLocalState.getTileStaticVariables());
+ Variable newT = findClonedVar(v, newGp.NonLocalState.getGroupSharedVariables());
Contract.Assert(newG == null || newT == null);
ri.NonLocalStateToCheck.getGlobalVariables().Clear();
- ri.NonLocalStateToCheck.getTileStaticVariables().Clear();
+ ri.NonLocalStateToCheck.getGroupSharedVariables().Clear();
ri.onlyLog1 = a1;
ri.onlyLog2 = a2;
@@ -112,7 +112,7 @@ namespace GPUVerify if (newT != null)
{
- ri.NonLocalStateToCheck.getTileStaticVariables().Add(newT);
+ ri.NonLocalStateToCheck.getGroupSharedVariables().Add(newT);
}
newGp.doit();
diff --git a/Source/GPUVerify/NonLocalStateLists.cs b/Source/GPUVerify/NonLocalStateLists.cs index a4b5e154..c47cddd5 100644 --- a/Source/GPUVerify/NonLocalStateLists.cs +++ b/Source/GPUVerify/NonLocalStateLists.cs @@ -10,12 +10,12 @@ namespace GPUVerify class NonLocalStateLists : INonLocalState
{
private List<Variable> GlobalVariables;
- private List<Variable> TileStaticVariables;
+ private List<Variable> GroupSharedVariables;
public NonLocalStateLists()
{
GlobalVariables = new List<Variable>();
- TileStaticVariables = new List<Variable>();
+ GroupSharedVariables = new List<Variable>();
}
public ICollection<Variable> getGlobalVariables()
@@ -23,16 +23,16 @@ namespace GPUVerify return GlobalVariables;
}
- public ICollection<Variable> getTileStaticVariables()
+ public ICollection<Variable> getGroupSharedVariables()
{
- return TileStaticVariables;
+ return GroupSharedVariables;
}
public ICollection<Variable> getAllNonLocalVariables()
{
List<Variable> all = new List<Variable>();
all.AddRange(GlobalVariables);
- all.AddRange(TileStaticVariables);
+ all.AddRange(GroupSharedVariables);
return all;
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 4f2f76be..692f1288 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -38,9 +38,9 @@ namespace GPUVerify {
NonLocalStateToCheck.getGlobalVariables().Add(v);
}
- foreach(Variable v in verifier.NonLocalState.getTileStaticVariables())
+ foreach(Variable v in verifier.NonLocalState.getGroupSharedVariables())
{
- NonLocalStateToCheck.getTileStaticVariables().Add(v);
+ NonLocalStateToCheck.getGroupSharedVariables().Add(v);
}
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6752a2b7..26361cdf 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -15,8 +15,10 @@ using AI = Microsoft.AbstractInterpretationFramework; using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
+using Set = Microsoft.Boogie.GSet<object>;
namespace Microsoft.Boogie {
+
public class CalleeCounterexampleInfo {
public Counterexample counterexample;
public List<Model.Element>/*!>!*/ args;
|