diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 5627363cb3a88ca1dbaa65998d569e268284b5fc..b1ea0c1640fa3ec537660808822c606eaa405184 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -281,6 +281,7 @@ let () = Cil_datatype.Term_lval.pretty_ref := pp_term_lval
 let () = Cil_datatype.Term_offset.pretty_ref := pp_term_offset
 let () = Cil_datatype.Code_annotation.pretty_ref := pp_code_annotation
 let () = Cil_datatype.Funspec.pretty_ref := pp_funspec
+let () = Cil_datatype.Funbehavior.pretty_ref := pp_behavior
 
 let () = Cil_datatype.Label.pretty_ref := pp_label
 let () = Cil_datatype.Compinfo.pretty_ref := pp_compinfo
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index b345e242afcf676bb54f4239a93c739a5b74152a..003b99cce16b41df6e8882febaad8c7c182092a4 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2304,23 +2304,26 @@ module Identified_predicate = struct
       end)
 end
 
-module Funbehavior =
-  Datatype.Make
-    (struct
-      include Datatype.Serializable_undefined
-      type t = funbehavior
-      let name = "Funbehavior"
-      let reprs =
-        [ {  b_name = "default!"; (* Cil.default_behavior_name *)
-             b_requires = Identified_predicate.reprs;
-             b_assumes = Identified_predicate.reprs;
-             b_post_cond =
-               List.map (fun x -> Normal, x) Identified_predicate.reprs;
-             b_assigns = WritesAny;
-             b_allocation = FreeAllocAny;
-             b_extended = []; } ]
-      let mem_project = Datatype.never_any_project
-    end)
+module Funbehavior = struct
+  let pretty_ref = ref (fun _ _ -> assert false)
+  include Datatype.Make
+      (struct
+        include Datatype.Serializable_undefined
+        type t = funbehavior
+        let name = "Funbehavior"
+        let reprs =
+          [ {  b_name = "default!"; (* Cil.default_behavior_name *)
+               b_requires = Identified_predicate.reprs;
+               b_assumes = Identified_predicate.reprs;
+               b_post_cond =
+                 List.map (fun x -> Normal, x) Identified_predicate.reprs;
+               b_assigns = WritesAny;
+               b_allocation = FreeAllocAny;
+               b_extended = []; } ]
+        let pretty fmt x = !pretty_ref fmt x
+        let mem_project = Datatype.never_any_project
+      end)
+end
 
 module Funspec = struct
   let pretty_ref = ref (fun _ _ -> assert false)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index d088edb1cde690465549be0e21c470341b9e135f..3370462e56180d807ee10c44c8fc415b29a801eb 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -253,7 +253,7 @@ module Code_annotation: sig
   val loc: t -> location option
 end
 
-module Funbehavior: S with type t = funbehavior
+module Funbehavior: S_with_pretty with type t = funbehavior
 
 module Funspec: S_with_pretty with type t = funspec