diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-09-28 09:03:03 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-09-28 09:03:03 +0530 |
| commit | 20b063e0fe89ab1588044d5f6946595764caa5e4 (patch) | |
| tree | 57ff71bbfa6114c94c3a5a7b8a1371809cbce33f /Source | |
| parent | 811b680ba5dfdbbe495729f7e6dcf024f3c4aabe (diff) | |
Bug fix to stratified inlining error trace values
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 4533363f..4fa339ee 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -3162,8 +3162,9 @@ namespace VC orderedStateIds.Add(new Tuple<int, int>(candidateId, foo));
}
}
-
- if (calleeName.StartsWith(recordProcName)) {
+
+ if (calleeName.StartsWith(recordProcName))
+ {
var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
// Record concrete value of the argument to this procedure
@@ -3172,6 +3173,14 @@ namespace VC {
args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));
}
+ else if (expr == VCExpressionGenerator.True)
+ {
+ args.Add(errModel.MkElement("true"));
+ }
+ else if (expr == VCExpressionGenerator.False)
+ {
+ args.Add(errModel.MkElement("false"));
+ }
else if (expr is VCExprVar)
{
var idExpr = expr as VCExprVar;
|