diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 75c2da8a093025837852d9a46bbc43b64ae07202..1f1ea2fcb0cdaf437cda8ffc33285e3eaff6e061 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -2077,10 +2077,8 @@ class cil_printer () = object (self) in let name' fmt = if filter_printing_attributes a = [] then pname fmt false - else if nameOpt = None then - printAttributes fmt a - else - fprintf fmt "(%a%a)" printAttributes a pname true + else if nameOpt = None then printAttributes fmt a + else fprintf fmt "(%a%a)" printAttributes a pname true in self#typ (Some (fun fmt -> @@ -2096,7 +2094,7 @@ class cil_printer () = object (self) | TFun (restyp, args, isvararg, a) -> let name' fmt = - if a = [] then pname fmt false + if filter_printing_attributes a = [] then pname fmt false else if nameOpt = None then printAttributes fmt a else fprintf fmt "(%a%a)" printAttributes a pname true in diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c index 483dbf2f421fe71d14ed5a5f7d81ad1ce620b7d0..62c4f08984c381d861bfa926cb998781ff613ca4 100644 --- a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c +++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c @@ -9,11 +9,11 @@ #include "time.h" extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict; -int ( __gen_e_acsl_empty_block_here)(void *s); +int __gen_e_acsl_empty_block_here(void *s); -int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n); +int __gen_e_acsl_valid_or_empty_here(void *s, unsigned long n); -int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n); +int __gen_e_acsl_valid_read_or_empty_here(void *s, unsigned long n); /*@ requires valid_dest: valid_or_empty(dest, n); requires valid_src: valid_read_or_empty(src, n); @@ -779,7 +779,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src, } } -int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n) +int __gen_e_acsl_valid_or_empty_here(void *s, unsigned long n) { int __gen_e_acsl_empty_block_here_2; int __gen_e_acsl_or; @@ -836,7 +836,7 @@ int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n) return __gen_e_acsl_and_2; } -int ( __gen_e_acsl_empty_block_here)(void *s) +int __gen_e_acsl_empty_block_here(void *s) { unsigned long __gen_e_acsl_block_length; int __gen_e_acsl_and; @@ -850,7 +850,7 @@ int ( __gen_e_acsl_empty_block_here)(void *s) return __gen_e_acsl_and; } -int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n) +int __gen_e_acsl_valid_read_or_empty_here(void *s, unsigned long n) { int __gen_e_acsl_empty_block_here_3; int __gen_e_acsl_or; diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c index efad32ac68e962ae59e21a54dedcd551f37959b1..2ee59ac21428c963a95e43ed214b48f2ec3dd711 100644 --- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c +++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c @@ -10,11 +10,11 @@ #include "time.h" extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict; -int ( __gen_e_acsl_empty_block_here)(void *s); +int __gen_e_acsl_empty_block_here(void *s); -int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n); +int __gen_e_acsl_valid_or_empty_here(void *s, unsigned long n); -int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n); +int __gen_e_acsl_valid_read_or_empty_here(void *s, unsigned long n); /*@ requires valid_dest: valid_or_empty(dest, n); requires valid_src: valid_read_or_empty(src, n); @@ -1041,7 +1041,7 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src, } } -int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n) +int __gen_e_acsl_valid_or_empty_here(void *s, unsigned long n) { int __gen_e_acsl_empty_block_here_2; int __gen_e_acsl_or; @@ -1098,7 +1098,7 @@ int ( __gen_e_acsl_valid_or_empty_here)(void *s, unsigned long n) return __gen_e_acsl_and_2; } -int ( __gen_e_acsl_empty_block_here)(void *s) +int __gen_e_acsl_empty_block_here(void *s) { unsigned long __gen_e_acsl_block_length; int __gen_e_acsl_and; @@ -1112,7 +1112,7 @@ int ( __gen_e_acsl_empty_block_here)(void *s) return __gen_e_acsl_and; } -int ( __gen_e_acsl_valid_read_or_empty_here)(void *s, unsigned long n) +int __gen_e_acsl_valid_read_or_empty_here(void *s, unsigned long n) { int __gen_e_acsl_empty_block_here_3; int __gen_e_acsl_or;