From 00c0d5684391c40a689479d99e364c306c058051 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 10 Sep 2024 15:11:45 +0200
Subject: [PATCH] [e-acsl] fix printing of superfluous parentheses for function
declarations
When attributes were present but not printed, unnecessary parentheses
were still placed. This applies the same solution for array declarations
to function declarations.
---
src/kernel_services/ast_printing/cil_printer.ml | 8 +++-----
src/plugins/e-acsl/tests/libc/oracle/gen_mem.c | 12 ++++++------
.../e-acsl/tests/temporal/oracle/gen_t_memcpy.c | 12 ++++++------
3 files changed, 15 insertions(+), 17 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 75c2da8a093..1f1ea2fcb0c 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 483dbf2f421..62c4f08984c 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 efad32ac68e..2ee59ac2142 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;
--
GitLab