diff options
| -rw-r--r-- | exportclight/ExportClight.ml | 67 | ||||
| -rw-r--r-- | test/clightgen/annotations.c | 6 |
2 files changed, 14 insertions, 59 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 96947545..321ed8c9 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -253,8 +253,6 @@ let signatur p sg = astrettype sg.sig_res callconv sg.sig_cc -let assertions = ref ([]: (string * typ list) list) - let external_function p = function | EF_external(name, sg) -> fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg @@ -270,14 +268,15 @@ let external_function p = function | EF_free -> fprintf p "EF_free" | EF_memcpy(sz, al) -> fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al) - | EF_annot(kind,text, targs) -> - assertions := (camlstring_of_coqstring text, targs) :: !assertions; - fprintf p "(EF_annot %a %a)" coqstring text (print_list asttype) targs - | EF_annot_val(kind,text, targ) -> - assertions := (camlstring_of_coqstring text, [targ]) :: !assertions; - fprintf p "(EF_annot_val %a %a)" coqstring text asttype targ + | EF_annot(kind, text, targs) -> + fprintf p "(EF_annot %ld%%positive %a %a)" + (P.to_int32 kind) coqstring text (print_list asttype) targs + | EF_annot_val(kind, text, targ) -> + fprintf p "(EF_annot_val %ld%%positive %a %a)" + (P.to_int32 kind) coqstring text asttype targ | EF_debug(kind, text, targs) -> - fprintf p "(EF_debug %ld%%positive %ld%%positive %a)" (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs + fprintf p "(EF_debug %ld%%positive %ld%%positive %a)" + (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs | EF_inline_asm(text, sg, clob) -> fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]" coqstring text @@ -447,55 +446,6 @@ let print_composite_definition p (Composite(id, su, m, a)) = (print_list (print_pair ident typ)) m attribute a -(* Assertion processing *) - -let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" - -type fragment = Text of string | Param of int - -(* For compatibility with OCaml < 4.00 *) -let list_iteri f l = - let rec iteri i = function - | [] -> () - | a::l -> f i a; iteri (i + 1) l - in iteri 0 l - -let print_assertion p (txt, targs) = - let frags = - List.map - (function - | Str.Text s -> Text s - | Str.Delim "%%" -> Text "%" - | Str.Delim s -> Param(int_of_string(String.sub s 1 (String.length s - 1)))) - (Str.full_split re_annot_param txt) in - let max_param = ref 0 in - List.iter - (function - | Text _ -> () - | Param n -> max_param := max n !max_param) - frags; - fprintf p " | \"%s\", " txt; - list_iteri - (fun i targ -> fprintf p "_x%d :: " (i + 1)) - targs; - fprintf p "nil =>@ "; - fprintf p " "; - List.iter - (function - | Text s -> fprintf p "%s" s - | Param n -> fprintf p "_x%d" n) - frags; - fprintf p "@ " - -let print_assertions p = - if !assertions <> [] then begin - fprintf p "Definition assertions (txt: string) args : Prop :=@ "; - fprintf p " match txt, args with@ "; - List.iter (print_assertion p) !assertions; - fprintf p " | _, _ => False@ "; - fprintf p " end.@ @ " - end - (* The prologue *) let prologue = "\ @@ -595,5 +545,4 @@ let print_program p prog sourcefile normalized = fprintf p "Definition prog : Clight.program := @ "; fprintf p " mkprogram composites global_definitions public_idents %a Logic.I.@ @ " ident prog.Ctypes.prog_main; - print_assertions p; fprintf p "@]@." diff --git a/test/clightgen/annotations.c b/test/clightgen/annotations.c new file mode 100644 index 00000000..56fc1700 --- /dev/null +++ b/test/clightgen/annotations.c @@ -0,0 +1,6 @@ +int f(int x, long y) +{ + __builtin_ais_annot("x is %e1, y is %e2", x, y); + __builtin_annot("x is %1, y is %2", x, y); + return __builtin_annot_intval("x was here: %1", x); +} |