From f03897712ead78026b3d91a4e42d3b6a1ba1dbb7 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@inria.fr>
Date: Wed, 13 Feb 2019 17:16:27 +0100
Subject: [PATCH] [Kernel - Printer] Ensures that ghost function pointers are
correctly printed
---
src/kernel_services/ast_printing/cil_printer.ml | 8 ++++++--
tests/syntax/ghost_func_ptr.i | 5 +++++
tests/syntax/oracle/ghost_func_ptr.res.oracle | 12 ++++++++++++
3 files changed, 23 insertions(+), 2 deletions(-)
create mode 100644 tests/syntax/ghost_func_ptr.i
create mode 100644 tests/syntax/oracle/ghost_func_ptr.res.oracle
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6762429ff05..1398a5f1ebb 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1906,11 +1906,15 @@ class cil_printer () = object (self)
else if nameOpt = None then printAttributes fmt a
else fprintf fmt "(%a%a)" printAttributes a pname (a <> [])
in
- let partition_ghosts is_ghost args =
+ let partition_ghosts ghost_arg args =
match args with
| None -> None, []
| Some l ->
- let ghost_args, args = List.partition is_ghost l in
+ let ghost_args, args = if is_ghost then
+ [], l
+ else
+ List.partition ghost_arg l
+ in
Some args, ghost_args
in
let pp_params fmt (args, ghost_args) pp_args =
diff --git a/tests/syntax/ghost_func_ptr.i b/tests/syntax/ghost_func_ptr.i
new file mode 100644
index 00000000000..ba5ce7a1911
--- /dev/null
+++ b/tests/syntax/ghost_func_ptr.i
@@ -0,0 +1,5 @@
+//@ ghost void (*g)(int *) = 0 ;
+
+int main(){
+ //@ ghost void (*l)(int *) = 0 ;
+}
diff --git a/tests/syntax/oracle/ghost_func_ptr.res.oracle b/tests/syntax/oracle/ghost_func_ptr.res.oracle
new file mode 100644
index 00000000000..9c2890ad3dc
--- /dev/null
+++ b/tests/syntax/oracle/ghost_func_ptr.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/ghost_func_ptr.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ ghost void (*g)(int *) = (void (*)(int *))0; */
+int main(void)
+{
+ int __retres;
+ /*@ ghost void (*l)(int *) = (void (*)(int *))0; */
+ __retres = 0;
+ return __retres;
+}
+
+
--
GitLab