| Line | |
|---|
| 1 | (** This module defines the labelling of a [Clight] program. *) |
|---|
| 2 | |
|---|
| 3 | (** [add_cost_labels prog] inserts some labels to enable |
|---|
| 4 | cost annotation. |
|---|
| 5 | |
|---|
| 6 | The labelling of a function proceeds as follows: |
|---|
| 7 | |
|---|
| 8 | - A label is added at the beginning of the function. |
|---|
| 9 | |
|---|
| 10 | - For each branching instruction in the function, a cost label is added at |
|---|
| 11 | the beginning of each branch. The concerned instructions are: |
|---|
| 12 | - ternary expressions (includind boolean 'and' and 'or' operators that are |
|---|
| 13 | transformed at this point); |
|---|
| 14 | - conditionals; |
|---|
| 15 | - loops; |
|---|
| 16 | - switches. |
|---|
| 17 | |
|---|
| 18 | - For each label instruction in the function, a cost label is added after |
|---|
| 19 | the label, in order to capture loops potentially created by gotos. |
|---|
| 20 | *) |
|---|
| 21 | |
|---|
| 22 | val add_cost_labels : Clight.program -> Clight.program |
|---|
Note: See
TracBrowser
for help on using the repository browser.
