diff options
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 36 |
1 files changed, 2 insertions, 34 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index a9c41efb..e5e3e549 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -312,9 +312,6 @@ namespace Microsoft.Boogie { seeker.Visit(d);
}
}
-
- AxiomExpander expander = new AxiomExpander(this, tc);
- expander.CollectExpansions();
}
public void ComputeStronglyConnectedComponents() {
@@ -761,7 +758,7 @@ namespace Microsoft.Boogie { Graph<Block> g = ProcessLoops(impl);
CreateProceduresForLoops(impl, g, loopImpls, fullMap);
}
- catch (IrreducibleLoopException e)
+ catch (IrreducibleLoopException)
{
System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name));
fullMap[impl.Name] = null;
@@ -1766,43 +1763,14 @@ namespace Microsoft.Boogie { }
}
- public class Expansion {
- public string ignore; // when to ignore
- public Expr/*!*/ body;
- public TypeVariableSeq/*!*/ TypeParameters;
- public Variable[]/*!*/ formals;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(body != null);
- Contract.Invariant(TypeParameters != null);
- Contract.Invariant(formals != null);
- }
-
-
- public Expansion(string ignore, Expr body,
- TypeVariableSeq/*!*/ typeParams, Variable[] formals) {
- Contract.Requires(typeParams != null);
- Contract.Requires(formals != null);
- Contract.Requires(body != null);
- this.ignore = ignore;
- this.body = body;
- this.TypeParameters = typeParams;
- this.formals = formals;
- }
- }
+
public class Function : DeclWithFormals {
public string Comment;
// the body is only set if the function is declared with {:inline}
public Expr Body;
- public List<Expansion/*!*/> expansions;
public bool doingExpansion;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(expansions, true));
- }
-
private bool neverTrigger;
private bool neverTriggerComputed;
|