diff options
| author |  rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
| commit | 554fb3a6780c412b81dc935835c2760e4cbe0b4d (patch) | |
| tree | b50aa3dbbb369a52751bfcb9f142c9c928e591ae /Source/AbsInt | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/LoopInvariantsOnDemand.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs index 49958289..5bb5916d 100644 --- a/Source/AbsInt/LoopInvariantsOnDemand.cs +++ b/Source/AbsInt/LoopInvariantsOnDemand.cs @@ -55,6 +55,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { return VisitFunApp((AI.IFunApp)expr);
else if (expr is AI.IFunction)
return VisitFunction((AI.IFunction)expr);
+ else if (expr is AI.IUnknown)
+ return null;
else {
Contract.Assert(false);
throw new cce.UnreachableException();
|