Commit d3c12b60 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[kernel] deprecate Pretty_utils.sfprintf

parent 9446a863
......@@ -277,7 +277,7 @@ module Logic_binding = struct
| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
| Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
let msg =
Pretty_utils.sfprintf
Format.asprintf
"logic variable of type %a" Logic_type.pretty lty
in
Error.not_yet msg
......
......@@ -54,7 +54,7 @@ let unmemoized_extend_ast () =
let share = Options.Share.dir ~error:true () in
Options.feedback ~level:3 "setting kernel options for E-ACSL.";
Kernel.CppExtraArgs.add
(Pretty_utils.sfprintf " -DE_ACSL_MACHDEP=%s -I%s/memory_model"
(Format.asprintf " -DE_ACSL_MACHDEP=%s -I%s/memory_model"
(Kernel.Machdep.get ())
share);
Kernel.Keep_unused_specified_functions.off ();
......@@ -64,7 +64,7 @@ let unmemoized_extend_ast () =
(File.NeedCPP
(s,
ppc
^ Pretty_utils.sfprintf " -I%s" share,
^ Format.asprintf " -I%s" share,
ppk))
in
List.iter register (Misc.library_files ())
......@@ -89,7 +89,7 @@ E-ACSL is going to work on a copy.";
Project.create_by_copy
~last:false
~selection
(Pretty_utils.sfprintf "%s for E-ACSL" name)
(Format.asprintf "%s for E-ACSL" name)
in
Project.on prj
(fun () ->
......
......@@ -146,7 +146,7 @@ let mk_e_acsl_guard ?(reverse=false) kind kf e p =
let loc = p.loc in
let msg =
Kernel.Unicode.without_unicode
(Pretty_utils.sfprintf "%a@?" Printer.pp_predicate_named) p
(Format.asprintf "%a@?" Printer.pp_predicate_named) p
in
let line = (fst loc).Lexing.pos_lnum in
let e =
......@@ -267,4 +267,4 @@ let term_addr_of ~loc tlv ty =
Local Variables:
compile-command: "make"
End:
*)
\ No newline at end of file
*)
......@@ -34,9 +34,9 @@ let term_to_exp_ref
let compute_quantif_guards quantif bounded_vars hyps =
let error msg pp x =
let msg1 = Pretty_utils.sfprintf msg pp x in
let msg1 = Format.asprintf msg pp x in
let msg2 =
Pretty_utils.sfprintf "@[ in quantification@ %a@]"
Format.asprintf "@[ in quantification@ %a@]"
Printer.pp_predicate_named quantif
in
Error.untypable (msg1 ^ msg2)
......@@ -93,7 +93,7 @@ let compute_quantif_guards quantif bounded_vars hyps =
| [] -> ()
| _ :: _ ->
let msg =
Pretty_utils.sfprintf
Format.asprintf
"@[unguarded variable%s %tin quantification@ %a@]"
(if List.length vars = 1 then "" else "s")
(fun fmt ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment