diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 6762429ff05cadbfeae382c06603ecc8c9d7968b..1398a5f1ebb2f6c78cd3a5b8be1c315ba90db029 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 0000000000000000000000000000000000000000..ba5ce7a1911a6eca9b0045ed36ef926977428985 --- /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 0000000000000000000000000000000000000000..9c2890ad3dc66b42245237d94ea410ff875b9ca5 --- /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; +} + +