diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml index 6b4654ce490cff697f72c500edecaffb63e99a9c..ceeac595c5bb77471bce0a0a364d172a3d6a4f3b 100644 --- a/src/plugins/e-acsl/src/libraries/functions.ml +++ b/src/plugins/e-acsl/src/libraries/functions.ml @@ -181,7 +181,7 @@ module Libc = struct | FLongDouble -> "E" (* [long double] *) in (* get a character representing a pointer type *) - let get_pkind_str ty = match ty with + let get_pkind_str a ty = match ty with | TInt(IChar,_) | TInt(ISChar,_) -> "s" (* [char*] *) | TInt(IUChar,_) -> "S" (* [unsigned char*] *) | TInt(IShort,_) -> "q" (* [short*] *) @@ -194,8 +194,9 @@ module Libc = struct | TInt(IULongLong,_) -> "W" (* [unsigned long int*] *) | TVoid _ -> "p" (* [void*] *) | _ -> - Options.fatal "Unexpected argument type in printf: %a @." + Options.fatal "unexpected argument type in printf: type %a of arg %a@." Printer.pp_typ ty + Printer.pp_exp a in let exps = drop (printf_fmt_position fn) args in let param_str = @@ -203,7 +204,7 @@ module Libc = struct (fun exp acc -> match Cil.unrollType (Cil.typeOf exp) with | TInt(k, _) -> get_ikind_str k ^ acc | TFloat(k, _) -> get_fkind_str k ^ acc - | TPtr(ty, _) -> get_pkind_str (Cil.unrollType ty) ^ acc + | TPtr(ty, _) -> get_pkind_str exp (Cil.unrollType ty) ^ acc | TVoid _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _ | TBuiltin_va_list _ -> assert false) exps @@ -244,3 +245,9 @@ let instrument kf = Options.Instrument.mem gen_kf with Not_found -> false)) + +(* +Local Variables: +compile-command: "make -C ../../../../.." +End: +*)