diff options
| -rw-r--r-- | driver/Interp.ml | 85 | ||||
| -rw-r--r-- | test/regression/Results/sizeof1 | 2 | ||||
| -rw-r--r-- | test/regression/sizeof1.c | 12 |
3 files changed, 58 insertions, 41 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index 99f9f4f..25d363c 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -296,10 +296,13 @@ let extract_string m blk ofs = (* Emulation of printf *) -(* All ISO C 99 formats except size modifier [L] (long double) *) +(* All ISO C 99 formats *) -let re_conversion = Str.regexp - "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\|ll\\)?\\([aAcdeEfgGinopsuxX%]\\)" +let re_conversion = Str.regexp ( + "\\(%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\)" (* group 1: flags, width, precision *) +^ "\\(\\|[lhjztL]\\|hh\\|ll\\)" (* group 3: length modifier *) +^ "\\([aAcdeEfgGinopsuxX%]\\)" (* group 4: conversion specifier *) +) external format_float: string -> float -> string = "caml_format_float" @@ -308,6 +311,36 @@ external format_int32: string -> int32 -> string external format_int64: string -> int64 -> string = "caml_int64_format" +let format_value m flags length conv arg = + match conv.[0], length, arg with + | ('d'|'i'|'u'|'o'|'x'|'X'|'c'), (""|"h"|"hh"|"l"|"z"|"t"), Vint i -> + format_int32 (flags ^ conv) (camlint_of_coqint i) + | ('d'|'i'|'u'|'o'|'x'|'X'|'c'), (""|"h"|"hh"|"l"|"z"|"t"), _ -> + "<int argument expected>" + | ('d'|'i'|'u'|'o'|'x'|'X'), ("ll"|"j"), Vlong i -> + format_int64 (flags ^ conv) (camlint64_of_coqint i) + | ('d'|'i'|'u'|'o'|'x'|'X'), ("ll"|"j"), _ -> + "<long long argument expected" + | ('f'|'e'|'E'|'g'|'G'|'a'), "", Vfloat f -> + format_float (flags ^ conv) (camlfloat_of_coqfloat f) + | ('f'|'e'|'E'|'g'|'G'|'a'), "", _ -> + "<float argument expected" + | 's', "", Vptr(blk, ofs) -> + begin match extract_string m blk ofs with + | Some s -> s + | None -> "<bad string>" + end + | 's', "", _ -> + "<pointer argument expected>" + | 'p', "", Vptr(blk, ofs) -> + Printf.sprintf "<%ld%+ld>" (P.to_int32 blk) (camlint_of_coqint ofs) + | 'p', "", Vint i -> + format_int32 (flags ^ "x") (camlint_of_coqint i) + | 'p', "", _ -> + "<int or pointer argument expected>" + | _, _, _ -> + "<unrecognized format>" + let do_printf m fmt args = let b = Buffer.create 80 in @@ -324,38 +357,22 @@ let do_printf m fmt args = Buffer.add_substring b fmt pos (len - pos) | Some pos1 -> Buffer.add_substring b fmt pos (pos1 - pos); - let pat = Str.matched_string fmt - and conv = Str.matched_group 3 fmt + let flags = Str.matched_group 1 fmt + and length = Str.matched_group 3 fmt + and conv = Str.matched_group 4 fmt and pos' = Str.match_end() in - match args, conv.[0] with - | _, '%' -> - Buffer.add_char b '%'; - scan pos' args - | [], _ -> - Buffer.add_string b "<missing argument>"; - scan pos' [] - | Vint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') -> - Buffer.add_string b (format_int32 pat (camlint_of_coqint i)); - scan pos' args' - | Vfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') -> - Buffer.add_string b (format_float pat (camlfloat_of_coqfloat f)); - scan pos' args' - | Vlong i :: args', ('d'|'i'|'u'|'o'|'x'|'X') -> - let pat = Str.replace_first (Str.regexp "ll") "" pat in - Buffer.add_string b (format_int64 pat (camlint64_of_coqint i)); - scan pos' args' - | Vptr(blk, ofs) :: args', 's' -> - Buffer.add_string b - (match extract_string m blk ofs with - | Some s -> s - | None -> "<bad string>"); - scan pos' args' - | Vptr(blk, ofs) :: args', 'p' -> - Printf.bprintf b "<%ld%+ld>" (P.to_int32 blk) (camlint_of_coqint ofs); - scan pos' args' - | _ :: args', _ -> - Buffer.add_string b "<formatting error>"; - scan pos' args' + if conv = "%" then begin + Buffer.add_char b '%'; + scan pos' args + end else begin + match args with + | [] -> + Buffer.add_string b "<missing argument>"; + scan pos' [] + | arg :: args' -> + Buffer.add_string b (format_value m flags length conv arg); + scan pos' args' + end end in scan 0 args; Buffer.contents b diff --git a/test/regression/Results/sizeof1 b/test/regression/Results/sizeof1 index 674f6da..a952be5 100644 --- a/test/regression/Results/sizeof1 +++ b/test/regression/Results/sizeof1 @@ -1,3 +1,3 @@ -sizeof(struct s) = 32, sizeof(tbl) = 32 +sizeof(struct s) = 20, sizeof(tbl) = 20 sizeof(struct bits1) = 1, sizeof(b1) = 1 sizeof(struct bits2) = 8, sizeof(b2) = 8 diff --git a/test/regression/sizeof1.c b/test/regression/sizeof1.c index d7d37d3..139b1bc 100644 --- a/test/regression/sizeof1.c +++ b/test/regression/sizeof1.c @@ -2,18 +2,18 @@ struct s { char c; - union { int i[3]; double d; } n; + union { short i[3]; int d; } n; struct { struct s * hd; struct s * tl; } l; }; char tbl[sizeof(struct s)]; /* Should be 32: char c at 0 - union n at 8 because alignment = 8; sizeof = 12 - struct l at 8+12=20 with alignment = 4; sizeof = 8 - end of struct at 20+8=28 - alignment of whole struct is 8 because of d - 28 aligned to 8 -> 32 + union n at 4 because alignment = 4; sizeof = 8 + struct l at 4+8=12 with alignment = 4; sizeof = 8 + end of struct at 12+8=20 + alignment of whole struct is 4 + 20 aligned to 4 -> 20 */ struct bits1 { |