diff options
Diffstat (limited to 'Source/Houdini')
| -rw-r--r-- | Source/Houdini/Houdini.cs | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 1b03c507..79c6fb77 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -268,7 +268,7 @@ namespace Microsoft.Boogie.Houdini { Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();
foreach (Declaration decl in program.TopLevelDeclarations) {
Implementation impl = decl as Implementation;
- if (impl != null) {
+ if (impl != null && !impl.SkipVerification) {
impls.Add(impl);
}
}
@@ -309,13 +309,13 @@ namespace Microsoft.Boogie.Houdini { }
foreach (Declaration decl in program.TopLevelDeclarations) {
Implementation impl = decl as Implementation;
- if (impl == null) continue;
+ if (impl == null || impl.SkipVerification) continue;
callGraph.AddSource(impl);
procToImpls[impl.Proc].Add(impl);
}
foreach (Declaration decl in program.TopLevelDeclarations) {
Implementation impl = decl as Implementation;
- if (impl == null) continue;
+ if (impl == null || impl.SkipVerification) continue;
foreach (Block b in impl.Blocks) {
foreach (Cmd c in b.Cmds) {
CallCmd cc = c as CallCmd;
@@ -333,9 +333,8 @@ namespace Microsoft.Boogie.Houdini { Queue<Implementation> queue = new Queue<Implementation>();
foreach (Declaration decl in program.TopLevelDeclarations) {
Implementation impl = decl as Implementation;
- if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {
- queue.Enqueue(impl);
- }
+ if (impl == null || impl.SkipVerification) continue;
+ queue.Enqueue(impl);
}
return queue;
}
|