Changeset 3038


Ignore:
Timestamp:
Mar 29, 2013, 5:27:54 PM (4 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:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/clightPrinter.ml

    r3025 r3038  
    655655  | Cost_instrumented _ ->
    656656      fprintf str_formatter "int __cost = 0;@\n@\n";
     657      fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";
    657658      fprintf str_formatter "void __cost_incr(int incr) {@\n";
    658659      fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n";
    659       fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";
    660660      fprintf str_formatter "void __stack_size_incr(int incr) {@\n";
    661661      fprintf str_formatter "  __stack_size = __stack_size + incr;@\n";
Note: See TracChangeset for help on using the changeset viewer.