Project

General

Profile

Bug #5407

Duplicated labels are generated

Added by Vadim Mutilin over 4 years ago. Updated 3 months ago.

Status:
Closed
Priority:
Urgent
Category:
C back-end
Start date:
11/05/2014
Due date:
% Done:

0%

Estimated time:
Detected in build:
2c42610
Platform:
Published in build:

Description

For the driver

linux-3.17-rc1.tar.xz    32_7a    net/rds/rds.ko

For the function rds_page_copy_user

 64         if (to_user) {
 65                 rds_stats_add(s_copy_to_user, bytes);
 66                 ret = copy_to_user(ptr, addr + offset, bytes);
 67         } else {
 68                 rds_stats_add(s_copy_from_user, bytes);
 69                 ret = copy_from_user(addr + offset, ptr, bytes);
 70         }

CPAchecker and GCC report an error

Error: Parsing failed (net/rds/page.o.i, line 74772: Duplicate label ldv_51354 in function rds_page_copy_user: ldv_51354:;) (EclipseCParser.buildCFA, SEVERE) 

It looks like this macro is apllied (or some similar)

308 #define __pcpu_size_call_return(stem, variable)                         \
309 ({                                                                      \
310         typeof(variable) pscr_ret__;                                    \
311         __verify_pcpu_ptr(&(variable));                                 \
312         switch(sizeof(variable)) {                                      \
313         case 1: pscr_ret__ = stem##1(variable); break;                  \
314         case 2: pscr_ret__ = stem##2(variable); break;                  \
315         case 4: pscr_ret__ = stem##4(variable); break;                  \
316         case 8: pscr_ret__ = stem##8(variable); break;                  \
317         default:                                                        \
318                 __bad_size_call_parameter(); break;                     \
319         }                                                               \
320         pscr_ret__;                                                     \
321 })

For two switches label with the same names are generated. Look into the attached file.


Files

page.o.i.zip (373 KB) page.o.i.zip Vadim Mutilin, 11/05/2014 09:13 PM

Related issues

Has duplicate C Instrumentation Framework - Bug #7895: Parsing failed: Duplicate label in CPAchecker inputRejected01/24/2017

Actions
Has duplicate C Instrumentation Framework - Bug #9534: Incorrect printing of Linux BUILD_BUG_ONRejected03/13/2019

Actions
Blocks Klever - Feature #9536: Update CIFClosed03/13/2019

Actions

History

#1

Updated by Evgeny Novikov over 4 years ago

  • Status changed from New to Open
  • Assignee set to Evgeny Novikov
#2

Updated by Evgeny Novikov over 3 years ago

  • Category set to C back-end
  • Priority changed from Normal to High
#3

Updated by Vadim Mutilin over 2 years ago

The priority is raised due to #7895
Affects module drivers/rtc/rtc-core.ko

#4

Updated by Alexey Khoroshilov over 2 years ago

As a "simple task" we should check if we can have a workaround as a redefinition for #define per_cpu(var, cpu) or something like this.

#5

Updated by Evgeny Novikov 3 months ago

#6

Updated by Evgeny Novikov 3 months ago

  • Priority changed from High to Urgent

This also confuses Frama-C (CIL). Perhaps the issue has the same reasons as #9534.

#7

Updated by Evgeny Novikov 3 months ago

  • Related to Bug #9534: Incorrect printing of Linux BUILD_BUG_ON added
#8

Updated by Evgeny Novikov 3 months ago

  • Related to deleted (Bug #9534: Incorrect printing of Linux BUILD_BUG_ON)
#9

Updated by Evgeny Novikov 3 months ago

  • Has duplicate Bug #9534: Incorrect printing of Linux BUILD_BUG_ON added
#10

Updated by Evgeny Novikov 3 months ago

  • Status changed from Open to Closed

I fixed the issue in d9d5f93. The cause of this issue was that GCC computes some values and add artificial tree nodes for them. Now C back-end just skips them completely. BTW, there already was TODO that suggested to do this.

Also available in: Atom PDF