Changeset 3038 for driver

Timestamp:

Mar 29, 2013, 5:27:54 PM (8 years ago)

Author:

sacerdot

Message:

Bug fixed: the stack_cost* variables must be declared before the
functions that manipulate them for the plug-in to work properly.

File:

• driver/clightPrinter.ml (modified) (1 diff)

driver/clightPrinter.ml

@@ -655 +655 @@
   | Cost_instrumented _ ->
       fprintf str_formatter "int __cost = 0;@\n@\n";
+      fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";
       fprintf str_formatter "void __cost_incr(int incr) {@\n";
       fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n";
-      fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";
       fprintf str_formatter "void __stack_size_incr(int incr) {@\n";
       fprintf str_formatter "  __stack_size = __stack_size + incr;@\n";