diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index a66624a0fd68623c39c61a95fa1ae66b0a92110d..7f5b53a7cd886e40910c5a6f71ce238aa23bd5d7 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -63,10 +63,16 @@ open Cil_types open Cil_datatype let stripUnderscore s = - let res = Extlib.strip_underscore s in - if res = "" then - Kernel.error ~once:true ~current:true "Invalid attribute name %s" s; - res + if String.length s = 1 then begin + if s = "_" then + Kernel.error ~once:true ~current:true "Invalid attribute name %s" s; + s + end else begin + let res = Extlib.strip_underscore s in + if res = "" then + Kernel.error ~once:true ~current:true "Invalid attribute name %s" s; + res + end let frama_c_keep_block = "FRAMA_C_KEEP_BLOCK" let () = Cil_printer.register_shallow_attribute frama_c_keep_block diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml index df326129833953442984d3dac9344f93890f5990..8e5d2022b9ead6818cc53c369c0a4f79d9f6d72a 100644 --- a/src/libraries/stdlib/extlib.ml +++ b/src/libraries/stdlib/extlib.ml @@ -477,11 +477,11 @@ let make_unique_name mem ?(sep=" ") ?(start=2) from = let strip_underscore s = let l = String.length s in let rec start i = - if i >= l then l-1 + if i >= l then l else if s.[i] = '_' then start (i + 1) else i in let st = start 0 in - if st = l - 1 then "" + if st = l then "" else begin let rec finish i = (* We know that we will stop at >= st >= 0 *) diff --git a/tests/syntax/attributes-declarations-definitions.c b/tests/syntax/attributes-declarations-definitions.c index 82a097052500564c5c727a77eca45e7fba8e9a4d..9c7daac462a74b6a5bef1b04b25a5b304a9ed330 100644 --- a/tests/syntax/attributes-declarations-definitions.c +++ b/tests/syntax/attributes-declarations-definitions.c @@ -45,3 +45,9 @@ iptr volatile h(const iptr ip3); void test(void) { int a, __attribute__((unused)) b; } + +int __attribute__((o)) one_letter_attribute; + +int __attribute__((_n)) one_letter_attribute_with_underscore; + +int __attribute__((e_)) one_letter_attribute_with_underscore_after; diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle index 40ab5bd3e4c647a6c27382809667e8c55a56a5e6..52cada7b7752aba80dfc8e145419f29b41a97db7 100644 --- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle +++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle @@ -49,4 +49,7 @@ void test(void) return; } +int __attribute__((__o__)) one_letter_attribute; +int __attribute__((__n__)) one_letter_attribute_with_underscore; +int __attribute__((__e__)) one_letter_attribute_with_underscore_after;