diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-05-30 14:19:45 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-05-30 14:19:45 -0700 |
| commit | 983156082a30529f11721e126705f9999923782a (patch) | |
| tree | aaf95551285581d961941cc32d842f17d0535166 /Source/VCGeneration | |
| parent | df064f4251f40f26f3ce0e86cc1a26f529196492 (diff) | |
moved a couple of overrides from StratifiedVCGen to StratifiedVCGenBase
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 82 |
1 files changed, 41 insertions, 41 deletions
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index cb507cfc..89c82a91 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -427,6 +427,47 @@ namespace VC { exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
}
}
+
+ public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {
+ // Construct the set of inlined procs in the original program
+ var inlinedProcs = new HashSet<string>();
+ foreach (var decl in program.TopLevelDeclarations) {
+ // Implementations
+ if (decl is Implementation) {
+ var impl = decl as Implementation;
+ if (!(impl.Proc is LoopProcedure)) {
+ inlinedProcs.Add(impl.Name);
+ }
+ }
+
+ // And recording procedures
+ if (decl is Procedure) {
+ var proc = decl as Procedure;
+ if (proc.Name.StartsWith(recordProcName)) {
+ Debug.Assert(!(decl is LoopProcedure));
+ inlinedProcs.Add(proc.Name);
+ }
+ }
+ }
+
+ return extractLoopTraceRec(
+ new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
+ mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ }
+
+ protected override bool elIsLoop(string procname) {
+ StratifiedInliningInfo info = null;
+ if (implName2StratifiedInliningInfo.ContainsKey(procname)) {
+ info = implName2StratifiedInliningInfo[procname];
+ }
+
+ if (info == null) return false;
+
+ var lp = info.impl.Proc as LoopProcedure;
+
+ if (lp == null) return false;
+ return true;
+ }
}
public class StratifiedVCGen : StratifiedVCGenBase {
@@ -2642,47 +2683,6 @@ namespace VC { }
}
- public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {
- // Construct the set of inlined procs in the original program
- var inlinedProcs = new HashSet<string>();
- foreach (var decl in program.TopLevelDeclarations) {
- // Implementations
- if (decl is Implementation) {
- var impl = decl as Implementation;
- if (!(impl.Proc is LoopProcedure)) {
- inlinedProcs.Add(impl.Name);
- }
- }
-
- // And recording procedures
- if (decl is Procedure) {
- var proc = decl as Procedure;
- if (proc.Name.StartsWith(recordProcName)) {
- Debug.Assert(!(decl is LoopProcedure));
- inlinedProcs.Add(proc.Name);
- }
- }
- }
-
- return extractLoopTraceRec(
- new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
- mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
- }
-
- protected override bool elIsLoop(string procname) {
- StratifiedInliningInfo info = null;
- if (implName2StratifiedInliningInfo.ContainsKey(procname)) {
- info = implName2StratifiedInliningInfo[procname];
- }
-
- if (info == null) return false;
-
- var lp = info.impl.Proc as LoopProcedure;
-
- if (lp == null) return false;
- return true;
- }
-
} // class StratifiedVCGen
} // namespace VC
|