diff options
Diffstat (limited to 'gcc/profile.c')
| -rw-r--r-- | gcc/profile.c | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/gcc/profile.c b/gcc/profile.c index bde8b4677f9..2334101ba8c 100644 --- a/gcc/profile.c +++ b/gcc/profile.c @@ -409,8 +409,17 @@ read_profile_edge_counts (gcov_type *exec_counts) e->count = exec_counts[exec_counts_pos++]; if (e->count > profile_info->sum_max) { - error ("corrupted profile info: edge from %i to %i exceeds maximal count", - bb->index, e->dest->index); + if (flag_profile_correction) + { + static bool informed = 0; + if (!informed) + inform (input_location, + "corrupted profile info: edge count exceeds maximal count"); + informed = 1; + } + else + error ("corrupted profile info: edge from %i to %i exceeds maximal count", + bb->index, e->dest->index); } } else |
