diff options
| author |  qadeer <unknown> | 2014-06-28 23:34:19 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-06-28 23:34:19 -0700 |
| commit | 55477dfd35b4e3da6063a622b65b5d0b0f321e70 (patch) | |
| tree | 852dba975b8b4ce6d26fc419169eb0f7a7039783 | |
| parent | f02c52549b82f44200a45f1fad528ec2f1e2fa1d (diff) | |
a fix in Inline method; it should look for inline attribute only on procedures and implementations
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 2f75b234..5e1d75ed 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -726,6 +726,10 @@ namespace Microsoft.Boogie public static void Inline(Program program)
{
Contract.Requires(program != null);
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Inlining...");
+
// Inline
var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);
@@ -734,10 +738,10 @@ namespace Microsoft.Boogie bool inline = false;
foreach (var d in TopLevelDeclarations)
{
- if (d.FindExprAttribute("inline") != null)
- {
- inline = true;
- }
+ if ((d is Procedure || d is Implementation) && d.FindExprAttribute("inline") != null)
+ {
+ inline = true;
+ }
}
if (inline)
{
|