- Timestamp:
- Mar 29, 2013, 5:27:54 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
driver/clightPrinter.ml
r3025 r3038 655 655 | Cost_instrumented _ -> 656 656 fprintf str_formatter "int __cost = 0;@\n@\n"; 657 fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n"; 657 658 fprintf str_formatter "void __cost_incr(int incr) {@\n"; 658 659 fprintf str_formatter " __cost = __cost + incr;@\n}@\n@\n"; 659 fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";660 660 fprintf str_formatter "void __stack_size_incr(int incr) {@\n"; 661 661 fprintf str_formatter " __stack_size = __stack_size + incr;@\n";
Note: See TracChangeset
for help on using the changeset viewer.