From 04501138e91fe6a901a0f8edce8c2900115afc05 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 5 Feb 2019 16:29:57 +0100
Subject: [PATCH] [lint] ast-printing
---
.Makefile.lint | 15 -
.../ast_printing/cabs_debug.ml | 424 ++++-----
.../ast_printing/cil_descriptive_printer.ml | 30 +-
.../ast_printing/cil_printer.ml | 894 +++++++++---------
.../ast_printing/cil_printer.mli | 8 +-
.../ast_printing/cil_types_debug.ml | 194 ++--
.../ast_printing/cil_types_debug.mli | 1 -
src/kernel_services/ast_printing/cprint.ml | 602 ++++++------
src/kernel_services/ast_printing/cprint.mli | 2 +-
.../ast_printing/description.ml | 272 +++---
.../ast_printing/description.mli | 4 +-
.../ast_printing/logic_print.ml | 656 ++++++-------
src/kernel_services/ast_printing/printer.ml | 102 +-
.../ast_printing/printer_api.mli | 112 +--
.../ast_printing/printer_builder.ml | 2 +-
.../ast_printing/printer_builder.mli | 6 +-
16 files changed, 1654 insertions(+), 1670 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index 88cc7104680..ea7f70ed4fe 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -93,21 +93,6 @@ ML_LINT_KO+=src/kernel_services/ast_data/property.mli
ML_LINT_KO+=src/kernel_services/ast_data/property_status.ml
ML_LINT_KO+=src/kernel_services/ast_data/property_status.mli
ML_LINT_KO+=src/kernel_services/ast_data/statuses_by_call.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cabs_debug.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_descriptive_printer.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_printer.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_printer.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_types_debug.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_types_debug.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/cprint.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cprint.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/description.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/description.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/logic_print.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/printer.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/printer_api.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/printer_builder.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/printer_builder.mli
ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.ml
ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil.ml
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index 25dca2c6207..fc191d85824 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -28,80 +28,80 @@ let pp_cabsloc fmt (pos1 , _pos2) =
fprintf fmt "%d,%s" pos1.Filepath.pos_lnum (pos1.Filepath.pos_path :> string)
let pp_storage fmt = function
- | NO_STORAGE -> fprintf fmt "NO_STORAGE"
- | AUTO -> fprintf fmt "AUTO"
- | STATIC -> fprintf fmt "STATIC"
- | EXTERN -> fprintf fmt "EXTERN"
- | REGISTER -> fprintf fmt "REGISTER"
+ | NO_STORAGE -> fprintf fmt "NO_STORAGE"
+ | AUTO -> fprintf fmt "AUTO"
+ | STATIC -> fprintf fmt "STATIC"
+ | EXTERN -> fprintf fmt "EXTERN"
+ | REGISTER -> fprintf fmt "REGISTER"
let pp_fun_spec fmt = function
- | INLINE -> fprintf fmt "INLINE"
- | VIRTUAL -> fprintf fmt "VIRTUAL"
- | EXPLICIT -> fprintf fmt "EXPLICIT"
+ | INLINE -> fprintf fmt "INLINE"
+ | VIRTUAL -> fprintf fmt "VIRTUAL"
+ | EXPLICIT -> fprintf fmt "EXPLICIT"
let pp_cvspec fmt = function
- | CV_CONST -> fprintf fmt "CV_CONST"
- | CV_VOLATILE -> fprintf fmt "CV_VOLATILE"
- | CV_RESTRICT -> fprintf fmt "CV_RESTRICT"
- | CV_ATTRIBUTE_ANNOT s -> fprintf fmt "CV_ATTRIBUTE_ANNOT %s" s
+ | CV_CONST -> fprintf fmt "CV_CONST"
+ | CV_VOLATILE -> fprintf fmt "CV_VOLATILE"
+ | CV_RESTRICT -> fprintf fmt "CV_RESTRICT"
+ | CV_ATTRIBUTE_ANNOT s -> fprintf fmt "CV_ATTRIBUTE_ANNOT %s" s
let pp_const fmt = function
- | CONST_INT s -> fprintf fmt "CONST_INT %s" s
- | CONST_FLOAT s -> fprintf fmt "CONST_FLOAT %s" s
- | CONST_CHAR l ->
+ | CONST_INT s -> fprintf fmt "CONST_INT %s" s
+ | CONST_FLOAT s -> fprintf fmt "CONST_FLOAT %s" s
+ | CONST_CHAR l ->
fprintf fmt "CONST_CHAR{";
List.iter (fun i -> fprintf fmt ",@ %s" (Int64.to_string i)) l;
fprintf fmt "}"
- | CONST_WCHAR l ->
+ | CONST_WCHAR l ->
fprintf fmt "CONST_WCHAR{";
List.iter (fun i -> fprintf fmt ",@ %s" (Int64.to_string i)) l;
fprintf fmt "}"
- | CONST_STRING s -> fprintf fmt "CONST_STRING %s" s
- | CONST_WSTRING l ->
+ | CONST_STRING s -> fprintf fmt "CONST_STRING %s" s
+ | CONST_WSTRING l ->
fprintf fmt "CONST_WSTRING{";
List.iter (fun i -> fprintf fmt ",@ %s" (Int64.to_string i)) l;
fprintf fmt "}"
let pp_labels fmt lbls =
fprintf fmt "%s" (String.concat " " lbls)
-
-
+
+
let rec pp_typeSpecifier fmt = function
| Tvoid -> fprintf fmt "Tvoid"
- | Tchar -> fprintf fmt "Tchar"
- | Tbool -> fprintf fmt "Tbool"
- | Tshort -> fprintf fmt "Tshort"
- | Tint -> fprintf fmt "Tint"
- | Tlong -> fprintf fmt "Tlong"
- | Tint64 -> fprintf fmt "Tint64"
- | Tfloat -> fprintf fmt "Tfloat"
- | Tdouble -> fprintf fmt "Tdouble"
- | Tsigned -> fprintf fmt "Tsigned"
- | Tunsigned -> fprintf fmt "Tunsigned"
- | Tnamed s -> fprintf fmt "%s" s
- | Tstruct (sname, None, alist) -> fprintf fmt "struct@ %s {} %a" sname pp_attrs alist
- | Tstruct (sname, Some fd_gp_list, alist) ->
+ | Tchar -> fprintf fmt "Tchar"
+ | Tbool -> fprintf fmt "Tbool"
+ | Tshort -> fprintf fmt "Tshort"
+ | Tint -> fprintf fmt "Tint"
+ | Tlong -> fprintf fmt "Tlong"
+ | Tint64 -> fprintf fmt "Tint64"
+ | Tfloat -> fprintf fmt "Tfloat"
+ | Tdouble -> fprintf fmt "Tdouble"
+ | Tsigned -> fprintf fmt "Tsigned"
+ | Tunsigned -> fprintf fmt "Tunsigned"
+ | Tnamed s -> fprintf fmt "%s" s
+ | Tstruct (sname, None, alist) -> fprintf fmt "struct@ %s {} %a" sname pp_attrs alist
+ | Tstruct (sname, Some fd_gp_list, alist) ->
fprintf fmt "struct@ %s {%a}@ attrs=(%a)" sname pp_field_groups fd_gp_list pp_attrs alist
- | Tunion (uname, None, alist) -> fprintf fmt "union@ %s {} %a" uname pp_attrs alist
+ | Tunion (uname, None, alist) -> fprintf fmt "union@ %s {} %a" uname pp_attrs alist
| Tunion (uname, Some fd_gp_list, alist) ->
fprintf fmt "union@ %s {%a}@ attrs=(%a)" uname pp_field_groups fd_gp_list pp_attrs alist
- | Tenum (ename, None, alist) -> fprintf fmt "enum@ %s {} %a" ename pp_attrs alist
- | Tenum (ename, Some e_item_list, alist) ->
+ | Tenum (ename, None, alist) -> fprintf fmt "enum@ %s {} %a" ename pp_attrs alist
+ | Tenum (ename, Some e_item_list, alist) ->
fprintf fmt "enum@ %s {" ename;
List.iter (fun e -> fprintf fmt ",@ %a" pp_enum_item e) e_item_list;
fprintf fmt "}@ %a" pp_attrs alist;
- | TtypeofE exp -> fprintf fmt "typeOfE %a" pp_exp exp
- | TtypeofT (spec, d_type) -> fprintf fmt "typeOfT(%a,%a)" pp_spec spec pp_decl_type d_type
+ | TtypeofE exp -> fprintf fmt "typeOfE %a" pp_exp exp
+ | TtypeofT (spec, d_type) -> fprintf fmt "typeOfT(%a,%a)" pp_spec spec pp_decl_type d_type
and pp_spec_elem fmt = function
- | SpecTypedef -> fprintf fmt "SpecTypedef"
- | SpecCV cvspec -> fprintf fmt "SpecCV %a" pp_cvspec cvspec
- | SpecAttr attr -> fprintf fmt "SpecAttr %a" pp_attr attr
- | SpecStorage storage -> fprintf fmt "SpecStorage %a" pp_storage storage
- | SpecInline -> fprintf fmt "SpecInline"
- | SpecType typeSpec -> fprintf fmt "SpecType %a" pp_typeSpecifier typeSpec
- | SpecPattern s -> fprintf fmt "SpecPattern %s" s
+ | SpecTypedef -> fprintf fmt "SpecTypedef"
+ | SpecCV cvspec -> fprintf fmt "SpecCV %a" pp_cvspec cvspec
+ | SpecAttr attr -> fprintf fmt "SpecAttr %a" pp_attr attr
+ | SpecStorage storage -> fprintf fmt "SpecStorage %a" pp_storage storage
+ | SpecInline -> fprintf fmt "SpecInline"
+ | SpecType typeSpec -> fprintf fmt "SpecType %a" pp_typeSpecifier typeSpec
+ | SpecPattern s -> fprintf fmt "SpecPattern %s" s
and pp_spec fmt spec_elems =
fprintf fmt "@[<hv 2>{" ;
@@ -111,17 +111,17 @@ and pp_spec fmt spec_elems =
fprintf fmt "} @]"
and pp_decl_type fmt = function
- | JUSTBASE -> fprintf fmt "@[<hov 2>JUSTBASE@]"
- | PARENTYPE (attrs1, decl_type, attrs2)
- -> fprintf fmt "@[<hov 2>PARENTYPE(%a, %a, %a)@]" pp_attrs attrs1 pp_decl_type decl_type pp_attrs attrs2
- | ARRAY (decl_type, attrs, exp)
- -> fprintf fmt "@[<hov 2>ARRAY[%a, %a, %a]@]" pp_decl_type decl_type pp_attrs attrs pp_exp exp
- | PTR (attrs, decl_type) -> fprintf fmt "@[<hov 2>PTR(%a, %a)@]" pp_attrs attrs pp_decl_type decl_type
- | PROTO (decl_type, single_names, b)
+ | JUSTBASE -> fprintf fmt "@[<hov 2>JUSTBASE@]"
+ | PARENTYPE (attrs1, decl_type, attrs2)
+ -> fprintf fmt "@[<hov 2>PARENTYPE(%a, %a, %a)@]" pp_attrs attrs1 pp_decl_type decl_type pp_attrs attrs2
+ | ARRAY (decl_type, attrs, exp)
+ -> fprintf fmt "@[<hov 2>ARRAY[%a, %a, %a]@]" pp_decl_type decl_type pp_attrs attrs pp_exp exp
+ | PTR (attrs, decl_type) -> fprintf fmt "@[<hov 2>PTR(%a, %a)@]" pp_attrs attrs pp_decl_type decl_type
+ | PROTO (decl_type, single_names, b)
-> fprintf fmt "@[<hov 2>PROTO decl_type(%a), single_names(" pp_decl_type decl_type;
- List.iter (fun sn -> fprintf fmt ",@ %a" pp_single_name sn) single_names;
- fprintf fmt "),@ %b@]" b
-
+ List.iter (fun sn -> fprintf fmt ",@ %a" pp_single_name sn) single_names;
+ fprintf fmt "),@ %b@]" b
+
and pp_name_group fmt (spec, names) =
fprintf fmt "@[<hov 2>name_group@ spec(%a), names{" pp_spec spec;
List.iter
@@ -135,7 +135,7 @@ and pp_field_group fmt = function
fprintf fmt "@[<hov 2>FIELD spec(%a), {" pp_spec spec;
List.iter
(fun (n,e_opt) -> fprintf fmt "@ %a" pp_name n;
- match e_opt with Some exp -> fprintf fmt "@ %a" pp_exp exp | _ -> ())
+ match e_opt with Some exp -> fprintf fmt "@ %a" pp_exp exp | _ -> ())
l;
fprintf fmt "}@]"
| TYPE_ANNOT _ -> fprintf fmt "TYPE_ANNOT"
@@ -151,43 +151,43 @@ and pp_init_name_group fmt (spec,init_names) =
( fun i -> fprintf fmt "@ %a" pp_init_name i)
init_names;
fprintf fmt "}@]"
-
+
and pp_name fmt (s,decl_type,attrs,loc) =
fprintf fmt "name %s, decl_type(%a), attrs(%a), loc(%a)"
s pp_decl_type decl_type pp_attrs attrs pp_cabsloc loc
-
+
and pp_init_name fmt (name,init_exp) =
fprintf fmt "init_name name(%a), init_exp(%a)" pp_name name pp_init_exp init_exp
-
+
and pp_single_name fmt (spec,name) =
fprintf fmt "@[<hov 2>single_name{spec(%a), name(%a)}@]" pp_spec spec pp_name name
-
+
and pp_enum_item fmt (s,exp,loc) =
fprintf fmt "@[<hov 2>enum_item %s, exp(%a, loc(%a))@]" s pp_exp exp pp_cabsloc loc
(* Warning : printing for GLOBANNOT and CUSTOM is not complete *)
and pp_def fmt = function
- | FUNDEF (_, single_name, bl, loc1, loc2) ->
+ | FUNDEF (_, single_name, bl, loc1, loc2) ->
fprintf fmt "@[<hov 2>FUNDEF (%a), loc1(%a), loc2(%a) {%a} @]"
pp_single_name single_name pp_cabsloc loc1 pp_cabsloc loc2 pp_block bl
- | DECDEF (_, init_name_group, loc) ->
+ | DECDEF (_, init_name_group, loc) ->
fprintf fmt "@[<hov 2>DECDEF (%a, loc(%a))@]" pp_init_name_group init_name_group pp_cabsloc loc
- | TYPEDEF (name_group, loc) -> (* typedef normal *)
- fprintf fmt "@[<hov 2>TYPEDEF (%a), loc(%a)@]" pp_name_group name_group pp_cabsloc loc
- | ONLYTYPEDEF (spec, loc) -> (* ex : struct s{...}; *)
- fprintf fmt "@[<hov 2>ONLYTYPEDEF (%a), loc(%a)@]" pp_spec spec pp_cabsloc loc
- | GLOBASM (s, loc) ->
- fprintf fmt "@[<hov 2>GLOBASM %s, loc(%a)@]" s pp_cabsloc loc
- | PRAGMA (exp, loc) ->
+ | TYPEDEF (name_group, loc) -> (* typedef normal *)
+ fprintf fmt "@[<hov 2>TYPEDEF (%a), loc(%a)@]" pp_name_group name_group pp_cabsloc loc
+ | ONLYTYPEDEF (spec, loc) -> (* ex : struct s{...}; *)
+ fprintf fmt "@[<hov 2>ONLYTYPEDEF (%a), loc(%a)@]" pp_spec spec pp_cabsloc loc
+ | GLOBASM (s, loc) ->
+ fprintf fmt "@[<hov 2>GLOBASM %s, loc(%a)@]" s pp_cabsloc loc
+ | PRAGMA (exp, loc) ->
fprintf fmt "@[<hov 2>PRAGMA exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
- | LINKAGE (s, loc, defs) ->
+ | LINKAGE (s, loc, defs) ->
fprintf fmt "@[<hov 2>LINKAGE %s, loc(%a), defs(" s pp_cabsloc loc;
List.iter (fun def -> fprintf fmt ",@ def(%a)" pp_def def) defs;
fprintf fmt ")@]"
- | GLOBANNOT _ -> fprintf fmt "GLOBANNOT"
- | CUSTOM _ -> fprintf fmt "CUSTOM"
-
+ | GLOBANNOT _ -> fprintf fmt "GLOBANNOT"
+ | CUSTOM _ -> fprintf fmt "CUSTOM"
+
and pp_file fmt (s,l) =
fprintf fmt "@[FILE %a, {" Filepath.Normalized.pp_abs s;
List.iter
@@ -196,7 +196,7 @@ and pp_file fmt (s,l) =
fprintf fmt "@] }"
and pp_block fmt bl =
- fprintf fmt "@[<hv 2>labels(%a), attrs(%a), {" pp_labels bl.blabels pp_attrs bl.battrs;
+ fprintf fmt "@[<hv 2>labels(%a), attrs(%a), {" pp_labels bl.blabels pp_attrs bl.battrs;
List.iter
(fun s -> fprintf fmt "@ %a" pp_stmt s)
bl.bstmts ;
@@ -204,48 +204,48 @@ and pp_block fmt bl =
(* Warning : printing for ASM, CODE_ANNOT and CODE_SPEC is not complete *)
and pp_raw_stmt fmt = function
- | NOP loc -> fprintf fmt "@[<hov 2>NOP loc(%a)@]" pp_cabsloc loc
- | COMPUTATION (exp, loc) ->
- fprintf fmt "@[<hov 2>COMPUTATION exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
- | BLOCK (bl, loc1, loc2) ->
- fprintf fmt "@[<hov 2>BLOCK loc1(%a), loc2(%a) {%a} @]"
- pp_cabsloc loc1 pp_cabsloc loc2 pp_block bl
- | SEQUENCE (stmt1, stmt2, loc) ->
+ | NOP loc -> fprintf fmt "@[<hov 2>NOP loc(%a)@]" pp_cabsloc loc
+ | COMPUTATION (exp, loc) ->
+ fprintf fmt "@[<hov 2>COMPUTATION exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
+ | BLOCK (bl, loc1, loc2) ->
+ fprintf fmt "@[<hov 2>BLOCK loc1(%a), loc2(%a) {%a} @]"
+ pp_cabsloc loc1 pp_cabsloc loc2 pp_block bl
+ | SEQUENCE (stmt1, stmt2, loc) ->
fprintf fmt "@[<hov 2>SEQUENCE stmt(%a), stmt(%a), loc(%a)@]" pp_stmt stmt1 pp_stmt stmt2 pp_cabsloc loc
- | IF (exp, stmt1, stmt2, loc) ->
+ | IF (exp, stmt1, stmt2, loc) ->
fprintf fmt "@[<hov 2>IF cond(%a), stmt(%a), stmt(%a), loc(%a)@]"
- pp_exp exp pp_stmt stmt1 pp_stmt stmt2 pp_cabsloc loc
- | WHILE (_loop_inv, exp, stmt, loc) -> (* Warning : no printing for loop_invariant *)
- fprintf fmt "@[<hov 2>WHILE cond(%a), stmt(%a), loc(%a)@]"
- pp_exp exp pp_stmt stmt pp_cabsloc loc
- | DOWHILE (_loop_inv, exp, stmt, loc) -> (* Warning : no printing for loop_invariant *)
+ pp_exp exp pp_stmt stmt1 pp_stmt stmt2 pp_cabsloc loc
+ | WHILE (_loop_inv, exp, stmt, loc) -> (* Warning : no printing for loop_invariant *)
+ fprintf fmt "@[<hov 2>WHILE cond(%a), stmt(%a), loc(%a)@]"
+ pp_exp exp pp_stmt stmt pp_cabsloc loc
+ | DOWHILE (_loop_inv, exp, stmt, loc) -> (* Warning : no printing for loop_invariant *)
fprintf fmt "@[<hov 2>DOWHILE cond(%a), stmt(%a), loc(%a)@]"
- pp_exp exp pp_stmt stmt pp_cabsloc loc
- | FOR (_loop_inv, for_clause, exp1, exp2, stmt, loc) -> (* Warning : no printing for loop_invariant *)
+ pp_exp exp pp_stmt stmt pp_cabsloc loc
+ | FOR (_loop_inv, for_clause, exp1, exp2, stmt, loc) -> (* Warning : no printing for loop_invariant *)
fprintf fmt "@[<hov 2>FOR for_clause(%a), exp1(%a), exp2(%a), stmt(%a), loc(%a)@]"
- pp_for_clause for_clause pp_exp exp1 pp_exp exp2 pp_stmt stmt pp_cabsloc loc
- | BREAK loc -> fprintf fmt "@[<hov 2>BREAK loc(%a)@]" pp_cabsloc loc
- | CONTINUE loc -> fprintf fmt "@[<hov 2>CONTINUE loc(%a)@]" pp_cabsloc loc
- | RETURN (exp, loc) -> fprintf fmt "@[<hov 2>RETURN exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
- | SWITCH (exp, stmt, loc) ->
+ pp_for_clause for_clause pp_exp exp1 pp_exp exp2 pp_stmt stmt pp_cabsloc loc
+ | BREAK loc -> fprintf fmt "@[<hov 2>BREAK loc(%a)@]" pp_cabsloc loc
+ | CONTINUE loc -> fprintf fmt "@[<hov 2>CONTINUE loc(%a)@]" pp_cabsloc loc
+ | RETURN (exp, loc) -> fprintf fmt "@[<hov 2>RETURN exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
+ | SWITCH (exp, stmt, loc) ->
fprintf fmt "@[<hov 2>SWITH exp(%a), stmt(%a), loc(%a)@]" pp_exp exp pp_stmt stmt pp_cabsloc loc
- | CASE (exp, stmt, loc) ->
+ | CASE (exp, stmt, loc) ->
fprintf fmt "@[<hov 2>CASE exp(%a), stmt(%a), loc(%a)@]" pp_exp exp pp_stmt stmt pp_cabsloc loc
- | CASERANGE (exp1, exp2, stmt, loc) ->
+ | CASERANGE (exp1, exp2, stmt, loc) ->
fprintf fmt "@[<hov 2>CASE exp(%a), exp(%a), stmt(%a), loc(%a)@]" pp_exp exp1 pp_exp exp2 pp_stmt stmt pp_cabsloc loc
- | DEFAULT (stmt, loc) ->
+ | DEFAULT (stmt, loc) ->
fprintf fmt "@[<hov 2>DEFAULT stmt(%a), loc(%a)@]" pp_stmt stmt pp_cabsloc loc
- | LABEL (s, stmt, loc) ->
+ | LABEL (s, stmt, loc) ->
fprintf fmt "@[<hov 2>LABEL %s stmt(%a), loc(%a)@]" s pp_stmt stmt pp_cabsloc loc
- | GOTO (s, loc) ->
+ | GOTO (s, loc) ->
fprintf fmt "@[<hov 2>GOTO %s, loc(%a)@]" s pp_cabsloc loc
- | COMPGOTO (exp, loc) -> fprintf fmt "@[<hov 2>COMPGOTO exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
- | DEFINITION def -> fprintf fmt "@[<hov 2>DEFINITION %a@]" pp_def def
- | ASM (_,_,_,_) -> fprintf fmt "ASM"
- | TRY_EXCEPT (bl1, exp, bl2, loc) ->
+ | COMPGOTO (exp, loc) -> fprintf fmt "@[<hov 2>COMPGOTO exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
+ | DEFINITION def -> fprintf fmt "@[<hov 2>DEFINITION %a@]" pp_def def
+ | ASM (_,_,_,_) -> fprintf fmt "ASM"
+ | TRY_EXCEPT (bl1, exp, bl2, loc) ->
fprintf fmt "@[<hov 2>TRY_EXCEPT block(%a) exp(%a) block(%a) loc(%a)@]"
pp_block bl1 pp_exp exp pp_block bl2 pp_cabsloc loc
- | TRY_FINALLY (bl1, bl2, loc) ->
+ | TRY_FINALLY (bl1, bl2, loc) ->
fprintf fmt "@[<hov 2>TRY_EXCEPT block(%a) block(%a) loc(%a)@]"
pp_block bl1 pp_block bl2 pp_cabsloc loc
| THROW(e,loc) ->
@@ -261,7 +261,7 @@ and pp_raw_stmt fmt = function
pp_stmt s
pp_cabsloc loc
(Pretty_utils.pp_list ~sep:"@;" print_one_catch) l
- | CODE_ANNOT (_,_) -> fprintf fmt "CODE_ANNOT"
+ | CODE_ANNOT (_,_) -> fprintf fmt "CODE_ANNOT"
| CODE_SPEC _ -> fprintf fmt "CODE_SPEC"
and pp_stmt fmt stmt =
@@ -270,129 +270,129 @@ and pp_stmt fmt stmt =
(*and loop_invariant = Logic_ptree.code_annot list *)
and pp_for_clause fmt = function
- | FC_EXP exp -> fprintf fmt "@[<hov 2>FC_EXP %a@]" pp_exp exp
- | FC_DECL def -> fprintf fmt "@[<hov 2>FC_DECL %a@]" pp_def def
-
+ | FC_EXP exp -> fprintf fmt "@[<hov 2>FC_EXP %a@]" pp_exp exp
+ | FC_DECL def -> fprintf fmt "@[<hov 2>FC_DECL %a@]" pp_def def
+
and pp_bin_op fmt = function
- | ADD -> fprintf fmt "ADD"
- | SUB -> fprintf fmt "SUB"
- | MUL -> fprintf fmt "MUL"
- | DIV -> fprintf fmt "DIV"
- | MOD -> fprintf fmt "MOD"
- | AND -> fprintf fmt "AND"
- | OR -> fprintf fmt "OR"
- | BAND -> fprintf fmt "BAND"
- | BOR -> fprintf fmt "BOR"
- | XOR -> fprintf fmt "XOR"
- | SHL -> fprintf fmt "SHL"
- | SHR -> fprintf fmt "SHR"
- | EQ -> fprintf fmt "EQ"
- | NE -> fprintf fmt "NE"
- | LT -> fprintf fmt "LT"
- | GT -> fprintf fmt "GT"
- | LE -> fprintf fmt "LE"
- | GE -> fprintf fmt "GE"
- | ASSIGN -> fprintf fmt "ASSIGN"
- | ADD_ASSIGN -> fprintf fmt "ADD_ASSIGN"
- | SUB_ASSIGN -> fprintf fmt "SUB_ASSIGN"
- | MUL_ASSIGN -> fprintf fmt "MUL_ASSIGN"
- | DIV_ASSIGN -> fprintf fmt "DIV_ASSIGN"
- | MOD_ASSIGN -> fprintf fmt "MOD_ASSIGN"
- | BAND_ASSIGN -> fprintf fmt "BAND_ASSIGN"
- | BOR_ASSIGN -> fprintf fmt "BOR_ASSIGN"
- | XOR_ASSIGN -> fprintf fmt "XOR_ASSIGN"
- | SHL_ASSIGN -> fprintf fmt "SHL_ASSIGN"
- | SHR_ASSIGN -> fprintf fmt "SHR_ASSIGN"
+ | ADD -> fprintf fmt "ADD"
+ | SUB -> fprintf fmt "SUB"
+ | MUL -> fprintf fmt "MUL"
+ | DIV -> fprintf fmt "DIV"
+ | MOD -> fprintf fmt "MOD"
+ | AND -> fprintf fmt "AND"
+ | OR -> fprintf fmt "OR"
+ | BAND -> fprintf fmt "BAND"
+ | BOR -> fprintf fmt "BOR"
+ | XOR -> fprintf fmt "XOR"
+ | SHL -> fprintf fmt "SHL"
+ | SHR -> fprintf fmt "SHR"
+ | EQ -> fprintf fmt "EQ"
+ | NE -> fprintf fmt "NE"
+ | LT -> fprintf fmt "LT"
+ | GT -> fprintf fmt "GT"
+ | LE -> fprintf fmt "LE"
+ | GE -> fprintf fmt "GE"
+ | ASSIGN -> fprintf fmt "ASSIGN"
+ | ADD_ASSIGN -> fprintf fmt "ADD_ASSIGN"
+ | SUB_ASSIGN -> fprintf fmt "SUB_ASSIGN"
+ | MUL_ASSIGN -> fprintf fmt "MUL_ASSIGN"
+ | DIV_ASSIGN -> fprintf fmt "DIV_ASSIGN"
+ | MOD_ASSIGN -> fprintf fmt "MOD_ASSIGN"
+ | BAND_ASSIGN -> fprintf fmt "BAND_ASSIGN"
+ | BOR_ASSIGN -> fprintf fmt "BOR_ASSIGN"
+ | XOR_ASSIGN -> fprintf fmt "XOR_ASSIGN"
+ | SHL_ASSIGN -> fprintf fmt "SHL_ASSIGN"
+ | SHR_ASSIGN -> fprintf fmt "SHR_ASSIGN"
and pp_un_op fmt = function
- | MINUS -> fprintf fmt "MINUS"
- | PLUS -> fprintf fmt "PLUS"
- | NOT -> fprintf fmt "NOT"
- | BNOT -> fprintf fmt "BNOT"
- | MEMOF -> fprintf fmt "MEMOF"
- | ADDROF -> fprintf fmt "ADDROF"
- | PREINCR -> fprintf fmt "PREINCR"
- | PREDECR -> fprintf fmt "PREDECR"
- | POSINCR -> fprintf fmt "POSINCR"
- | POSDECR -> fprintf fmt "POSDECR"
+ | MINUS -> fprintf fmt "MINUS"
+ | PLUS -> fprintf fmt "PLUS"
+ | NOT -> fprintf fmt "NOT"
+ | BNOT -> fprintf fmt "BNOT"
+ | MEMOF -> fprintf fmt "MEMOF"
+ | ADDROF -> fprintf fmt "ADDROF"
+ | PREINCR -> fprintf fmt "PREINCR"
+ | PREDECR -> fprintf fmt "PREDECR"
+ | POSINCR -> fprintf fmt "POSINCR"
+ | POSDECR -> fprintf fmt "POSDECR"
and pp_exp fmt exp =
fprintf fmt "exp(%a)" pp_exp_node exp.expr_node
-
+
and pp_exp_node fmt = function
- | NOTHING -> fprintf fmt "NOTHING"
- | UNARY (un_op, exp) -> fprintf fmt "@[<hov 2>%a(%a)@]" pp_un_op un_op pp_exp exp
- | LABELADDR s -> fprintf fmt "@[<hov 2>LABELADDR %s@]" s
- | BINARY (bin_op, exp1, exp2) ->
- fprintf fmt "@[<hov 2>%a %a %a@]" pp_exp exp1 pp_bin_op bin_op pp_exp exp2
- | QUESTION (exp1, exp2, exp3) ->
- fprintf fmt "@[<hov 2>QUESTION(%a, %a, %a)@]" pp_exp exp1 pp_exp exp2 pp_exp exp3
- | CAST ((spec, decl_type), init_exp) ->
- fprintf fmt "@[<hov 2>CAST (%a, %a) %a@]" pp_spec spec pp_decl_type decl_type pp_init_exp init_exp
- | CALL (exp1, exps) ->
- fprintf fmt "@[<hov 2>CALL %a {" pp_exp exp1;
- List.iter
- (fun e -> fprintf fmt ",@ %a" pp_exp e)
- exps;
- fprintf fmt "}@]"
- | COMMA exps ->
- fprintf fmt "@[<hov 2>COMMA {";
- List.iter
- (fun e -> fprintf fmt ",@ %a" pp_exp e)
- exps;
- fprintf fmt "}@]"
- | CONSTANT c -> fprintf fmt "%a" pp_const c
- | PAREN exp -> fprintf fmt "PAREN(%a)" pp_exp exp
- | VARIABLE s -> fprintf fmt "VAR %s" s
- | EXPR_SIZEOF exp -> fprintf fmt "EXPR_SIZEOF(%a)" pp_exp exp
- | TYPE_SIZEOF (spec, decl_type) ->
- fprintf fmt "TYP_SIZEOF(%a,%a)" pp_spec spec pp_decl_type decl_type
- | EXPR_ALIGNOF exp ->
- fprintf fmt "EXPR_ALIGNOF(%a)" pp_exp exp
- | TYPE_ALIGNOF (spec, decl_type) ->
- fprintf fmt "TYP_ALIGNEOF(%a,%a)" pp_spec spec pp_decl_type decl_type
- | INDEX (exp1, exp2) ->
- fprintf fmt "INDEX(%a, %a)" pp_exp exp1 pp_exp exp2
- | MEMBEROF (exp, s) ->
- fprintf fmt "MEMBEROF(%a,%s)" pp_exp exp s
- | MEMBEROFPTR (exp, s) ->
- fprintf fmt "MEMBEROFPTR(%a,%s)" pp_exp exp s
- | GNU_BODY bl -> fprintf fmt "GNU_BODY %a" pp_block bl
- | EXPR_PATTERN s -> fprintf fmt "EXPR_PATTERN %s" s
-
+ | NOTHING -> fprintf fmt "NOTHING"
+ | UNARY (un_op, exp) -> fprintf fmt "@[<hov 2>%a(%a)@]" pp_un_op un_op pp_exp exp
+ | LABELADDR s -> fprintf fmt "@[<hov 2>LABELADDR %s@]" s
+ | BINARY (bin_op, exp1, exp2) ->
+ fprintf fmt "@[<hov 2>%a %a %a@]" pp_exp exp1 pp_bin_op bin_op pp_exp exp2
+ | QUESTION (exp1, exp2, exp3) ->
+ fprintf fmt "@[<hov 2>QUESTION(%a, %a, %a)@]" pp_exp exp1 pp_exp exp2 pp_exp exp3
+ | CAST ((spec, decl_type), init_exp) ->
+ fprintf fmt "@[<hov 2>CAST (%a, %a) %a@]" pp_spec spec pp_decl_type decl_type pp_init_exp init_exp
+ | CALL (exp1, exps) ->
+ fprintf fmt "@[<hov 2>CALL %a {" pp_exp exp1;
+ List.iter
+ (fun e -> fprintf fmt ",@ %a" pp_exp e)
+ exps;
+ fprintf fmt "}@]"
+ | COMMA exps ->
+ fprintf fmt "@[<hov 2>COMMA {";
+ List.iter
+ (fun e -> fprintf fmt ",@ %a" pp_exp e)
+ exps;
+ fprintf fmt "}@]"
+ | CONSTANT c -> fprintf fmt "%a" pp_const c
+ | PAREN exp -> fprintf fmt "PAREN(%a)" pp_exp exp
+ | VARIABLE s -> fprintf fmt "VAR %s" s
+ | EXPR_SIZEOF exp -> fprintf fmt "EXPR_SIZEOF(%a)" pp_exp exp
+ | TYPE_SIZEOF (spec, decl_type) ->
+ fprintf fmt "TYP_SIZEOF(%a,%a)" pp_spec spec pp_decl_type decl_type
+ | EXPR_ALIGNOF exp ->
+ fprintf fmt "EXPR_ALIGNOF(%a)" pp_exp exp
+ | TYPE_ALIGNOF (spec, decl_type) ->
+ fprintf fmt "TYP_ALIGNEOF(%a,%a)" pp_spec spec pp_decl_type decl_type
+ | INDEX (exp1, exp2) ->
+ fprintf fmt "INDEX(%a, %a)" pp_exp exp1 pp_exp exp2
+ | MEMBEROF (exp, s) ->
+ fprintf fmt "MEMBEROF(%a,%s)" pp_exp exp s
+ | MEMBEROFPTR (exp, s) ->
+ fprintf fmt "MEMBEROFPTR(%a,%s)" pp_exp exp s
+ | GNU_BODY bl -> fprintf fmt "GNU_BODY %a" pp_block bl
+ | EXPR_PATTERN s -> fprintf fmt "EXPR_PATTERN %s" s
+
and pp_init_exp fmt = function
- | NO_INIT -> fprintf fmt "NO_INIT"
- | SINGLE_INIT exp ->
+ | NO_INIT -> fprintf fmt "NO_INIT"
+ | SINGLE_INIT exp ->
fprintf fmt "SINGLE_INIT %a" pp_exp exp
- | COMPOUND_INIT l ->
+ | COMPOUND_INIT l ->
fprintf fmt "@[<hov 2>COMPOUND_INIT {";
match l with
- | [] -> fprintf fmt "}@]"
- | (iw, ie)::rest ->
- fprintf fmt ",@ (%a, %a)" pp_initwhat iw pp_init_exp ie;
- List.iter (fun (iw, ie) -> fprintf fmt ",@ (%a, %a)" pp_initwhat iw pp_init_exp ie) rest;
- fprintf fmt "}@]"
-
+ | [] -> fprintf fmt "}@]"
+ | (iw, ie)::rest ->
+ fprintf fmt ",@ (%a, %a)" pp_initwhat iw pp_init_exp ie;
+ List.iter (fun (iw, ie) -> fprintf fmt ",@ (%a, %a)" pp_initwhat iw pp_init_exp ie) rest;
+ fprintf fmt "}@]"
+
and pp_initwhat fmt = function
- | NEXT_INIT -> fprintf fmt "NEXT_INIT"
- | INFIELD_INIT (s,iw) -> fprintf fmt "@[<hov 2>INFIELD_INIT (%s, %a)@]" s pp_initwhat iw
- | ATINDEX_INIT (exp,iw) -> fprintf fmt "@[<hov 2>ATINDEX_INIT (%a, %a)@]" pp_exp exp pp_initwhat iw
- | ATINDEXRANGE_INIT (exp1, exp2) -> fprintf fmt "@[<hov 2>ATINDEXRANGE_INIT (%a, %a)@]" pp_exp exp1 pp_exp exp2
-
+ | NEXT_INIT -> fprintf fmt "NEXT_INIT"
+ | INFIELD_INIT (s,iw) -> fprintf fmt "@[<hov 2>INFIELD_INIT (%s, %a)@]" s pp_initwhat iw
+ | ATINDEX_INIT (exp,iw) -> fprintf fmt "@[<hov 2>ATINDEX_INIT (%a, %a)@]" pp_exp exp pp_initwhat iw
+ | ATINDEXRANGE_INIT (exp1, exp2) -> fprintf fmt "@[<hov 2>ATINDEXRANGE_INIT (%a, %a)@]" pp_exp exp1 pp_exp exp2
+
and pp_attr fmt (s,el) =
fprintf fmt "ATTR (%s, {" s;
match el with
- | [] -> fprintf fmt "})"
- | e :: es ->
- fprintf fmt ",@ %a" pp_exp e;
- List.iter (fun e -> fprintf fmt ",@ %a" pp_exp e) es;
- fprintf fmt "})"
+ | [] -> fprintf fmt "})"
+ | e :: es ->
+ fprintf fmt ",@ %a" pp_exp e;
+ List.iter (fun e -> fprintf fmt ",@ %a" pp_exp e) es;
+ fprintf fmt "})"
and pp_attrs fmt l =
fprintf fmt "{";
match l with
- | [] -> fprintf fmt "}"
- | a :: attrs ->
- fprintf fmt ",@ %a" pp_attr a;
- List.iter (fun a -> fprintf fmt ",@ %a" pp_attr a) attrs;
- fprintf fmt "}"
+ | [] -> fprintf fmt "}"
+ | a :: attrs ->
+ fprintf fmt ",@ %a" pp_attr a;
+ List.iter (fun a -> fprintf fmt ",@ %a" pp_attr a) attrs;
+ fprintf fmt "}"
diff --git a/src/kernel_services/ast_printing/cil_descriptive_printer.ml b/src/kernel_services/ast_printing/cil_descriptive_printer.ml
index f4c2885c064..214371c00f7 100644
--- a/src/kernel_services/ast_printing/cil_descriptive_printer.ml
+++ b/src/kernel_services/ast_printing/cil_descriptive_printer.ml
@@ -37,15 +37,15 @@ class descriptive_printer = object (self)
match vi.vdescr with
| Some vd ->
if vi.vdescrpure || not useTemps then
- Format.fprintf fmt "%s" vd
+ Format.fprintf fmt "%s" vd
else begin
- try
- let _, name, _ = List.find (fun (vi', _, _) -> vi == vi') temps in
- Format.fprintf fmt "%s" name
- with Not_found ->
- let name = "tmp" ^ string_of_int (List.length temps) in
- temps <- (vi, name, vi.vdescr) :: temps;
- Format.fprintf fmt "%s" name
+ try
+ let _, name, _ = List.find (fun (vi', _, _) -> vi == vi') temps in
+ Format.fprintf fmt "%s" name
+ with Not_found ->
+ let name = "tmp" ^ string_of_int (List.length temps) in
+ temps <- (vi, name, vi.vdescr) :: temps;
+ Format.fprintf fmt "%s" name
end
| None ->
super#varinfo fmt vi
@@ -55,13 +55,13 @@ class descriptive_printer = object (self)
but we shouldn't substitute there since "foo(a,b) = foo(a,b)"
would make no sense to the user.) *)
method! exp fmt e = match e.enode with
- | Lval (Var vi, o)
- | StartOf (Var vi, o) ->
- Format.fprintf fmt "%a%a" self#pVarDescriptive vi self#offset o
- | AddrOf (Var vi, o) ->
- (* No parens needed, since offsets have higher precedence than & *)
- Format.fprintf fmt "& %a%a" self#pVarDescriptive vi self#offset o
- | _ -> super#exp fmt e
+ | Lval (Var vi, o)
+ | StartOf (Var vi, o) ->
+ Format.fprintf fmt "%a%a" self#pVarDescriptive vi self#offset o
+ | AddrOf (Var vi, o) ->
+ (* No parens needed, since offsets have higher precedence than & *)
+ Format.fprintf fmt "& %a%a" self#pVarDescriptive vi self#offset o
+ | _ -> super#exp fmt e
end
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 583f672121c..28b8fa420e2 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -273,7 +273,7 @@ module Precedence = struct
(* Multiplicative *)
| TBinOp((Div|Mod|Mult),_,_) -> multiplicativeLevel
| Tapp({ l_var_info },[],[_;_])
- when l_var_info.lv_name = "\\repeat" -> bitwiseLevel
+ when l_var_info.lv_name = "\\repeat" -> bitwiseLevel
(* Unary *)
| TCastE(_,_) -> 30
| TAddrOf(_) -> addrOfLevel
@@ -308,7 +308,7 @@ module Precedence = struct
| AInt _ | AStr _ | ACons _ -> 0
| ASizeOf _ | ASizeOfE _ -> 20
| AAlignOf _ | AAlignOfE _ -> 20
- | AUnOp (uo, _) ->
+ | AUnOp (uo, _) ->
getParenthLevel
(Cil.dummy_exp
(UnOp(uo, Cil.zero ~loc:Cil_datatype.Location.unknown, Cil.intType)))
@@ -385,7 +385,7 @@ let is_same_direction_rel dir op =
(* when pretty-printing relation chains, a < b && b' < c, it can happen that
b has a coercion and b' hasn't or vice-versa (bc c is an integer and a and
- b are ints for instance). We nevertheless want to
+ b are ints for instance). We nevertheless want to
pretty-print that as a < b < c. For that, we compare b and b' after having
removed any existing head coercion.
*)
@@ -474,11 +474,11 @@ class cil_printer () = object (self)
method private current_behavior = current_behavior
method private set_current_behavior b =
- assert (current_behavior = None);
+ assert (current_behavior = None);
current_behavior <- Some b
method private reset_current_behavior () =
- assert (current_behavior <> None);
+ assert (current_behavior <> None);
current_behavior <- None
val mutable has_annot = false
@@ -488,8 +488,8 @@ class cil_printer () = object (self)
method private push_stmt s = Stack.push s current_stmt
method private pop_stmt s =
- ignore (Stack.pop current_stmt);
- has_annot <- false;
+ ignore (Stack.pop current_stmt);
+ has_annot <- false;
s
method private current_stmt =
@@ -509,7 +509,7 @@ class cil_printer () = object (self)
(*fprintf fmt "/* %Lx */" i;*)
(** We must make sure to capture the type of the constant. For some
constants this is done with a suffix, for others with a cast
- prefix.*)
+ prefix.*)
let suffix = match ik with
| IUInt -> "U"
| ILong -> "L"
@@ -545,7 +545,7 @@ class cil_printer () = object (self)
| CChr(c) -> fprintf fmt "'%s'" (Escape.escape_char c)
| CReal(_, _, Some s) -> fprintf fmt "%s" s
| CReal(f, fsize, None) ->
- fprintf fmt "%a%s"
+ fprintf fmt "%a%s"
Floating_point.pretty f
(match fsize with
FFloat -> "f"
@@ -704,7 +704,7 @@ class cil_printer () = object (self)
true
else if contextprec == Precedence.bitwiseLevel then
(* quiet down some GCC warnings *)
- thisLevel == Precedence.additiveLevel
+ thisLevel == Precedence.additiveLevel
|| thisLevel == Precedence.comparativeLevel
else
false
@@ -801,7 +801,7 @@ class cil_printer () = object (self)
BinOp((PlusA|PlusPI|IndexPI),
{enode = Lval(lv')},
{enode=Const(CInt64(one,_,_))},_)
- when LvalStructEq.equal lv lv' && Integer.equal one Integer.one
+ when LvalStructEq.equal lv lv' && Integer.equal one Integer.one
&& not state.print_cil_as_is ->
fprintf fmt "%a ++%s"
(self#lval_prec Precedence.indexLevel) lv
@@ -849,13 +849,13 @@ class cil_printer () = object (self)
pp_call None (Cil.evar f) fmt args
| Local_init(vi, ConsInit(f, args, Plain_func), _) ->
Format.fprintf fmt "@[<2>%a =@ %a@]" self#vdecl vi
- (pp_call None (Cil.evar f)) args;
- (* In cabs2cil we have turned the call to builtin_va_arg into a
- three-argument call: the last argument is the address of the
- destination *)
+ (pp_call None (Cil.evar f)) args;
+ (* In cabs2cil we have turned the call to builtin_va_arg into a
+ three-argument call: the last argument is the address of the
+ destination *)
| Call(None, {enode = Lval(Var vi, NoOffset)},
[dest; {enode = SizeOf t}; adest], (l,_))
- when vi.vname = "__builtin_va_arg"
+ when vi.vname = "__builtin_va_arg"
&& not state.print_cil_as_is ->
let destlv = match (Cil.stripCasts adest).enode with
AddrOf destlv -> destlv
@@ -886,7 +886,7 @@ class cil_printer () = object (self)
(* In cabs2cil we have dropped the last argument in the call to
__builtin_next_arg. *)
| Call(res, {enode = Lval(Var vi, NoOffset)}, [ ], l)
- when vi.vname = "__builtin_next_arg"
+ when vi.vname = "__builtin_next_arg"
&& not state.print_cil_as_is ->
let last = self#getLastNamedArgument () in
self#instr fmt (Call(res,Cil.dummy_exp(Lval(Var vi,NoOffset)),[last],l))
@@ -976,11 +976,11 @@ class cil_printer () = object (self)
(* No need to output a final colon if there's no label. *)
if not lab_nil then
Pretty_utils.pp_list ~pre:"@;@[:" ~suf:"@]" ~sep:",@ "
- (fun fmt r ->
- match pickLabel !r.labels with
+ (fun fmt r ->
+ match pickLabel !r.labels with
| Some label -> Format.pp_print_string fmt label
| None ->
- Kernel.error "Cannot find label for target of asm goto: %a"
+ Kernel.error "Cannot find label for target of asm goto: %a"
(self#without_annot self#stmt) !r;
Format.pp_print_string fmt "__invalid_label")
fmt
@@ -990,9 +990,9 @@ class cil_printer () = object (self)
| Code_annot (annot, l) ->
has_annot <- true;
if logic_printer_enabled then begin
- self#line_directive ~forcefile:false fmt l;
+ self#line_directive ~forcefile:false fmt l;
Format.fprintf fmt "%t " (fun fmt -> self#pp_open_annotation fmt);
- self#code_annotation fmt annot ;
+ self#code_annotation fmt annot ;
Format.fprintf fmt "@ %t" (fun fmt -> self#pp_close_annotation fmt);
end
@@ -1045,8 +1045,8 @@ class cil_printer () = object (self)
method initinfo fmt io =
match io.init with
- | None -> fprintf fmt "{}"
- | Some i -> fprintf fmt "%a" self#init i
+ | None -> fprintf fmt "{}"
+ | Some i -> fprintf fmt "%a" self#init i
method fundec fmt fd = fprintf fmt "%a" self#varinfo fd.svar
@@ -1064,13 +1064,13 @@ class cil_printer () = object (self)
let was_ghost = is_ghost in
let display_ghost = s.ghost && not was_ghost in
if display_ghost then begin
- is_ghost <- true;
+ is_ghost <- true;
Format.fprintf fmt "%t %a "
(fun fmt -> self#pp_open_annotation fmt) self#pp_acsl_keyword "ghost"
end;
self#stmtkind s.sattr next fmt s.skind ;
if display_ghost then begin
- is_ghost <- false;
+ is_ghost <- false;
self#pp_close_annotation fmt
end
end;
@@ -1088,34 +1088,34 @@ class cil_printer () = object (self)
| _, _, _ :: _,_ | _, _ :: _, _, _ -> true
| _::_::_,[],[],Stmt_block s ->
not (Cil.has_extern_local_init blk) &&
- (self#stmt_has_annot s || s.labels <> [])
- (* Do not put braces around a Local_init statement if we are not
- in the appropriate block. This trumps the presence of a binding
- annotation (or a label at block level, in case of something like:
- { /* start of scoping block */
- //@ slicing pragma stmt;
- /* { */ /* start of non-scoping block
- int x = 42;
- x++;
- ...
- /* } */ /* end of non-scoping block
+ (self#stmt_has_annot s || s.labels <> [])
+ (* Do not put braces around a Local_init statement if we are not
+ in the appropriate block. This trumps the presence of a binding
+ annotation (or a label at block level, in case of something like:
+ { /* start of scoping block */
+ //@ slicing pragma stmt;
+ /* { */ /* start of non-scoping block
+ int x = 42;
x++;
- } /* end of scoping block */
+ ...
+ /* } */ /* end of non-scoping block
+ x++;
+ } /* end of scoping block */
In such case, the pretty-printer can't satisfy the scope of the
annotation and the scope of x at the same time. We favor x, which
gives us at least a correct, compilable, C code.
- *)
+ *)
| _::_::_,[],[],_ -> is_cfg_block ctxt
| [ { skind = Block b } as s' ], [], [], Stmt_block s ->
(b.bscoping ||
(not (Cil.has_extern_local_init b) && self#stmt_has_annot s))
&& self#require_braces ctxt b
&& not (self#require_braces (Stmt_block s') b)
- (* If b wants braces in current context but not in subcontext, put
- braces directly there. Otherwise, wait for children to do it. *)
+ (* If b wants braces in current context but not in subcontext, put
+ braces directly there. Otherwise, wait for children to do it. *)
| [ { skind = Block b } ], [], [], _ -> self#require_braces ctxt b
| [ { skind = UnspecifiedSequence s } ], [], [], _ ->
- self#require_braces ctxt (Cil.block_from_unspecified_sequence s)
+ self#require_braces ctxt (Cil.block_from_unspecified_sequence s)
| [_],[],[], Then_with_else -> self#block_has_dangling_else blk
| [ _ ], [], [], _ -> false
| [],[],[],_ -> false)
@@ -1130,18 +1130,18 @@ class cil_printer () = object (self)
method private block_is_function blk = match blk.bstmts with
| [ { skind = Instr (Call _) } ] -> true
| [ { skind = Instr (Local_init (_, ConsInit _, _)) } ] -> true
- (* NB: a block consisting solely of an initializer is pretty useless,
- but who knows? *)
+ (* NB: a block consisting solely of an initializer is pretty useless,
+ but who knows? *)
| [ { skind = Block blk } ] -> self#block_is_function blk
| _ -> false
method private block_has_dangling_else blk = match blk.bstmts with
- | [ { skind = If(_, { bstmts=[]; battrs=[] }, _, _)
- | If(_, {bstmts=[{skind=Goto _; labels=[]}]; battrs=[]}, _, _)
- | If(_, _, { bstmts=[]; battrs=[] }, _)
- | If(_, _, {bstmts=[{skind=Goto _; labels=[]}]; battrs=[]}, _) } ]
+ | [ { skind = If(_, { bstmts=[]; battrs=[] }, _, _)
+ | If(_, {bstmts=[{skind=Goto _; labels=[]}]; battrs=[]}, _, _)
+ | If(_, _, { bstmts=[]; battrs=[] }, _)
+ | If(_, _, {bstmts=[{skind=Goto _; labels=[]}]; battrs=[]}, _) } ]
-> true
- | [ { skind = Block blk | If(_, _, blk, _) } ] ->
+ | [ { skind = Block blk | If(_, _, blk, _) } ] ->
self#block_has_dangling_else blk
| _ -> false
@@ -1168,29 +1168,29 @@ class cil_printer () = object (self)
if braces && not inline then pp_print_space fmt ();
if blk.blocals <> [] && verbose then
fprintf fmt "@[/* Locals: %a */@]@ "
- (Pretty_utils.pp_list ~sep:",@ " self#varinfo) blk.blocals;
+ (Pretty_utils.pp_list ~sep:",@ " self#varinfo) blk.blocals;
if verbose && not blk.bscoping then fprintf fmt "/* non-scoping */@\n";
- if blk.battrs <> [] then
+ if blk.battrs <> [] then
(* [JS 2012/12/07] could directly call self#attributesGen whenever we are
- sure than it puts its printing material inside a box *)
+ sure than it puts its printing material inside a box *)
fprintf fmt "@[%a@]" (self#attributesGen true) blk.battrs;
let locals_decl = List.filter (fun v -> not v.vdefined) blk.blocals in
if locals_decl <> [] then
- Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@;" ~suf:"@]@ "
- self#vdecl_complete fmt locals_decl;
+ Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@;" ~suf:"@]@ "
+ self#vdecl_complete fmt locals_decl;
let rec iterblock ~cut fmt = function
| [] -> ()
| [ s ] ->
- fprintf fmt "";
- if cut && not inline && not braces then pp_print_cut fmt ();
- self#next_stmt Cil.invalidStmt fmt s
+ fprintf fmt "";
+ if cut && not inline && not braces then pp_print_cut fmt ();
+ self#next_stmt Cil.invalidStmt fmt s
| s_cur :: (s_next :: _ as tail) ->
- Format.fprintf fmt "%a@ %a"
- (self#next_stmt s_next) s_cur
- (iterblock ~cut:false) tail
+ Format.fprintf fmt "%a@ %a"
+ (self#next_stmt s_next) s_cur
+ (iterblock ~cut:false) tail
in
let stmts = blk.bstmts in
- if stmts = [] && not braces then fprintf fmt ";"
+ if stmts = [] && not braces then fprintf fmt ";"
else fprintf fmt "%a" (iterblock ~cut) stmts;
if braces then Format.fprintf fmt "@;<1 -2>}"
@@ -1212,14 +1212,14 @@ class cil_printer () = object (self)
| Some _ when (fst l).Filepath.pos_lnum <= 0 -> ()
(* Do not print lineComment if the same line as above *)
- | Some Line_comment_sparse when (fst l).Filepath.pos_lnum = lastLineNumber ->
+ | Some Line_comment_sparse when (fst l).Filepath.pos_lnum = lastLineNumber ->
()
| Some style ->
let directive = match style with
- | Line_comment | Line_comment_sparse -> "//#line"
- | Line_preprocessor_output when not (Cil.msvcMode ()) -> "#"
- | Line_preprocessor_output | Line_preprocessor_input -> "#line"
+ | Line_comment | Line_comment_sparse -> "//#line"
+ | Line_preprocessor_output when not (Cil.msvcMode ()) -> "#"
+ | Line_preprocessor_output | Line_preprocessor_input -> "#line"
in
let pos = fst l in
lastLineNumber <- pos.Filepath.pos_lnum;
@@ -1228,11 +1228,11 @@ class cil_printer () = object (self)
lastFileName <- pos.Filepath.pos_path;
Format.asprintf " \"%a\""
Datatype.Filepath.pretty pos.Filepath.pos_path
- end else
- ""
+ end else
+ ""
in
- fprintf fmt "@[@<0>\n@<0>%s@<0> @<0>%d@<0> @<0>%s@]@\n"
- directive (fst l).Filepath.pos_lnum filename
+ fprintf fmt "@[@<0>\n@<0>%s@<0> @<0>%d@<0> @<0>%s@]@\n"
+ directive (fst l).Filepath.pos_lnum filename
method stmtkind sattr (next: stmt) fmt = function
| UnspecifiedSequence seq ->
@@ -1247,19 +1247,19 @@ class cil_printer () = object (self)
if verbose ||
Kernel.is_debug_key_enabled Kernel.dkey_print_unspecified
then
- Format.fprintf fmt "@ /*effects: @[(%a) %a@ <-@ %a@]*/"
+ Format.fprintf fmt "@ /*effects: @[(%a) %a@ <-@ %a@]*/"
(Pretty_utils.pp_list ~sep:",@ " self#lval) modifies
- (Pretty_utils.pp_list ~sep:",@ " self#lval) writes
- (Pretty_utils.pp_list ~sep:",@ " self#lval) reads
+ (Pretty_utils.pp_list ~sep:",@ " self#lval) writes
+ (Pretty_utils.pp_list ~sep:",@ " self#lval) reads
in
let rec iterblock fmt = function
| [] -> ()
| [ srw ] ->
- print_stmt (self#next_stmt Cil.invalidStmt) fmt srw
+ print_stmt (self#next_stmt Cil.invalidStmt) fmt srw
| srw_first :: ((s_next,_,_,_,_) :: _ as tail) ->
print_stmt (self#next_stmt s_next) fmt srw_first ;
pp_print_space fmt ();
- iterblock fmt tail
+ iterblock fmt tail
in
fprintf fmt "%t%a%t"
(fun fmt ->
@@ -1286,12 +1286,12 @@ class cil_printer () = object (self)
match pickLabel !sref.labels with
| Some lbl ->
fprintf fmt "@[%a%a %s;@]"
- (fun fmt -> self#line_directive fmt) l
+ (fun fmt -> self#line_directive fmt) l
self#pp_keyword "goto"
- lbl
+ lbl
| None ->
- Kernel.error "Cannot find label for target of goto: %a"
- (self#without_annot self#stmt) !sref;
+ Kernel.error "Cannot find label for target of goto: %a"
+ (self#without_annot self#stmt) !sref;
fprintf fmt "@[%a@ __invalid_label;@]" self#pp_keyword "goto"
end
@@ -1305,10 +1305,10 @@ class cil_printer () = object (self)
(fun fmt -> self#line_directive fmt) l
self#pp_keyword "continue"
- | Instr i ->
+ | Instr i ->
self#instr fmt i
- | If(be,t,{bstmts=[];battrs=[]},l)
+ | If(be,t,{bstmts=[];battrs=[]},l)
when not state.print_cil_as_is ->
fprintf fmt "@[<hv>%a@[<v 2>%a (%a) %a@]@]"
(fun fmt -> self#line_directive ~forcefile:false fmt) l
@@ -1324,7 +1324,7 @@ class cil_printer () = object (self)
self#exp be
(self#unboxed_block Other) t
- | If(be,{bstmts=[];battrs=[]},e,l)
+ | If(be,{bstmts=[];battrs=[]},e,l)
when not state.print_cil_as_is ->
fprintf fmt "@[<hv>%a@[<v 2>%a (%a) %a@]@]"
(fun fmt -> self#line_directive ~forcefile:false fmt) l
@@ -1348,7 +1348,7 @@ class cil_printer () = object (self)
|| not (self#inline_block Then_with_else t)
|| not (self#inline_block Other e)
|| (* call to a function in both branches (for GUI' status bullets) *)
- (force_brace && self#block_is_function t && self#block_is_function e)
+ (force_brace && self#block_is_function t && self#block_is_function e)
in
fprintf fmt "@[<v 2>%a (%a) %a@]"
self#pp_keyword "if"
@@ -1381,19 +1381,19 @@ class cil_printer () = object (self)
in
((* Maybe the first thing is a conditional. Turn it into a WHILE *)
try
- let rec skipEmpty = function
- | [] -> []
+ let rec skipEmpty = function
+ | [] -> []
| { skind = Instr (Skip _) } as h :: rest
- when self#may_be_skipped h-> skipEmpty rest
- | x -> x
- in
- let term, bodystmts =
- (* Bill McCloskey: Do not remove the If if it has labels *)
- match skipEmpty b.bstmts with
- | { skind = If(e,tb,fb,_) } as to_skip :: rest
- when not state.print_cil_as_is
- && self#may_be_skipped to_skip ->
- (match skipEmpty tb.bstmts, skipEmpty fb.bstmts with
+ when self#may_be_skipped h-> skipEmpty rest
+ | x -> x
+ in
+ let term, bodystmts =
+ (* Bill McCloskey: Do not remove the If if it has labels *)
+ match skipEmpty b.bstmts with
+ | { skind = If(e,tb,fb,_) } as to_skip :: rest
+ when not state.print_cil_as_is
+ && self#may_be_skipped to_skip ->
+ (match skipEmpty tb.bstmts, skipEmpty fb.bstmts with
| [], [ { skind = Break _ } as s ] when self#may_be_skipped s ->
e, rest
| [], [ { skind = Goto(sref, _) } as s ]
@@ -1401,31 +1401,31 @@ class cil_printer () = object (self)
&& Cil_datatype.Stmt.equal !sref next ->
e, rest
| [ { skind = Break _ } as s ], [] when self#may_be_skipped s ->
- Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
+ Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
| [ { skind = Goto(sref, _) } as s ], []
when self#may_be_skipped s
&& Cil_datatype.Stmt.equal !sref next ->
Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
- | _ -> raise Not_found)
- | _ -> raise Not_found
- in
- let b = match skipEmpty bodystmts with
- [{ skind=Block b} as s ] when self#may_be_skipped s -> b
- | _ -> { b with bstmts = bodystmts }
- in
- Format.fprintf fmt "%a@[<v 2>%a (%a) %t%a@]"
- (fun fmt -> self#line_directive fmt) l
+ | _ -> raise Not_found)
+ | _ -> raise Not_found
+ in
+ let b = match skipEmpty bodystmts with
+ [{ skind=Block b} as s ] when self#may_be_skipped s -> b
+ | _ -> { b with bstmts = bodystmts }
+ in
+ Format.fprintf fmt "%a@[<v 2>%a (%a) %t%a@]"
+ (fun fmt -> self#line_directive fmt) l
self#pp_keyword "while"
- self#exp term
- pp_sattr
- (self#unboxed_block Other) b;
+ self#exp term
+ pp_sattr
+ (self#unboxed_block Other) b;
with Not_found ->
- Format.fprintf fmt "%a@[<v 2>%a (1) %t%a@]"
- (fun fmt -> self#line_directive fmt) l
+ Format.fprintf fmt "%a@[<v 2>%a (1) %t%a@]"
+ (fun fmt -> self#line_directive fmt) l
self#pp_keyword "while"
pp_sattr
- (self#unboxed_block Other) b);
+ (self#unboxed_block Other) b);
Format.pp_close_box fmt ()
| Block b ->
@@ -1660,9 +1660,9 @@ class cil_printer () = object (self)
method fieldinfo fmt fi =
fprintf fmt "%a %s%a;"
(self#typ
- (Some (fun fmt ->
- if fi.fname <> Cil.missingFieldName then
- self#varname fmt fi.fname)))
+ (Some (fun fmt ->
+ if fi.fname <> Cil.missingFieldName then
+ self#varname fmt fi.fname)))
fi.ftype
(match fi.fbitfield with
| None -> ""
@@ -1728,9 +1728,9 @@ class cil_printer () = object (self)
| ILong -> "long"
| IULong -> "unsigned long"
| ILongLong ->
- if Cil.msvcMode () then "__int64" else "long long"
+ if Cil.msvcMode () then "__int64" else "long long"
| IULongLong ->
- if Cil.msvcMode () then "unsigned __int64" else "unsigned long long"
+ if Cil.msvcMode () then "unsigned __int64" else "unsigned long long"
)
method typ ?fundecl nameOpt
@@ -1743,8 +1743,8 @@ class cil_printer () = object (self)
match nameOpt with
| None when not state.print_cil_input && not (Cil.msvcMode ()) -> ()
(* Cannot print the attributes in this case because gcc does not like them
- here, except if we are printing for CIL, or for MSVC. In fact, for
- MSVC we MUST print attributes such as __stdcall *)
+ here, except if we are printing for CIL, or for MSVC. In fact, for
+ MSVC we MUST print attributes such as __stdcall *)
(* if pa = nil then nil else text "/*" ++ pa ++ text "*/"*)
| _ -> self#attributes fmt a
in
@@ -1759,18 +1759,18 @@ class cil_printer () = object (self)
| TComp (comp, _, a) -> (* A reference to a struct *)
fprintf fmt
- "%a %a%a%a"
- self#pp_keyword (if comp.cstruct then "struct" else "union")
- self#varname comp.cname
- self#attributes a
- pname true
+ "%a %a%a%a"
+ self#pp_keyword (if comp.cstruct then "struct" else "union")
+ self#varname comp.cname
+ self#attributes a
+ pname true
| TEnum (enum, a) ->
fprintf fmt "%a %a%a%a"
self#pp_keyword "enum"
self#varname enum.ename
- self#attributes a
- pname true
+ self#attributes a
+ pname true
| TPtr (bt, a) ->
(* Parenthesize the ( * attr name) if a pointer to a function or an
@@ -1778,28 +1778,28 @@ class cil_printer () = object (self)
* before the pointer constructor "(__stdcall *f)". We push them into
* the parenthesis. *)
let (paren: (formatter -> unit) option), (bt': typ) =
- match bt with
- | TFun(rt, args, isva, fa) when Cil.msvcMode () ->
- let an, af', at = Cil.partitionAttributes ~default:Cil.AttrType fa in
- (* We take the af' and we put them into the parentheses *)
- Some
- (fun fmt ->
- fprintf fmt
- "(%a"
- printAttributes af'),
- TFun(rt, args, isva, Cil.addAttributes an at)
- | TFun _ | TArray _ -> (Some (fun fmt -> fprintf fmt "(")), bt
- | _ -> None, bt
+ match bt with
+ | TFun(rt, args, isva, fa) when Cil.msvcMode () ->
+ let an, af', at = Cil.partitionAttributes ~default:Cil.AttrType fa in
+ (* We take the af' and we put them into the parentheses *)
+ Some
+ (fun fmt ->
+ fprintf fmt
+ "(%a"
+ printAttributes af'),
+ TFun(rt, args, isva, Cil.addAttributes an at)
+ | TFun _ | TArray _ -> (Some (fun fmt -> fprintf fmt "(")), bt
+ | _ -> None, bt
in
- let name' =
- fun fmt -> fprintf fmt "*%a%a" printAttributes a pname (a <> [])
+ let name' =
+ fun fmt -> fprintf fmt "*%a%a" printAttributes a pname (a <> [])
in
let name'' =
- fun fmt ->
- (* Put the parenthesis *)
- match paren with
- | Some p -> fprintf fmt "%t%t)" p name'
- | None -> fprintf fmt "%t" name'
+ fun fmt ->
+ (* Put the parenthesis *)
+ match paren with
+ | Some p -> fprintf fmt "%t%t)" p name'
+ | None -> fprintf fmt "%t" name'
in
self#typ (Some name'') fmt bt'
@@ -1809,31 +1809,31 @@ class cil_printer () = object (self)
result if the qualifier is misplaced. *)
let atts_elem, a = Cil.splitArrayAttributes a in
if atts_elem != [] then
- Kernel.failure ~current:true
- "Found some incorrect attributes for array (%a). Please report."
- self#attributes atts_elem;
+ Kernel.failure ~current:true
+ "Found some incorrect attributes for array (%a). Please report."
+ self#attributes atts_elem;
let name' fmt =
- if a = [] then pname fmt false
+ if a = [] then pname fmt false
else if nameOpt = None then
- printAttributes fmt a
- else
- fprintf fmt "(%a%a)" printAttributes a pname true
+ printAttributes fmt a
+ else
+ fprintf fmt "(%a%a)" printAttributes a pname true
in
self#typ
- (Some (fun fmt ->
- fprintf fmt "%t[%t]"
- name'
- (fun fmt ->
- match lo with
- | None -> ()
- | Some e -> self#exp fmt e)
- ))
- fmt
- elemt
+ (Some (fun fmt ->
+ fprintf fmt "%t[%t]"
+ name'
+ (fun fmt ->
+ match lo with
+ | None -> ()
+ | Some e -> self#exp fmt e)
+ ))
+ fmt
+ elemt
| TFun (restyp, args, isvararg, a) ->
let name' fmt =
- if a = [] then pname fmt false
+ if a = [] then pname fmt false
else if nameOpt = None then printAttributes fmt a
else fprintf fmt "(%a%a)" printAttributes a pname (a <> [])
in
@@ -1869,14 +1869,14 @@ class cil_printer () = object (self)
| TNamed (t, a) ->
fprintf fmt "%a%a%a"
- self#varname t.tname
- self#attributes a
- pname true
+ self#varname t.tname
+ self#attributes a
+ pname true
| TBuiltin_va_list a ->
fprintf fmt "__builtin_va_list%a%a"
- self#attributes a
- pname true
+ self#attributes a
+ pname true
(**** PRINTING ATTRIBUTES *********)
method attributes fmt a = self#attributesGen false fmt a
@@ -1893,36 +1893,36 @@ class cil_printer () = object (self)
| "thread", [] when not (Cil.msvcMode ()) -> fprintf fmt "__thread"; false
| "volatile", [] -> self#pp_keyword fmt "volatile"; false
| "restrict", [] -> fprintf fmt "__restrict"; false
- | "missingproto", [] ->
- if self#display_comment () then fprintf fmt "/* missing proto */";
+ | "missingproto", [] ->
+ if self#display_comment () then fprintf fmt "/* missing proto */";
false
- | "cdecl", [] when Cil.msvcMode () ->
+ | "cdecl", [] when Cil.msvcMode () ->
fprintf fmt "__cdecl"; false
| "stdcall", [] when Cil.msvcMode () ->
fprintf fmt "__stdcall"; false
- | "fastcall", [] when Cil.msvcMode () ->
+ | "fastcall", [] when Cil.msvcMode () ->
fprintf fmt "__fastcall"; false
| "declspec", args when Cil.msvcMode () ->
fprintf fmt "__declspec(%a)"
- (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
+ (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
false
- | "w64", [] when Cil.msvcMode () ->
+ | "w64", [] when Cil.msvcMode () ->
fprintf fmt "__w64"; false
| "asm", args ->
fprintf fmt "__asm__(%a)"
- (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
+ (Pretty_utils.pp_list ~sep:"" self#attrparam) args;
false
(* we suppress printing mode(__si__) because it triggers an
- internal compiler error in all current gcc versions
+ internal compiler error in all current gcc versions
sm: I've now encountered a problem with mode(__hi__)...
I don't know what's going on, but let's try disabling all "mode". *)
| "mode", [ACons(tag,[])] ->
if self#display_comment () then fprintf fmt "/* mode(%s) */" tag;
false
- (* sm: also suppress "format" because we seem to print it in
+ (* sm: also suppress "format" because we seem to print it in
a way gcc does not like *)
- | "format", _ ->
+ | "format", _ ->
if self#display_comment () then fprintf fmt "/* format attribute */";
false
@@ -1931,17 +1931,17 @@ class cil_printer () = object (self)
(* sm: here's another one I don't want to see gcc warnings about.. *)
| "mayPointToStack", _ when not state.print_cil_input ->
(* [matth: may be inside another comment.]
- -> text "/*mayPointToStack*/", false *)
+ -> text "/*mayPointToStack*/", false *)
false
| "arraylen", [a] ->
if self#display_comment () then fprintf fmt "/*[%a]*/" self#attrparam a;
false
- | "static",_ ->
+ | "static",_ ->
if self#display_comment () then fprintf fmt "/* static */"; false
| "", _ ->
fprintf fmt "%a "
- (Pretty_utils.pp_list ~sep:" " self#attrparam) args;
+ (Pretty_utils.pp_list ~sep:" " self#attrparam) args;
true
| s, _ when
s = Cil.bitfield_attribute_name &&
@@ -1951,14 +1951,14 @@ class cil_printer () = object (self)
| _ -> (* This is the default case *)
(* Add underscores to the name *)
let an' =
- if Cil.msvcMode () then "__" ^ an else "__" ^ an ^ "__"
+ if Cil.msvcMode () then "__" ^ an else "__" ^ an ^ "__"
in
(match args with
| [] -> fprintf fmt "%s" an'
| _ :: _ ->
- fprintf fmt "%s(%a)"
- an'
- (Pretty_utils.pp_list ~sep:"," self#attrparam) args);
+ fprintf fmt "%s(%a)"
+ an'
+ (Pretty_utils.pp_list ~sep:"," self#attrparam) args);
true)
| AttrAnnot s ->
fprintf fmt "%s" (Cil.mkAttrAnnot s); false
@@ -1967,13 +1967,13 @@ class cil_printer () = object (self)
let thisLevel = Precedence.getParenthLevelAttrParam a in
let needParens =
if thisLevel >= contextprec then
- true
+ true
else if contextprec == Precedence.bitwiseLevel then
- (* quiet down some GCC warnings *)
- thisLevel == Precedence.additiveLevel
- || thisLevel == Precedence.comparativeLevel
+ (* quiet down some GCC warnings *)
+ thisLevel == Precedence.additiveLevel
+ || thisLevel == Precedence.comparativeLevel
else
- false
+ false
in
if needParens then fprintf fmt "(%a)" self#attrparam a
else self#attrparam fmt a
@@ -1991,8 +1991,8 @@ class cil_printer () = object (self)
| ACons("__fc_float", [AStr s]) -> pp_print_string fmt s
| ACons(s,al) ->
fprintf fmt "%s(%a)"
- s
- (Pretty_utils.pp_list ~sep:"" self#attrparam) al
+ s
+ (Pretty_utils.pp_list ~sep:"" self#attrparam) al
| ASizeOfE a ->
fprintf fmt "%a(%a)"
self#pp_keyword "sizeof"
@@ -2007,9 +2007,9 @@ class cil_printer () = object (self)
fprintf fmt "%a %a" self#unop u (self#attribute_prec level) a1
| ABinOp(b,a1,a2) ->
fprintf fmt "@[(%a)%a@ (%a) @]"
- (self#attribute_prec level) a1
- self#binop b
- (self#attribute_prec level) a2
+ (self#attribute_prec level) a1
+ self#binop b
+ (self#attribute_prec level) a2
| ADot (ap, s) ->
fprintf fmt "%a.%s" self#attrparam ap s
| AStar a1 ->
@@ -2020,9 +2020,9 @@ class cil_printer () = object (self)
fprintf fmt "%a[%a]" self#attrparam a1 self#attrparam a2
| AQuestion (a1, a2, a3) ->
fprintf fmt "%a ? %a : %a"
- self#attrparam a1
- self#attrparam a2
- self#attrparam a3
+ self#attrparam a1
+ self#attrparam a2
+ self#attrparam a3
(* A general way of printing lists of attributes *)
method private attributesGen (block: bool) fmt (a: attributes) =
@@ -2075,13 +2075,13 @@ class cil_printer () = object (self)
fprintf fmt "L";
List.iter
(fun elt ->
- if (elt >= Int64.zero &&
- elt <= (Int64.of_int 255)) then
- fprintf fmt "%S"
- (Escape.escape_char (Char.chr (Int64.to_int elt)))
- else
- fprintf fmt "\"\\x%LX\"" elt;
- fprintf fmt "@ ")
+ if (elt >= Int64.zero &&
+ elt <= (Int64.of_int 255)) then
+ fprintf fmt "%S"
+ (Escape.escape_char (Char.chr (Int64.to_int elt)))
+ else
+ fprintf fmt "\"\\x%LX\"" elt;
+ fprintf fmt "@ ")
s;
(* we cannot print L"\xabcd" "feedme" as L"\xabcdfeedme" -- the former
has 7 wide characters and the later has 3. *)
@@ -2098,31 +2098,31 @@ class cil_printer () = object (self)
function
| Ctype typ -> self#typ name fmt typ
| Linteger ->
- let res =
- if Kernel.Unicode.get () then Utf8_logic.integer else "integer"
+ let res =
+ if Kernel.Unicode.get () then Utf8_logic.integer else "integer"
in
Format.fprintf fmt "%s%t" res pname
| Lreal ->
- let res =
- if Kernel.Unicode.get () then Utf8_logic.real else "real"
+ let res =
+ if Kernel.Unicode.get () then Utf8_logic.real else "real"
in
Format.fprintf fmt "%s%t" res pname
| Ltype ({ lt_name = name},[]) when name = Utf8_logic.boolean->
- let res =
- if Kernel.Unicode.get () then Utf8_logic.boolean else "boolean"
+ let res =
+ if Kernel.Unicode.get () then Utf8_logic.boolean else "boolean"
in
Format.fprintf fmt "%s%t" res pname
| Ltype (s,l) ->
fprintf fmt "%a%a%t" self#logic_type_info s
- ((* the space avoids the issue of list<list<int>> where the double >
- would be read as a shift. It could be optimized away in most of
- the cases. *)
- Pretty_utils.pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@]>@ "
- (self#logic_type None)) l pname
+ ((* the space avoids the issue of list<list<int>> where the double >
+ would be read as a shift. It could be optimized away in most of
+ the cases. *)
+ Pretty_utils.pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@]>@ "
+ (self#logic_type None)) l pname
| Larrow (args,rt) ->
fprintf fmt "@[@[<2>{@ %a@]}@]%a%t"
- (Pretty_utils.pp_list ~sep:",@ " (self#logic_type None)) args
- (self#logic_type None) rt pname
+ (Pretty_utils.pp_list ~sep:",@ " (self#logic_type None)) args
+ (self#logic_type None) rt pname
| Lvar s -> fprintf fmt "%a%t" self#varname s pname
method private name fmt s =
@@ -2133,13 +2133,13 @@ class cil_printer () = object (self)
let thisLevel = Precedence.getParenthLevelLogic e.term_node in
let needParens =
if thisLevel >= contextprec then
- true
+ true
else if contextprec == Precedence.bitwiseLevel then
- (* quiet down some GCC warnings *)
- thisLevel == Precedence.additiveLevel
- || thisLevel == Precedence.comparativeLevel
+ (* quiet down some GCC warnings *)
+ thisLevel == Precedence.additiveLevel
+ || thisLevel == Precedence.comparativeLevel
else
- false
+ false
in
if needParens then fprintf fmt "@[<hov 2>(%a)@]" self#term e
else self#term fmt e
@@ -2151,11 +2151,11 @@ class cil_printer () = object (self)
if debug then
fprintf fmt "/*(type:%a */" (self#logic_type None) t.term_type;
begin match t.term_name with
- | [] -> self#term_node fmt t
- | _ :: _ ->
- fprintf fmt "(@[%a:@ %a@])"
- (Pretty_utils.pp_list ~sep:":@ " self#name) t.term_name
- self#term_node t
+ | [] -> self#term_node fmt t
+ | _ :: _ ->
+ fprintf fmt "(@[%a:@ %a@])"
+ (Pretty_utils.pp_list ~sep:":@ " self#name) t.term_name
+ self#term_node t
end;
if debug then fprintf fmt "/*)*/"
@@ -2246,7 +2246,7 @@ class cil_printer () = object (self)
~sep:",@ " ~pre:"@[<hov>" ~suf:"@]@;" self#term_node) l
| _ ->
fprintf fmt "%a%a" self#varname ci.ctor_name
- (Pretty_utils.pp_list ~pre:"(@[" ~suf:"@])" ~sep:",@ " self#term)
+ (Pretty_utils.pp_list ~pre:"(@[" ~suf:"@])" ~sep:",@ " self#term)
args)
| TLval lv -> fprintf fmt "%a" (self#term_lval_prec current_level) lv
| TSizeOf t ->
@@ -2269,8 +2269,8 @@ class cil_printer () = object (self)
(self#term_prec current_level) r
| TCastE (ty,e) ->
fprintf fmt "(%a)%a" (self#typ None) ty
- (self#term_prec current_level) e
- | TAddrOf lv ->
+ (self#term_prec current_level) e
+ | TAddrOf lv ->
fprintf fmt "&%a" (self#term_lval_prec Precedence.addrOfLevel) lv
| TStartOf lv -> fprintf fmt "(%a)%a"
(self#logic_type None) t.term_type
@@ -2280,121 +2280,121 @@ class cil_printer () = object (self)
| Tapp ({ l_var_info },[],[e1; e2])
when l_var_info.lv_name = "\\concat" && not state.print_cil_as_is ->
fprintf fmt "%a ^ %a"
- (self#term_prec current_level) e1
- (self#term_prec current_level) e2
+ (self#term_prec current_level) e1
+ (self#term_prec current_level) e2
| Tapp ({ l_var_info },[],[e1;e2])
- when l_var_info.lv_name = "\\repeat" && not state.print_cil_as_is ->
+ when l_var_info.lv_name = "\\repeat" && not state.print_cil_as_is ->
fprintf fmt "%a *^ %a"
(self#term_prec current_level) e1
(self#term_prec current_level) e2
- | Tapp (f, labels, tl) ->
+ | Tapp (f, labels, tl) ->
fprintf fmt "%a%a%a"
- self#logic_info f
- self#labels labels
- (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@]" ~sep:",@ " self#term) tl
+ self#logic_info f
+ self#labels labels
+ (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@]" ~sep:",@ " self#term) tl
| Tif (cond,th,el) ->
fprintf fmt "@[<2>%a?@;%a:@;%a@]"
- (self#term_prec current_level) cond
- (self#term_prec current_level) th
- (self#term_prec current_level) el
- | Tat (t,lab) ->
- let old_label = current_label in
- current_label <- lab;
- if Cil_datatype.Logic_label.equal lab Logic_const.old_label then
- fprintf fmt "@[%a(@[%a@])@]" self#pp_acsl_keyword "\\old" self#term t
- else
- fprintf fmt "@[%a(@[@[%a@],@,@[%a@]@])@]"
- self#pp_acsl_keyword "\\at" self#term t self#logic_label lab;
- current_label <- old_label
- | Toffset (l,t) ->
- fprintf fmt "%a%a(%a)" self#pp_acsl_keyword "\\offset"
- self#labels [l] self#term t
- | Tbase_addr (l,t) ->
- fprintf fmt "%a%a(%a)" self#pp_acsl_keyword "\\base_addr"
- self#labels [l] self#term t
- | Tblock_length (l,t) ->
- fprintf fmt "%a%a(%a)" self#pp_acsl_keyword "\\block_length"
- self#labels [l] self#term t
- | Tnull -> self#pp_acsl_keyword fmt "\\null"
- | TCoerce (e,ty) ->
- fprintf fmt "%a@ :>@ %a"
- (self#term_prec current_level) e (self#typ None) ty
- | TCoerceE (e,ce) ->
- fprintf fmt "%a :> %a"
- (self#term_prec current_level) e (self#term_prec current_level) ce
- | TUpdate (t,toff,v) ->
- fprintf fmt "{%a %a %a = %a}"
- self#term t
- self#pp_acsl_keyword "\\with"
- self#term_offset toff
- self#term v
- | Tlambda(prms,expr) ->
- fprintf fmt "@[<2>%a@ %a;@ %a@]"
- self#pp_acsl_keyword "\\lambda"
- self#quantifiers prms (self#term_prec current_level) expr
- | Ttypeof t ->
- fprintf fmt "%a(%a)" self#pp_acsl_keyword "\\typeof" self#term t
- | Ttype ty ->
- fprintf fmt "%a(%a)" self#pp_acsl_keyword "\\type" (self#typ None) ty
- | Tunion l
- when ((List.for_all (fun t -> not(Logic_const.is_set_type t.term_type)) l)
- && (not state.print_cil_as_is)) ->
- fprintf fmt "{%a}" (Pretty_utils.pp_list ~sep:",@ " self#term) l
- | Tunion locs ->
- fprintf fmt "@[<hov 2>%a(@,%a)@]"
- self#pp_acsl_keyword "\\union"
- (Pretty_utils.pp_list ~sep:",@ " self#term) locs
- | Tinter locs ->
- fprintf fmt "@[<hov 2>%a(@,%a)@]"
- self#pp_acsl_keyword "\\inter"
- (Pretty_utils.pp_list ~sep:",@ " self#term) locs
- | Tempty_set -> self#pp_acsl_keyword fmt "\\empty"
- | Tcomprehension(lv,quant,pred) ->
- fprintf fmt "{@[%a@ |@ %a%a@]}"
- self#term lv self#quantifiers quant
- (Pretty_utils.pp_opt
- (fun fmt p -> fprintf fmt ";@ %a" self#predicate p))
- pred
- | Trange(low,high) ->
- let pp_term = self#term_prec current_level in
- fprintf fmt "@[%a..%a@]"
- (Pretty_utils.pp_opt
- (fun fmt v -> Format.fprintf fmt "%a " pp_term v)) low
- (Pretty_utils.pp_opt
- (fun fmt v -> Format.fprintf fmt "@ %a" pp_term v)) high;
- | Tlet(def,body) ->
- assert
- (Kernel.verify (def.l_labels = [])
- "invalid logic construction: local definition with label");
- assert
- (Kernel.verify (def.l_tparams = [])
- "invalid logic construction: polymorphic local definition");
- let v = def.l_var_info in
- let args = def.l_profile in
- let pp_defn = match def.l_body with
- | LBterm t -> fun fmt -> self#term fmt t
- | LBpred p -> fun fmt -> self#predicate fmt p
- | LBnone
- | LBreads _ | LBinductive _ ->
- Kernel.fatal "invalid logic local definition"
- in
- fprintf fmt "@[%a@ %a@ =@ %t%t;@ %a@]"
- self#pp_acsl_keyword "\\let"
- self#logic_var v
- (fun fmt -> if args <> [] then
- fprintf fmt "@[<2>%a@ %a;@]@ "
- self#pp_acsl_keyword "\\lambda"
- self#quantifiers args)
- pp_defn
- (self#term_prec current_level) body
- | TLogic_coerce(ty,t) ->
- let debug =
- Kernel.is_debug_key_enabled Kernel.dkey_print_logic_coercions
- in
- if debug then
- fprintf fmt "/* (coercion to:%a */" (self#logic_type None) ty;
- self#term_prec current_level fmt t;
- if debug then fprintf fmt "/* ) */"
+ (self#term_prec current_level) cond
+ (self#term_prec current_level) th
+ (self#term_prec current_level) el
+ | Tat (t,lab) ->
+ let old_label = current_label in
+ current_label <- lab;
+ if Cil_datatype.Logic_label.equal lab Logic_const.old_label then
+ fprintf fmt "@[%a(@[%a@])@]" self#pp_acsl_keyword "\\old" self#term t
+ else
+ fprintf fmt "@[%a(@[@[%a@],@,@[%a@]@])@]"
+ self#pp_acsl_keyword "\\at" self#term t self#logic_label lab;
+ current_label <- old_label
+ | Toffset (l,t) ->
+ fprintf fmt "%a%a(%a)" self#pp_acsl_keyword "\\offset"
+ self#labels [l] self#term t
+ | Tbase_addr (l,t) ->
+ fprintf fmt "%a%a(%a)" self#pp_acsl_keyword "\\base_addr"
+ self#labels [l] self#term t
+ | Tblock_length (l,t) ->
+ fprintf fmt "%a%a(%a)" self#pp_acsl_keyword "\\block_length"
+ self#labels [l] self#term t
+ | Tnull -> self#pp_acsl_keyword fmt "\\null"
+ | TCoerce (e,ty) ->
+ fprintf fmt "%a@ :>@ %a"
+ (self#term_prec current_level) e (self#typ None) ty
+ | TCoerceE (e,ce) ->
+ fprintf fmt "%a :> %a"
+ (self#term_prec current_level) e (self#term_prec current_level) ce
+ | TUpdate (t,toff,v) ->
+ fprintf fmt "{%a %a %a = %a}"
+ self#term t
+ self#pp_acsl_keyword "\\with"
+ self#term_offset toff
+ self#term v
+ | Tlambda(prms,expr) ->
+ fprintf fmt "@[<2>%a@ %a;@ %a@]"
+ self#pp_acsl_keyword "\\lambda"
+ self#quantifiers prms (self#term_prec current_level) expr
+ | Ttypeof t ->
+ fprintf fmt "%a(%a)" self#pp_acsl_keyword "\\typeof" self#term t
+ | Ttype ty ->
+ fprintf fmt "%a(%a)" self#pp_acsl_keyword "\\type" (self#typ None) ty
+ | Tunion l
+ when ((List.for_all (fun t -> not(Logic_const.is_set_type t.term_type)) l)
+ && (not state.print_cil_as_is)) ->
+ fprintf fmt "{%a}" (Pretty_utils.pp_list ~sep:",@ " self#term) l
+ | Tunion locs ->
+ fprintf fmt "@[<hov 2>%a(@,%a)@]"
+ self#pp_acsl_keyword "\\union"
+ (Pretty_utils.pp_list ~sep:",@ " self#term) locs
+ | Tinter locs ->
+ fprintf fmt "@[<hov 2>%a(@,%a)@]"
+ self#pp_acsl_keyword "\\inter"
+ (Pretty_utils.pp_list ~sep:",@ " self#term) locs
+ | Tempty_set -> self#pp_acsl_keyword fmt "\\empty"
+ | Tcomprehension(lv,quant,pred) ->
+ fprintf fmt "{@[%a@ |@ %a%a@]}"
+ self#term lv self#quantifiers quant
+ (Pretty_utils.pp_opt
+ (fun fmt p -> fprintf fmt ";@ %a" self#predicate p))
+ pred
+ | Trange(low,high) ->
+ let pp_term = self#term_prec current_level in
+ fprintf fmt "@[%a..%a@]"
+ (Pretty_utils.pp_opt
+ (fun fmt v -> Format.fprintf fmt "%a " pp_term v)) low
+ (Pretty_utils.pp_opt
+ (fun fmt v -> Format.fprintf fmt "@ %a" pp_term v)) high;
+ | Tlet(def,body) ->
+ assert
+ (Kernel.verify (def.l_labels = [])
+ "invalid logic construction: local definition with label");
+ assert
+ (Kernel.verify (def.l_tparams = [])
+ "invalid logic construction: polymorphic local definition");
+ let v = def.l_var_info in
+ let args = def.l_profile in
+ let pp_defn = match def.l_body with
+ | LBterm t -> fun fmt -> self#term fmt t
+ | LBpred p -> fun fmt -> self#predicate fmt p
+ | LBnone
+ | LBreads _ | LBinductive _ ->
+ Kernel.fatal "invalid logic local definition"
+ in
+ fprintf fmt "@[%a@ %a@ =@ %t%t;@ %a@]"
+ self#pp_acsl_keyword "\\let"
+ self#logic_var v
+ (fun fmt -> if args <> [] then
+ fprintf fmt "@[<2>%a@ %a;@]@ "
+ self#pp_acsl_keyword "\\lambda"
+ self#quantifiers args)
+ pp_defn
+ (self#term_prec current_level) body
+ | TLogic_coerce(ty,t) ->
+ let debug =
+ Kernel.is_debug_key_enabled Kernel.dkey_print_logic_coercions
+ in
+ if debug then
+ fprintf fmt "/* (coercion to:%a */" (self#logic_type None) ty;
+ self#term_prec current_level fmt t;
+ if debug then fprintf fmt "/* ) */"
method private term_lval_prec contextprec fmt lv =
if Precedence.getParenthLevelLogic (TLval lv) > contextprec then
@@ -2438,8 +2438,8 @@ class cil_printer () = object (self)
method quantifiers fmt l =
Pretty_utils.pp_list ~sep:",@ "
(fun fmt lv ->
- let pvar fmt = self#logic_var fmt lv in
- self#logic_type (Some pvar) fmt lv.lv_type)
+ let pvar fmt = self#logic_var fmt lv in
+ self#logic_type (Some pvar) fmt lv.lv_type)
fmt l
method private pred_prec fmt (contextprec,p) =
@@ -2453,13 +2453,13 @@ class cil_printer () = object (self)
| [] -> self#pred_prec fmt (parenth,content)
| _ :: _ ->
if parenth = Precedence.upperLevel then
- fprintf fmt "@[<hv 2>%a:@ %a@]"
- (Pretty_utils.pp_list ~sep:":@ " self#name) names
- self#pred_prec (Precedence.upperLevel, content)
+ fprintf fmt "@[<hv 2>%a:@ %a@]"
+ (Pretty_utils.pp_list ~sep:":@ " self#name) names
+ self#pred_prec (Precedence.upperLevel, content)
else
- fprintf fmt "(@[<hv 2>%a:@ %a@])"
- (Pretty_utils.pp_list ~sep:":@ " self#name) names
- self#pred_prec (Precedence.upperLevel, content)
+ fprintf fmt "(@[<hv 2>%a:@ %a@])"
+ (Pretty_utils.pp_list ~sep:":@ " self#name) names
+ self#pred_prec (Precedence.upperLevel, content)
method private pred_prec_named fmt (parenth,p) =
self#named_pred fmt (parenth,p.pred_name,p.pred_content)
@@ -2474,7 +2474,7 @@ class cil_printer () = object (self)
method private preds kw fmt l =
Pretty_utils.pp_list ~suf:"@]@\n" ~sep:"@\n"
(fun fmt p ->
- fprintf fmt "@[%s %a;@]" kw self#identified_predicate p) fmt l
+ fprintf fmt "@[%s %a;@]" kw self#identified_predicate p) fmt l
method private pand_list fmt l =
let term = self#term_prec Precedence.comparativeLevel in
@@ -2517,75 +2517,75 @@ class cil_printer () = object (self)
(if Kernel.Unicode.get () then Utf8_logic.inset else "\\in")
self#term tr
| None ->
- fprintf fmt "@[%a%a%a@]"
- self#logic_info pi
- self#labels labels
- (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@]" ~sep:",@ " self#term) l
- end
+ fprintf fmt "@[%a%a%a@]"
+ self#logic_info pi
+ self#labels labels
+ (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@]" ~sep:",@ " self#term) l
+ end
| Prel (rel,l,r) ->
fprintf fmt "@[%a@ %a@ %a@]" term l self#relation rel term r
| Pand (p1, p2) when not state.print_cil_as_is ->
fprintf fmt "@[%a@]" self#pand_list (get_pand_list p1 [p2])
| Pand (p1,p2) ->
fprintf fmt "@[%a %a@ %a@]"
- self#pred_prec_named (current_level,p1)
- self#term_binop LAnd
- self#pred_prec_named (current_level,p2)
+ self#pred_prec_named (current_level,p1)
+ self#term_binop LAnd
+ self#pred_prec_named (current_level,p2)
| Por (p1, p2) ->
fprintf fmt "@[%a %a@ %a@]"
- self#pred_prec_named (current_level,p1)
- self#term_binop LOr
- self#pred_prec_named (current_level,p2)
+ self#pred_prec_named (current_level,p1)
+ self#term_binop LOr
+ self#pred_prec_named (current_level,p2)
| Pxor (p1, p2) ->
fprintf fmt "@[%a %s@ %a@]"
- self#pred_prec_named (current_level,p1)
- (if Kernel.Unicode.get () then Utf8_logic.x_or else "^^")
- self#pred_prec_named (current_level,p2)
+ self#pred_prec_named (current_level,p1)
+ (if Kernel.Unicode.get () then Utf8_logic.x_or else "^^")
+ self#pred_prec_named (current_level,p2)
| Pimplies (p1,p2) ->
fprintf fmt "@[%a %s@ %a@]"
- self#pred_prec_named (current_level,p1)
- (if Kernel.Unicode.get () then Utf8_logic.implies else "==>")
- self#pred_prec_named (current_level+1,p2)
+ self#pred_prec_named (current_level,p1)
+ (if Kernel.Unicode.get () then Utf8_logic.implies else "==>")
+ self#pred_prec_named (current_level+1,p2)
| Piff (p1,p2) ->
fprintf fmt "@[%a %s@ %a@]"
- self#pred_prec_named (current_level,p1)
- (if Kernel.Unicode.get () then Utf8_logic.iff else "<==>")
- self#pred_prec_named (current_level,p2)
+ self#pred_prec_named (current_level,p1)
+ (if Kernel.Unicode.get () then Utf8_logic.iff else "<==>")
+ self#pred_prec_named (current_level,p2)
| Pnot a -> fprintf fmt "@[%s%a@]"
(if Kernel.Unicode.get () then Utf8_logic.neg else "!")
self#pred_prec_named (current_level,a)
| Pif (e, p1, p2) ->
fprintf fmt "@[<hv 2>%a?@ %a:@ %a@]"
- term e
- self#pred_prec_named (current_level, p1)
- self#pred_prec_named (current_level, p2)
+ term e
+ self#pred_prec_named (current_level, p1)
+ self#pred_prec_named (current_level, p2)
| Plet (def, p) ->
assert
- (Kernel.verify (def.l_labels = [])
- "invalid logic construction: local definition with label");
+ (Kernel.verify (def.l_labels = [])
+ "invalid logic construction: local definition with label");
assert
- (Kernel.verify (def.l_tparams = [])
- "invalid logic construction: polymorphic local definition");
+ (Kernel.verify (def.l_tparams = [])
+ "invalid logic construction: polymorphic local definition");
let v = def.l_var_info in
let args = def.l_profile in
let pp_defn = match def.l_body with
- | LBterm t -> fun fmt -> self#term fmt t
- | LBpred p -> fun fmt -> self#pred_prec_named fmt (current_level,p)
- | LBnone
- | LBreads _ | LBinductive _ ->
- Kernel.fatal "invalid logic local definition"
+ | LBterm t -> fun fmt -> self#term fmt t
+ | LBpred p -> fun fmt -> self#pred_prec_named fmt (current_level,p)
+ | LBnone
+ | LBreads _ | LBinductive _ ->
+ Kernel.fatal "invalid logic local definition"
in
Precedence.needIndent current_level p fmt
"@[<hov 2>%a@ %a =@ %t%t;@]@ %a"
self#pp_acsl_keyword "\\let"
- self#logic_var v
- (fun fmt ->
- if args <> [] then
- fprintf fmt "@[<hv 2>%a@ %a;@]@ "
+ self#logic_var v
+ (fun fmt ->
+ if args <> [] then
+ fprintf fmt "@[<hv 2>%a@ %a;@]@ "
self#pp_acsl_keyword "\\lambda"
self#quantifiers args)
- pp_defn
- self#pred_prec_named (current_level,p)
+ pp_defn
+ self#pred_prec_named (current_level,p)
| Pforall (quant,pred) ->
Precedence.needIndent current_level pred fmt
"@[%t %a;@]@ %a"
@@ -2631,22 +2631,22 @@ class cil_printer () = object (self)
| Pfresh (l1,l2,e1,e2) ->
fprintf fmt "@[%a%a(@[%a@],@[%a@])@]"
self#pp_acsl_keyword "\\fresh"
- self#labels [l1;l2] self#term e1 self#term e2
+ self#labels [l1;l2] self#term e1 self#term e2
| Pseparated seps ->
fprintf fmt "@[<hv 2>%a(@,%a@,)@]"
self#pp_acsl_keyword "\\separated"
- (Pretty_utils.pp_list ~sep:",@ " self#term) seps
+ (Pretty_utils.pp_list ~sep:",@ " self#term) seps
| Pat(p,lab) ->
let old_label = current_label in
current_label <- lab;
if Cil_datatype.Logic_label.equal lab Logic_const.old_label then
- fprintf fmt "@[%a(@[%a@])@]"
+ fprintf fmt "@[%a(@[%a@])@]"
self#pp_acsl_keyword "\\old"
- self#pred_prec_named (Precedence.upperLevel,p)
+ self#pred_prec_named (Precedence.upperLevel,p)
else
- fprintf fmt "@[%a(@[@[%a@],@,%a@])@]"
+ fprintf fmt "@[%a(@[@[%a@],@,%a@])@]"
self#pp_acsl_keyword "\\at"
- self#pred_prec_named (Precedence.upperLevel,p)
+ self#pred_prec_named (Precedence.upperLevel,p)
self#logic_label lab;
current_label <- old_label
| Psubtype (e,ce) ->
@@ -2700,19 +2700,19 @@ class cil_printer () = object (self)
method allocation ~isloop fmt = function
| FreeAllocAny -> ()
- | FreeAlloc([],[]) ->
+ | FreeAlloc([],[]) ->
fprintf fmt "@[%a@ %a;@]"
self#pp_acsl_keyword (if isloop then "loop allocates" else "allocates")
self#pp_acsl_keyword "\\nothing"
| FreeAlloc(f,a) ->
let pFreeAlloc kw fmt = function
| [] -> ()
- | _ :: _ as af ->
- fprintf fmt "@[%a@ %a;@]"
- self#pp_acsl_keyword (if isloop then "loop "^kw else kw)
- (Pretty_utils.pp_list ~sep:",@ " self#identified_term) af
+ | _ :: _ as af ->
+ fprintf fmt "@[%a@ %a;@]"
+ self#pp_acsl_keyword (if isloop then "loop "^kw else kw)
+ (Pretty_utils.pp_list ~sep:",@ " self#identified_term) af
in
- fprintf fmt "@[<v>%a%(%)%a@]"
+ fprintf fmt "@[<v>%a%(%)%a@]"
(pFreeAlloc "frees") f
(if f != [] && a != [] then format_of_string "@ " else "")
(pFreeAlloc "allocates") a
@@ -2724,14 +2724,14 @@ class cil_printer () = object (self)
| Writes l ->
let without_result =
List.filter
- (function (a,_) -> not (Logic_const.is_exit_status a.it_content))
+ (function (a,_) -> not (Logic_const.is_exit_status a.it_content))
l
in
fprintf fmt "@[<h>%t%a@]"
(fun fmt -> if without_result <> [] then
Format.fprintf fmt "%a " self#pp_acsl_keyword kw)
(Pretty_utils.pp_list ~sep:",@ " ~suf:";@]"
- (fun fmt (t, _) -> self#identified_term fmt t))
+ (fun fmt (t, _) -> self#identified_term fmt t))
without_result
method private assigns_deps kw fmt = function
@@ -2746,7 +2746,7 @@ class cil_printer () = object (self)
method from kw fmt (base,deps) = match deps with
| FromAny -> ()
| From [] ->
- fprintf fmt "@[<hv 2>@[<h>%a@ %a@]@ @[<h>%a %a@];@]"
+ fprintf fmt "@[<hv 2>@[<h>%a@ %a@]@ @[<h>%a %a@];@]"
self#pp_acsl_keyword kw
self#identified_term base
self#pp_acsl_keyword "\\from"
@@ -2761,17 +2761,17 @@ class cil_printer () = object (self)
(* not enclosed in a box *)
method private terminates_decreases ~extra_nl nl fmt (terminates, variant) =
let nl_terminates = nl || variant != None in
- let pp_opt nl fmt =
+ let pp_opt nl fmt =
let suf = if nl then format_of_string "@]@\n" else "@]" in
- Pretty_utils.pp_opt ~suf fmt
+ Pretty_utils.pp_opt ~suf fmt
in
fprintf fmt "%a%a%(%)"
(pp_opt nl_terminates self#terminates) terminates
(pp_opt nl self#decreases) variant
- (format_of_string
- (if extra_nl && nl && (variant != None || terminates != None)
- then format_of_string "@\n"
- else ""))
+ (format_of_string
+ (if extra_nl && nl && (variant != None || terminates != None)
+ then format_of_string "@\n"
+ else ""))
(* not enclosed in a box *)
method private behavior_contents ~extra_nl nl ?terminates ?variant fmt b =
@@ -2813,22 +2813,22 @@ class cil_printer () = object (self)
self#pp_acsl_keyword "behavior"
b.b_name
(self#behavior_contents ~extra_nl:false false
- ?terminates:None ?variant:None)
+ ?terminates:None ?variant:None)
b
method funspec fmt ({ spec_behavior = behaviors;
- spec_variant = variant;
- spec_terminates = terminates;
- spec_complete_behaviors = complete;
- spec_disjoint_behaviors = disjoint } as spec) =
- let pp_list ?(extra_nl=false) nl fmt =
- let suf =
+ spec_variant = variant;
+ spec_terminates = terminates;
+ spec_complete_behaviors = complete;
+ spec_disjoint_behaviors = disjoint } as spec) =
+ let pp_list ?(extra_nl=false) nl fmt =
+ let suf =
if nl then
if extra_nl then format_of_string "@]@\n@\n" else "@]@\n"
else "@]"
in
let sep = if extra_nl then format_of_string "@\n@\n" else "@\n" in
- Pretty_utils.pp_list ~pre:"@[<v>" ~sep ~suf fmt
+ Pretty_utils.pp_list ~pre:"@[<v>" ~sep ~suf fmt
in
fprintf fmt "@[<v>";
let default_bhv = Cil.find_default_behavior spec in
@@ -2839,31 +2839,31 @@ class cil_printer () = object (self)
let nl_other_bhvs = nl_complete || complete != [] in
let nl_default = nl_other_bhvs || other_bhvs != [] in
(match default_bhv with
- | None ->
+ | None ->
self#terminates_decreases ~extra_nl:nl_default nl_default fmt
- (terminates, variant)
+ (terminates, variant)
| Some b
when b.b_assumes == [] && b.b_requires == [] && b.b_post_cond == []
- && b.b_extended == []
- && b.b_allocation == FreeAllocAny && b.b_assigns == WritesAny ->
+ && b.b_extended == []
+ && b.b_allocation == FreeAllocAny && b.b_assigns == WritesAny ->
self#terminates_decreases ~extra_nl:nl_default nl_default fmt
- (terminates, variant)
- | Some b ->
- self#behavior_contents
- ~extra_nl:nl_default nl_default ?terminates ?variant fmt b);
+ (terminates, variant)
+ | Some b ->
+ self#behavior_contents
+ ~extra_nl:nl_default nl_default ?terminates ?variant fmt b);
fprintf fmt "%a%a%a@]"
(pp_list ~extra_nl:true nl_other_bhvs self#behavior) other_bhvs
(pp_list nl_complete self#complete_behaviors) complete
(pp_list false self#disjoint_behaviors) disjoint
method private loop_pragma fmt = function
- | Widen_hints terms ->
+ | Widen_hints terms ->
fprintf fmt "WIDEN_HINTS @[%a@]"
(Pretty_utils.pp_list ~sep:",@ " self#term) terms
- | Widen_variables terms ->
+ | Widen_variables terms ->
fprintf fmt "WIDEN_VARIABLES @[%a@]"
(Pretty_utils.pp_list ~sep:",@ " self#term) terms
- | Unroll_specs terms ->
+ | Unroll_specs terms ->
fprintf fmt "UNROLL @[%a@]"
(Pretty_utils.pp_list ~sep:",@ " self#term) terms
@@ -2877,7 +2877,7 @@ class cil_printer () = object (self)
| IPstmt -> Format.pp_print_string fmt "stmt"
(* TODO: add the annot ID in debug mode?*)
- method code_annotation fmt ca =
+ method code_annotation fmt ca =
let pp_for_behavs fmt l =
match l with
| [] -> ()
@@ -2960,9 +2960,9 @@ class cil_printer () = object (self)
| FormalLabel s -> pp_print_string fmt s
| StmtLabel sref ->
let rec pickLabel = function
- | [] -> None
- | Label (l, _, _) :: _ -> Some l
- | _ :: rest -> pickLabel rest
+ | [] -> None
+ | Label (l, _, _) :: _ -> Some l
+ | _ :: rest -> pickLabel rest
in
let s = match pickLabel !sref.labels with
| Some l -> l
@@ -2971,14 +2971,14 @@ class cil_printer () = object (self)
pp_print_string fmt s
method private labels fmt labels =
- match labels with
+ match labels with
| [ l ] when
- Cil_datatype.Logic_label.equal current_label l
+ Cil_datatype.Logic_label.equal current_label l
&& not state.print_cil_as_is
-> ()
| _ ->
Pretty_utils.pp_list ~pre:"{@[" ~suf:"@]}" ~sep:",@ "
- self#logic_label fmt labels
+ self#logic_label fmt labels
method model_info fmt mfi =
let print_decl fmt = self#model_field fmt mfi in
@@ -2994,8 +2994,8 @@ class cil_printer () = object (self)
fprintf fmt "@[<hv 2>@[%a %a%a=@]@ %a;@]@\n"
self#pp_acsl_keyword "type invariant"
self#logic_var a.l_var_info
- (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@] " ~sep:",@ "
- self#logicPrms) a.l_profile
+ (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@] " ~sep:",@ "
+ self#logicPrms) a.l_profile
self#predicate (pred_body a.l_body);
current_label <- old_label
| Dmodel_annot (mfi,_) ->
@@ -3041,7 +3041,7 @@ class cil_printer () = object (self)
| Some rt ->
fprintf fmt "@[<hov 2>@[%a %a"
self#pp_acsl_keyword "logic"
- (self#logic_type None) rt
+ (self#logic_type None) rt
| None ->
(match li.l_body with
| LBinductive _ ->
@@ -3054,7 +3054,7 @@ class cil_printer () = object (self)
self#labels li.l_labels
self#polyTypePrms li.l_tparams
(Pretty_utils.pp_list ~pre:"@[(" ~suf:")@] " ~sep:",@ "
- self#logicPrms)
+ self#logicPrms)
li.l_profile;
(* Except for inductive definitions, where this must be done for
each individual case that declare a unique label, if the predicate
@@ -3070,15 +3070,15 @@ class cil_printer () = object (self)
fprintf fmt "@]@\n@[%a %a;@]"
self#pp_acsl_keyword "reads" self#pp_acsl_keyword "\\nothing"
| _ ->
- fprintf fmt "@]@\n@[%a@ %a;@]"
+ fprintf fmt "@]@\n@[%a@ %a;@]"
self#pp_acsl_keyword "reads"
- (Pretty_utils.pp_list
- ~sep:",@ "
- (fun fmt x -> self#term fmt x.it_content)) reads)
+ (Pretty_utils.pp_list
+ ~sep:",@ "
+ (fun fmt x -> self#term fmt x.it_content)) reads)
| LBpred def ->
(match li.l_labels with | [ l ] -> current_label <- l | _ -> ());
fprintf fmt "=@]@ %a;"
- self#predicate def
+ self#predicate def
| LBinductive indcases ->
fprintf fmt "{@]@ %a}"
(Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
@@ -3097,7 +3097,7 @@ class cil_printer () = object (self)
| LBterm def ->
(match li.l_labels with | [ l ] -> current_label <- l | _ -> ());
fprintf fmt "=@]@ %a;"
- self#term def);
+ self#term def);
fprintf fmt "@]@\n";
current_label <- old_lab
| Dvolatile(tsets,rvi_opt,wvi_opt,_attr, _) ->
@@ -3109,7 +3109,7 @@ class cil_printer () = object (self)
fprintf fmt "@[<hov 2>%a@ %a%a%a;@]"
self#pp_acsl_keyword "volatile"
(Pretty_utils.pp_list ~sep:",@ "
- (fun fmt x -> self#term fmt x.it_content))
+ (fun fmt x -> self#term fmt x.it_content))
tsets
(pp_vol "reads") rvi_opt
(pp_vol "writes") wvi_opt ;
@@ -3119,7 +3119,7 @@ class cil_printer () = object (self)
self#pp_acsl_keyword "axiomatic"
id
(Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
- self#global_annotation)
+ self#global_annotation)
decls
| Dextended (e,_attr,_) -> self#extended fmt e
@@ -3127,10 +3127,10 @@ class cil_printer () = object (self)
| LTsum l ->
Pretty_utils.pp_list ~sep:"@ |@ "
(fun fmt info ->
- fprintf fmt "%s@[%a@]" info.ctor_name
- (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@]" ~sep:",@ "
- (self#logic_type None)) info.ctor_params) fmt l
- | LTsyn typ ->
+ fprintf fmt "%s@[%a@]" info.ctor_name
+ (Pretty_utils.pp_list ~pre:"@[(" ~suf:")@]" ~sep:",@ "
+ (self#logic_type None)) info.ctor_params) fmt l
+ | LTsyn typ ->
self#logic_type None fmt typ
method file fmt file =
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 1eb890808ea..3edbd8bc09e 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -41,7 +41,7 @@ val register_behavior_extension:
Cil_types.acsl_extension_kind -> unit) -> unit
(** Register a pretty-printer used for behavior extension.
@plugin development guide
- *)
+*)
val register_global_extension:
string ->
@@ -49,7 +49,7 @@ val register_global_extension:
Cil_types.acsl_extension_kind -> unit) -> unit
(** Register a pretty-printer used for behavior extension.
@plugin development guide
- *)
+*)
val register_code_annot_extension:
string ->
@@ -57,7 +57,7 @@ val register_code_annot_extension:
Cil_types.acsl_extension_kind -> unit) -> unit
(** Register a pretty-printer used for behavior extension.
@plugin development guide
- *)
+*)
val register_loop_annot_extension:
string ->
@@ -65,7 +65,7 @@ val register_loop_annot_extension:
Cil_types.acsl_extension_kind -> unit) -> unit
(** Register a pretty-printer used for behavior extension.
@plugin development guide
- *)
+*)
val state: Printer_api.state
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 8a0c8c33b31..b4f7c0431b2 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -34,7 +34,7 @@ let print_locations = false
(* compinfo, fieldinfo, enuminfo, typeinfo and varinfo are shortened by default.
Setting several to true may result in infinite mutually recursive calls!
- *)
+*)
let print_full_compinfo = false
let print_full_fieldinfo = false
let print_full_enuminfo = false
@@ -413,9 +413,9 @@ and pp_exp_node fmt = function
| Info(exp,exp_info) -> Format.fprintf fmt "Info(%a,%a)" pp_exp exp pp_exp_info exp_info
and pp_exp_info fmt _exp_info = Format.fprintf fmt "pp_exp_info_TODO" (*{
- exp_type : logic_type;
- exp_name: string_list;
-}*)
+ exp_type : logic_type;
+ exp_name: string_list;
+ }*)
and pp_constant fmt = function
| CInt64(integer,ikind,string_option) ->
@@ -476,21 +476,21 @@ and pp_init fmt = function
and pp_initinfo fmt _initinfo = Format.fprintf fmt "pp_initinfo_TODO" (*{ mutable init : init_option }*)
and pp_fundec fmt _fundec = Format.fprintf fmt "pp_fundec_TODO" (*{
- mutable svar: varinfo;
- mutable sformals: varinfo_list;
- mutable slocals: varinfo_list;
- mutable smaxid: int;
- mutable sbody: block;
- mutable smaxstmtid: int_option;
- mutable sallstmts: stmt_list;
- mutable sspec: funspec;
-}*)
+ mutable svar: varinfo;
+ mutable sformals: varinfo_list;
+ mutable slocals: varinfo_list;
+ mutable smaxid: int;
+ mutable sbody: block;
+ mutable smaxstmtid: int_option;
+ mutable sallstmts: stmt_list;
+ mutable sspec: funspec;
+ }*)
and pp_block fmt _block = Format.fprintf fmt "pp_block_TODO" (*{
- mutable battrs: attributes;
- mutable blocals: varinfo_list;
- mutable bstmts: stmt_list;
-}*)
+ mutable battrs: attributes;
+ mutable blocals: varinfo_list;
+ mutable bstmts: stmt_list;
+ }*)
and pp_stmt fmt stmt = Format.fprintf fmt
"{sid=%a;labels=%a;skind=%a;ghost=%a;TODO}"
@@ -570,12 +570,12 @@ and pp_instr fmt = function
Format.fprintf fmt "Local_init(%a,%a,%a)" pp_varinfo vi pp_local_init i pp_location location
and pp_extended_asm fmt _extended_asm = Format.fprintf fmt "pp_extended_asm_TODO" (*{
- {
- asm_outputs: (string_option * string * lval)_list;
- asm_inputs: (string_option * string * exp)_list;
- asm_clobbers: string_list;
- asm_gotos: (stmt ref)_list;
-}*)
+ {
+ asm_outputs: (string_option * string * lval)_list;
+ asm_inputs: (string_option * string * exp)_list;
+ asm_clobbers: string_list;
+ asm_gotos: (stmt ref)_list;
+ }*)
and pp_filepath_position fmt filepath_position =
Format.fprintf fmt "{pos_path=%s;pos_lnum=%d;pos_bol=%d;pos_cnum=%d}"
@@ -606,11 +606,11 @@ and pp_logic_constant fmt = function
| LEnum(enumitem) -> Format.fprintf fmt "LEnum(%a)" pp_enumitem enumitem
and pp_logic_real fmt _logic_real = Format.fprintf fmt "pp_logic_real_TODO" (*{
- r_literal : string ;
- r_nearest : float ;
- r_upper : float ;
- r_lower : float ;
-}*)
+ r_literal : string ;
+ r_nearest : float ;
+ r_upper : float ;
+ r_lower : float ;
+ }*)
and pp_logic_type fmt = function
| Ctype(typ) -> Format.fprintf fmt "Ctype(%a)" pp_typ typ
@@ -710,13 +710,13 @@ and pp_term_lhost fmt = function
| TMem(term) -> Format.fprintf fmt "TMem(%a)" pp_term term
and pp_model_info fmt _model_info = Format.fprintf fmt "pp_model_info_TODO" (*{
- mi_name: string;
- mi_field_type: logic_type;
- mi_base_type: typ;
- mi_decl: location;
- mutable mi_attr: attributes;
+ mi_name: string;
+ mi_field_type: logic_type;
+ mi_base_type: typ;
+ mi_decl: location;
+ mutable mi_attr: attributes;
-}*)
+ }*)
and pp_term_offset fmt = function
| TNoOffset -> Format.fprintf fmt "TNoOffset"
@@ -740,15 +740,15 @@ and pp_logic_info fmt logic_info =
mutable l_type : logic_type_option;
mutable l_profile : logic_var_list;
mutable l_body : logic_body;
-}*)
+ }*)
and pp_builtin_logic_info fmt _builtin_logic_info = Format.fprintf fmt "pp_builtin_logic_info_TODO" (*{
- mutable bl_name: string;
- mutable bl_labels: logic_label_list;
- mutable bl_params: string_list;
- mutable bl_type: logic_type_option;
- mutable bl_profile: (string * logic_type)_list;
-}*)
+ mutable bl_name: string;
+ mutable bl_labels: logic_label_list;
+ mutable bl_params: string_list;
+ mutable bl_type: logic_type_option;
+ mutable bl_profile: (string * logic_type)_list;
+ }*)
and pp_logic_body fmt = function
| LBnone -> Format.fprintf fmt "LBnone"
@@ -789,7 +789,7 @@ and pp_logic_var fmt logic_var =
mutable lv_kind: logic_var_kind;
mutable lv_origin : varinfo_option;
mutable lv_attr: attributes
-}*)
+ }*)
and pp_logic_ctor_info fmt logic_ctor_info =
Format.fprintf fmt "{ctor_name=%a;ctor_type=TODO;ctor_params=%a}"
@@ -860,7 +860,7 @@ and pp_predicate_node fmt = function
Format.fprintf fmt "Pfresh(%a,%a,%a,%a)" pp_logic_label logic_label1 pp_logic_label logic_label2
pp_term term1 pp_term term2
| Psubtype(term1,term2) ->
- Format.fprintf fmt "Psubtype(%a,%a)" pp_term term1 pp_term term2
+ Format.fprintf fmt "Psubtype(%a,%a)" pp_term term1 pp_term term2
and pp_identified_predicate fmt identified_predicate =
Format.fprintf fmt "{ip_id=%d;ip_content=%a}"
@@ -872,12 +872,12 @@ and pp_predicate fmt predicate = Format.fprintf fmt "{%a%apred_content=%a}"
pp_predicate_node predicate.pred_content
and pp_spec fmt _spec = Format.fprintf fmt "pp_spec_TODO" (*{
- mutable spec_behavior : behavior_list;
- mutable spec_variant : term variant_option;
- mutable spec_terminates: identified_predicate_option;
- mutable spec_complete_behaviors: string_list_list;
- mutable spec_disjoint_behaviors: string_list_list;
-}*)
+ mutable spec_behavior : behavior_list;
+ mutable spec_variant : term variant_option;
+ mutable spec_terminates: identified_predicate_option;
+ mutable spec_complete_behaviors: string_list_list;
+ mutable spec_disjoint_behaviors: string_list_list;
+ }*)
and pp_acsl_extension fmt = pp_tuple4 pp_int pp_string pp_location pp_acsl_extension_kind fmt
@@ -887,14 +887,14 @@ and pp_acsl_extension_kind fmt = function
| Ext_preds(predicate_list) -> Format.fprintf fmt "Ext_preds(%a)" (pp_list pp_predicate) predicate_list
and pp_behavior fmt _behavior = Format.fprintf fmt "pp_behavior_TODO" (*{
- mutable b_name : string;
- mutable b_requires : identified_predicate_list;
- mutable b_assumes : identified_predicate_list;
- mutable b_post_cond : (termination_kind * identified_predicate)_list;
- mutable b_assigns : assigns;
- mutable b_allocation : allocation;
- mutable b_extended : acsl_extension_list
-}*)
+ mutable b_name : string;
+ mutable b_requires : identified_predicate_list;
+ mutable b_assumes : identified_predicate_list;
+ mutable b_post_cond : (termination_kind * identified_predicate)_list;
+ mutable b_assigns : assigns;
+ mutable b_allocation : allocation;
+ mutable b_extended : acsl_extension_list
+ }*)
and pp_termination_kind fmt = function
| Normal -> Format.fprintf fmt "Normal"
@@ -946,9 +946,9 @@ and pp_code_annotation_node fmt = function
and pp_funspec fmt _funspec = Format.fprintf fmt "pp_funspec_TODO"
and pp_code_annotation fmt _code_annotation = Format.fprintf fmt "pp_code_annotation_TODO" (*{
- annot_id: int;
- annot_content : code_annotation_node;
-}*)
+ annot_id: int;
+ annot_content : code_annotation_node;
+ }*)
and pp_funbehavior fmt = pp_behavior fmt
@@ -998,9 +998,9 @@ let pp_cil_function fmt = function
(pp_option (pp_list pp_varinfo)) varinfo_list_option pp_location location
let pp_kernel_function fmt _kernel_function = Format.fprintf fmt "pp_kernel_function_TODO" (*{
- mutable fundec : cil_function;
- mutable spec : funspec;
-}*)
+ mutable fundec : cil_function;
+ mutable spec : funspec;
+ }*)
let pp_localisation fmt = function
| VGlobal -> Format.fprintf fmt "VGlobal"
@@ -1008,37 +1008,37 @@ let pp_localisation fmt = function
| VFormal(kernel_function) -> Format.fprintf fmt "VFormal(%a)" pp_kernel_function kernel_function
let pp_mach fmt _mach = Format.fprintf fmt "pp_mach_TODO" (*{
- sizeof_short: int;
- sizeof_int: int;
- sizeof_long: int ;
- sizeof_longlong: int;
- sizeof_ptr: int;
- sizeof_float: int;
- sizeof_double: int;
- sizeof_longdouble: int;
- sizeof_void: int;
- sizeof_fun: int;
- size_t: string;
- wchar_t: string;
- ptrdiff_t: string;
- alignof_short: int;
- alignof_int: int;
- alignof_long: int;
- alignof_longlong: int;
- alignof_ptr: int;
- alignof_float: int;
- alignof_double: int;
- alignof_longdouble: int;
- alignof_str: int;
- alignof_fun: int;
- char_is_unsigned: bool;
- underscore_name: bool;
- const_string_literals: bool;
- little_endian: bool;
- alignof_aligned: int;
- has__builtin_va_list: bool;
- __thread_is_keyword: bool;
- compiler: string;
- cpp_arch_flags: string_list;
- version: string;
-}*)
+ sizeof_short: int;
+ sizeof_int: int;
+ sizeof_long: int ;
+ sizeof_longlong: int;
+ sizeof_ptr: int;
+ sizeof_float: int;
+ sizeof_double: int;
+ sizeof_longdouble: int;
+ sizeof_void: int;
+ sizeof_fun: int;
+ size_t: string;
+ wchar_t: string;
+ ptrdiff_t: string;
+ alignof_short: int;
+ alignof_int: int;
+ alignof_long: int;
+ alignof_longlong: int;
+ alignof_ptr: int;
+ alignof_float: int;
+ alignof_double: int;
+ alignof_longdouble: int;
+ alignof_str: int;
+ alignof_fun: int;
+ char_is_unsigned: bool;
+ underscore_name: bool;
+ const_string_literals: bool;
+ little_endian: bool;
+ alignof_aligned: int;
+ has__builtin_va_list: bool;
+ __thread_is_keyword: bool;
+ compiler: string;
+ cpp_arch_flags: string_list;
+ version: string;
+ }*)
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index e8b52c76c1c..e6cca0530b1 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -169,4 +169,3 @@ val pp_cil_function : Format.formatter -> Cil_types.cil_function -> unit
val pp_kernel_function : Format.formatter -> 'a -> unit
val pp_localisation : Format.formatter -> Cil_types.localisation -> unit
val pp_mach : Format.formatter -> 'a -> unit
-
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index d3240945dbc..f8169bee15b 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -42,25 +42,25 @@
(****************************************************************************)
(* cprint -- pretty printer of C program from abstract syntax
-**
-** Project: FrontC
-** File: cprint.ml
-** Version: 2.1e
-** Date: 9.1.99
-** Author: Hugues Cassé
-**
-** 1.0 2.22.99 Hugues Cassé First version.
-** 2.0 3.18.99 Hugues Cassé Compatible with Frontc 2.1, use of CAML
-** pretty printer.
-** 2.1 3.22.99 Hugues Cassé More efficient custom pretty printer used.
-** 2.1a 4.12.99 Hugues Cassé Correctly handle:
-** char *m, *m, *p; m + (n - p)
-** 2.1b 4.15.99 Hugues Cassé x + (y + z) stays x + (y + z) for
-** keeping computation order.
-** 2.1c 7.23.99 Hugues Cassé Improvement of case and default display.
-** 2.1d 8.25.99 Hugues Cassé Rebuild escape sequences in string and
-** characters.
-** 2.1e 9.1.99 Hugues Cassé Fix, recognize and correctly display '\0'.
+ **
+ ** Project: FrontC
+ ** File: cprint.ml
+ ** Version: 2.1e
+ ** Date: 9.1.99
+ ** Author: Hugues Cassé
+ **
+ ** 1.0 2.22.99 Hugues Cassé First version.
+ ** 2.0 3.18.99 Hugues Cassé Compatible with Frontc 2.1, use of CAML
+ ** pretty printer.
+ ** 2.1 3.22.99 Hugues Cassé More efficient custom pretty printer used.
+ ** 2.1a 4.12.99 Hugues Cassé Correctly handle:
+ ** char *m, *m, *p; m + (n - p)
+ ** 2.1b 4.15.99 Hugues Cassé x + (y + z) stays x + (y + z) for
+ ** keeping computation order.
+ ** 2.1c 7.23.99 Hugues Cassé Improvement of case and default display.
+ ** 2.1d 8.25.99 Hugues Cassé Rebuild escape sequences in string and
+ ** characters.
+ ** 2.1e 9.1.99 Hugues Cassé Fix, recognize and correctly display '\0'.
*)
(* George Necula: I changed this pretty dramatically since CABS changed *)
@@ -82,24 +82,24 @@ let printComments = ref false
(*
** Expression printing
-** Priorities
-** 16 variables
-** 15 . -> [] call()
-** 14 ++, -- (post)
-** 13 ++ -- (pre) ~ ! - + & *(cast)
-** 12 * / %
-** 11 + -
-** 10 << >>
-** 9 < <= > >=
-** 8 == !=
-** 7 &
-** 6 ^
-** 5 |
-** 4 &&
-** 3 ||
-** 2 ? :
-** 1 = ?=
-** 0 ,
+** Priorities
+** 16 variables
+** 15 . -> [] call()
+** 14 ++, -- (post)
+** 13 ++ -- (pre) ~ ! - + & *(cast)
+** 12 * / %
+** 11 + -
+** 10 << >>
+** 9 < <= > >=
+** 8 == !=
+** 7 &
+** 6 ^
+** 5 |
+** 4 &&
+** 3 ||
+** 2 ? :
+** 1 = ?=
+** 0 ,
*)
let cast_level = 13
@@ -109,49 +109,49 @@ let get_operator exp =
NOTHING -> ("", 16)
| PAREN _ -> ("", 16)
| UNARY (op, _) ->
- (match op with
- MINUS -> ("-", 13)
- | PLUS -> ("+", 13)
- | NOT -> ("!", 13)
- | BNOT -> ("~", 13)
- | MEMOF -> ("*", 13)
- | ADDROF -> ("&", 13)
- | PREINCR -> ("++", 13)
- | PREDECR -> ("--", 13)
- | POSINCR -> ("++", 14)
- | POSDECR -> ("--", 14))
+ (match op with
+ MINUS -> ("-", 13)
+ | PLUS -> ("+", 13)
+ | NOT -> ("!", 13)
+ | BNOT -> ("~", 13)
+ | MEMOF -> ("*", 13)
+ | ADDROF -> ("&", 13)
+ | PREINCR -> ("++", 13)
+ | PREDECR -> ("--", 13)
+ | POSINCR -> ("++", 14)
+ | POSDECR -> ("--", 14))
| LABELADDR _ -> ("", 16) (* Like a constant *)
| BINARY (op, _, _) ->
- (match op with
- MUL -> ("*", 12)
- | DIV -> ("/", 12)
- | MOD -> ("%", 12)
- | ADD -> ("+", 11)
- | SUB -> ("-", 11)
- | SHL -> ("<<", 10)
- | SHR -> (">>", 10)
- | LT -> ("<", 9)
- | LE -> ("<=", 9)
- | GT -> (">", 9)
- | GE -> (">=", 9)
- | EQ -> ("==", 8)
- | NE -> ("!=", 8)
- | BAND -> ("&", 7)
- | XOR -> ("^", 6)
- | BOR -> ("|", 5)
- | AND -> ("&&", 4)
- | OR -> ("||", 3)
- | ASSIGN -> ("=", 1)
- | ADD_ASSIGN -> ("+=", 1)
- | SUB_ASSIGN -> ("-=", 1)
- | MUL_ASSIGN -> ("*=", 1)
- | DIV_ASSIGN -> ("/=", 1)
- | MOD_ASSIGN -> ("%=", 1)
- | BAND_ASSIGN -> ("&=", 1)
- | BOR_ASSIGN -> ("|=", 1)
- | XOR_ASSIGN -> ("^=", 1)
- | SHL_ASSIGN -> ("<<=", 1)
- | SHR_ASSIGN -> (">>=", 1))
+ (match op with
+ MUL -> ("*", 12)
+ | DIV -> ("/", 12)
+ | MOD -> ("%", 12)
+ | ADD -> ("+", 11)
+ | SUB -> ("-", 11)
+ | SHL -> ("<<", 10)
+ | SHR -> (">>", 10)
+ | LT -> ("<", 9)
+ | LE -> ("<=", 9)
+ | GT -> (">", 9)
+ | GE -> (">=", 9)
+ | EQ -> ("==", 8)
+ | NE -> ("!=", 8)
+ | BAND -> ("&", 7)
+ | XOR -> ("^", 6)
+ | BOR -> ("|", 5)
+ | AND -> ("&&", 4)
+ | OR -> ("||", 3)
+ | ASSIGN -> ("=", 1)
+ | ADD_ASSIGN -> ("+=", 1)
+ | SUB_ASSIGN -> ("-=", 1)
+ | MUL_ASSIGN -> ("*=", 1)
+ | DIV_ASSIGN -> ("/=", 1)
+ | MOD_ASSIGN -> ("%=", 1)
+ | BAND_ASSIGN -> ("&=", 1)
+ | BOR_ASSIGN -> ("|=", 1)
+ | XOR_ASSIGN -> ("^=", 1)
+ | SHL_ASSIGN -> ("<<=", 1)
+ | SHR_ASSIGN -> (">>=", 1))
| QUESTION _ -> ("", 2)
| CAST _ -> ("", cast_level)
| CALL _ -> ("", 15)
@@ -214,46 +214,46 @@ and print_type_spec fmt = function
| Tnamed s -> fprintf fmt "%s" s
| Tstruct (n, None, _) -> fprintf fmt "struct %s" n
| Tstruct (n, Some flds, extraAttrs) ->
- fprintf fmt "@[<hov 2>%a@ {@ %a@;}@]"
- (print_struct_name_attr "struct") (n, extraAttrs) print_fields flds
+ fprintf fmt "@[<hov 2>%a@ {@ %a@;}@]"
+ (print_struct_name_attr "struct") (n, extraAttrs) print_fields flds
| Tunion (n, None, _) -> fprintf fmt "union %s" n
| Tunion (n, Some flds, extraAttrs) ->
- fprintf fmt "@[<hov 2>%a@ {@ %a@;}@]"
- (print_struct_name_attr "union") (n, extraAttrs) print_fields flds
+ fprintf fmt "@[<hov 2>%a@ {@ %a@;}@]"
+ (print_struct_name_attr "union") (n, extraAttrs) print_fields flds
| Tenum (n, None, _) -> fprintf fmt "enum %s" n
| Tenum (n, Some enum_items, extraAttrs) ->
- fprintf fmt "@[<hov 2>%a@ {@ %a@;}@]"
- (print_struct_name_attr "enum") (n, extraAttrs)
- print_enum_items enum_items
+ fprintf fmt "@[<hov 2>%a@ {@ %a@;}@]"
+ (print_struct_name_attr "enum") (n, extraAttrs)
+ print_enum_items enum_items
| TtypeofE e -> fprintf fmt "__typeof__(@[%a@])" print_expression e
| TtypeofT (s,d) ->
- fprintf fmt "__typeof__(@[%a@])"print_onlytype (s, d)
+ fprintf fmt "__typeof__(@[%a@])"print_onlytype (s, d)
(* print "struct foo", but with specified keyword and a list of
* attributes to put between keyword and name *)
and print_struct_name_attr keyword fmt (name, extraAttrs) =
- fprintf fmt "%s%a%a@ %s"
- keyword
- (pp_cond (extraAttrs <> [])) "@ "
- print_attributes extraAttrs name
+ fprintf fmt "%s%a%a@ %s"
+ keyword
+ (pp_cond (extraAttrs <> [])) "@ "
+ print_attributes extraAttrs name
(* This is the main printer for declarations. It is easy because the
* declarations are laid out as they need to be printed. *)
and print_decl (n: string) fmt = function
JUSTBASE ->
- let cond = n = "___missing_field_name" in
- fprintf fmt "%a%s%a" (pp_cond cond) "/*@ " n (pp_cond cond) "@ */"
+ let cond = n = "___missing_field_name" in
+ fprintf fmt "%a%s%a" (pp_cond cond) "/*@ " n (pp_cond cond) "@ */"
| PARENTYPE (al1, d, al2) ->
- fprintf fmt "(@[%a%a%a@])"
- print_attributes al1 (print_decl n) d print_attributes al2
+ fprintf fmt "(@[%a%a%a@])"
+ print_attributes al1 (print_decl n) d print_attributes al2
| PTR (al, d) ->
- fprintf fmt "*%a%a" print_attributes al (print_decl n) d
+ fprintf fmt "*%a%a" print_attributes al (print_decl n) d
| ARRAY (d, al, e) ->
- fprintf fmt "%a[@[%a%a@]]"
- (print_decl n) d print_attributes al print_expression e
+ fprintf fmt "%a[@[%a%a@]]"
+ (print_decl n) d print_attributes al print_expression e
| PROTO(d, args, isva) ->
- fprintf fmt "@[%a@;(%a)@]"
- (print_decl n) d print_params (args,isva)
+ fprintf fmt "@[%a@;(%a)@]"
+ (print_decl n) d print_params (args,isva)
and print_fields fmt (flds : field_group list) =
pp_list ~sep:"@ " print_field_group fmt flds
@@ -273,8 +273,8 @@ and print_name fmt ((n, decl, attrs, _) : name) =
and print_init_name fmt ((n, i) : init_name) =
match i with
- NO_INIT -> print_name fmt n
- | _ -> fprintf fmt "%a@ =@ %a" print_name n print_init_expression i
+ NO_INIT -> print_name fmt n
+ | _ -> fprintf fmt "%a@ =@ %a" print_name n print_init_expression i
and print_name_group fmt (specs, names) =
fprintf fmt "%a@ %a"
@@ -282,17 +282,17 @@ and print_name_group fmt (specs, names) =
and print_field_group fmt fld = match fld with
| FIELD (specs, fields) ->
- fprintf fmt "%a@ %a;"
- print_specifiers specs
- (pp_list ~sep:",@ " print_field) fields
+ fprintf fmt "%a@ %a;"
+ print_specifiers specs
+ (pp_list ~sep:",@ " print_field) fields
| TYPE_ANNOT annot ->
- fprintf fmt "@\n/*@@@[@ %a@]@ */@\n"
- Logic_print.print_type_annot annot
+ fprintf fmt "@\n/*@@@[@ %a@]@ */@\n"
+ Logic_print.print_type_annot annot
and print_field fmt (name, widtho) =
match widtho with
- None -> print_name fmt name
- | Some w -> fprintf fmt "%a:@ %a" print_name name print_expression w
+ None -> print_name fmt name
+ | Some w -> fprintf fmt "%a:@ %a" print_name name print_expression w
and print_init_name_group fmt (specs, names) =
fprintf fmt "%a@ @[%a@]"
@@ -305,8 +305,8 @@ and print_params fmt (pars,ell) =
pp_list ~sep:",@ " print_single_name fmt pars;
if ell then begin
match pars with
- [] -> pp_print_string fmt "..."
- | _ -> fprintf fmt ",@ ..."
+ [] -> pp_print_string fmt "..."
+ | _ -> fprintf fmt ",@ ..."
end
and print_comma_exps fmt exps =
@@ -317,28 +317,28 @@ and print_init_expression fmt (iexp: init_expression) =
NO_INIT -> ()
| SINGLE_INIT e -> print_expression fmt e
| COMPOUND_INIT initexps ->
- let doinitexp fmt = function
- NEXT_INIT, e -> print_init_expression fmt e
- | i, e ->
- let rec doinit fmt = function
- NEXT_INIT -> ()
- | INFIELD_INIT (fn, i) -> fprintf fmt ".%s%a" fn doinit i
- | ATINDEX_INIT (e, i) ->
- fprintf fmt "[@[%a@]]%a" print_expression e doinit i
- | ATINDEXRANGE_INIT (s, e) ->
- fprintf fmt "@[%a@;...@;%a@]"
- print_expression s print_expression e
- in
- fprintf fmt "%a@ =@ %a"
- doinit i print_init_expression e
- in
- fprintf fmt "{@[<hov 2>%a@]}"
- (pp_list ~sep:",@ " doinitexp) initexps
+ let doinitexp fmt = function
+ NEXT_INIT, e -> print_init_expression fmt e
+ | i, e ->
+ let rec doinit fmt = function
+ NEXT_INIT -> ()
+ | INFIELD_INIT (fn, i) -> fprintf fmt ".%s%a" fn doinit i
+ | ATINDEX_INIT (e, i) ->
+ fprintf fmt "[@[%a@]]%a" print_expression e doinit i
+ | ATINDEXRANGE_INIT (s, e) ->
+ fprintf fmt "@[%a@;...@;%a@]"
+ print_expression s print_expression e
+ in
+ fprintf fmt "%a@ =@ %a"
+ doinit i print_init_expression e
+ in
+ fprintf fmt "{@[<hov 2>%a@]}"
+ (pp_list ~sep:",@ " doinitexp) initexps
and print_cast_expression fmt = function
NO_INIT -> Kernel.fatal "no init in cast"
| COMPOUND_INIT _ as ie ->
- fprintf fmt "(@[%a@])" print_init_expression ie
+ fprintf fmt "(@[%a@])" print_init_expression ie
| SINGLE_INIT e -> print_expression_level cast_level fmt e
and print_expression fmt (exp: expression) = print_expression_level 0 fmt exp
@@ -351,27 +351,27 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
match e.expr_node with
NOTHING -> ()
| PAREN exp -> print_expression fmt exp
- (* parentheses are added by the level matching. *)
+ (* parentheses are added by the level matching. *)
| UNARY ((POSINCR|POSDECR), exp') ->
- fprintf fmt "%a%s" print_expression exp' txt
+ fprintf fmt "%a%s" print_expression exp' txt
| UNARY (_,exp') -> fprintf fmt "%s%a" txt print_expression exp'
| LABELADDR l -> fprintf fmt "&&%s" l
| BINARY (_op, exp1, exp2) ->
- fprintf fmt "%a@ %s@ %a"
- print_expression exp1 txt print_expression exp2
+ fprintf fmt "%a@ %s@ %a"
+ print_expression exp1 txt print_expression exp2
| QUESTION (exp1, exp2, exp3) ->
- fprintf fmt "%a@ ?@ %a@ :@ %a"
- print_expression exp1 print_expression exp2 print_expression exp3
+ fprintf fmt "%a@ ?@ %a@ :@ %a"
+ print_expression exp1 print_expression exp2 print_expression exp3
| CAST (typ, iexp) ->
- fprintf fmt "(@[%a@])@;%a"
- print_onlytype typ print_cast_expression iexp
+ fprintf fmt "(@[%a@])@;%a"
+ print_onlytype typ print_cast_expression iexp
| CALL ({ expr_node = VARIABLE "__builtin_va_arg"},
[arg; { expr_node = TYPE_SIZEOF (bt, dt) } ]) ->
- fprintf fmt "__builtin_va_arg(@[%a,@ %a@])"
- (print_expression_level 0) arg print_onlytype (bt, dt)
+ fprintf fmt "__builtin_va_arg(@[%a,@ %a@])"
+ (print_expression_level 0) arg print_onlytype (bt, dt)
| CALL (exp, args) ->
- fprintf fmt "%a(@[@;%a@])"
- print_expression exp print_comma_exps args
+ fprintf fmt "%a(@[@;%a@])"
+ print_expression exp print_comma_exps args
| CONSTANT (CONST_INT i) -> pp_print_string fmt i
| CONSTANT (CONST_FLOAT f) -> pp_print_string fmt f
| CONSTANT (CONST_CHAR c) -> fprintf fmt "'%s'" (escape_wstring c)
@@ -380,21 +380,21 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
| CONSTANT (CONST_WSTRING s) -> print_wstring fmt s
| VARIABLE name -> pp_print_string fmt name
| EXPR_SIZEOF exp ->
- fprintf fmt "sizeof%a" print_expression exp
+ fprintf fmt "sizeof%a" print_expression exp
| TYPE_SIZEOF (bt,dt) ->
- fprintf fmt "sizeof(@[%a@])" print_onlytype (bt,dt)
+ fprintf fmt "sizeof(@[%a@])" print_onlytype (bt,dt)
| EXPR_ALIGNOF exp ->
- fprintf fmt "__alignof__%a" print_expression exp
+ fprintf fmt "__alignof__%a" print_expression exp
| TYPE_ALIGNOF (bt,dt) ->
- fprintf fmt "__alignof__(@[%a@])" print_onlytype (bt, dt)
+ fprintf fmt "__alignof__(@[%a@])" print_onlytype (bt, dt)
| INDEX (exp, idx) ->
- fprintf fmt "%a[@[%a@]]"
- print_expression exp (print_expression_level 0) idx
+ fprintf fmt "%a[@[%a@]]"
+ print_expression exp (print_expression_level 0) idx
| MEMBEROF (exp, fld) ->
- fprintf fmt "%a.%s" print_expression exp fld
+ fprintf fmt "%a.%s" print_expression exp fld
| MEMBEROFPTR (exp, fld) ->
- fprintf fmt "%a->%s"
- print_expression exp fld
+ fprintf fmt "%a->%s"
+ print_expression exp fld
| GNU_BODY blk -> fprintf fmt "(@[%a@])" print_block blk
| EXPR_PATTERN (name) -> fprintf fmt "@@expr(%s)" name
| COMMA l -> pp_list ~sep:",@ " print_expression fmt l
@@ -408,117 +408,117 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
*)
and print_for_init fmt fc =
match fc with
- FC_EXP exp -> print_expression fmt exp
- | FC_DECL dec -> print_def fmt dec
+ FC_EXP exp -> print_expression fmt exp
+ | FC_DECL dec -> print_def fmt dec
and print_statement fmt stat =
let loc = Cabshelper.get_statementloc stat in
Cil_const.CurrentLoc.set loc;
- if Kernel.debug_atleast 2 then
+ if Kernel.debug_atleast 2 then
fprintf fmt "@\n/* %a */@\n" Cil_printer.pp_location loc;
match stat.stmt_node with
- NOP _ -> pp_print_string fmt ";"
- | COMPUTATION (exp,_) -> fprintf fmt "%a;" print_expression exp
- | BLOCK (blk, _,_) -> print_block fmt blk
- | SEQUENCE (s1, s2,_) ->
- fprintf fmt "%a;@ %a" print_statement s1 print_statement s2
- | IF (exp, s1, s2, _) ->
- fprintf fmt "@[<hov 2>if@ (@[%a@])@ %a@."
- print_expression exp print_substatement s1;
- (match s2.stmt_node with
- | NOP(_) -> fprintf fmt "@]"
- | _ -> fprintf fmt "@ else@ %a@]" print_substatement s2)
- | WHILE (annot,exp, stat,_) ->
- fprintf fmt "%a@[<hov 2>while@ (@[%a@])@ %a@]"
- (pp_list ~pre:"/*@@ @[" ~sep:"@\n" ~suf:"@]*/" print_code_annot)
- annot
- print_expression exp print_substatement stat
- | DOWHILE (annot,exp, stat, _) ->
- fprintf fmt "%a@[<hov 2>do@ %a@ while@ (@[%a@])@]"
- (pp_list ~pre:"/*@@ @[" ~sep:"@\n" ~suf:"@]*/" print_code_annot)
- annot
- print_substatement stat print_expression exp
- | FOR (annot,fc1, exp2, exp3, stat, _) ->
- fprintf fmt "%a@[<hov 2>for(@[%a;@ %a;@ %a@])@ %a@]"
- (pp_list ~pre:"/*@@ @[" ~sep:"@\n" ~suf:"@]*/" print_code_annot)
- annot
- print_for_init fc1
- print_expression exp2
- print_expression exp3
- print_substatement stat
- | BREAK _ -> pp_print_string fmt "break;"
- | CONTINUE _ -> pp_print_string fmt "continue;"
- | RETURN (exp, _) ->
- let has_paren exp =
- match exp.expr_node with
- | PAREN _ -> true
- | _ -> false in
- fprintf fmt "return%a%a;"
- (pp_cond (not (exp.expr_node = NOTHING || has_paren exp))) "@ "
- print_expression exp
- | SWITCH (exp, stat,_) ->
- fprintf fmt "@[<hov 2>switch@ (@[%a@])@ %a@]"
- print_expression exp print_substatement stat
- | CASE (exp, stat, _) ->
- fprintf fmt "@[<2>case@ %a:@ %a@]"
- print_expression exp print_substatement stat
- | CASERANGE (expl, exph, stat, _) ->
- fprintf fmt "@[<2>case@ %a@;...@;%a:@ %a@]"
- print_expression expl
- print_expression exph
- print_substatement stat
- | DEFAULT (stat,_) ->
- fprintf fmt "@[<2>default:@ %a@]" print_substatement stat
- | LABEL (name, stat, _) ->
- fprintf fmt "@.@[<2>%s:@ %a@]" name print_substatement stat
- | GOTO (name, _) -> fprintf fmt "goto %s;" name
- | COMPGOTO (exp, _) ->
- fprintf fmt "goto@ @[*%a@];" print_expression exp
- | DEFINITION d -> print_def fmt d
- | ASM (attrs, tlist, details, _) ->
- let print_asm_operand fmt (_identop,cnstr, e) =
- fprintf fmt "@[%s@ (@[%a@])@]" cnstr print_expression e
- in
- if !msvcMode then begin
- fprintf fmt "__asm@ {@[%a@]}"
- (pp_list ~sep:"@\n" pp_print_string) tlist
- end else begin
- let print_details
- fmt { aoutputs = outs; ainputs = ins; aclobbers = clobs } =
- pp_list ~sep:",@ " print_asm_operand fmt outs;
- pp_cond (ins<>[]||clobs<>[]) fmt ":@ ";
- pp_list ~sep:",@ " print_asm_operand fmt ins;
- pp_cond (clobs<>[]) fmt ":@ ";
- pp_list ~sep:",@ " pp_print_string fmt clobs
- in
- fprintf fmt "@[__asm__%a@;(@[%a%a])@]"
- print_attributes attrs
- (pp_list ~sep:"@ " pp_print_string) tlist
- (pp_opt ~pre:":@ " print_details) details
- end
- | THROW(e,_) ->
- fprintf fmt "@[<hov 2>throw%a@]"
- (Pretty_utils.pp_opt ~pre:" (@;" ~suf:")" print_expression) e
- | TRY_CATCH(s,l,_) ->
- let print_one_catch fmt (e,s) =
- fprintf fmt "@[<v 2>@[catch %a {@]@;%a@]@;}@;"
- (Pretty_utils.pp_opt print_single_name) e
- print_statement s
+ NOP _ -> pp_print_string fmt ";"
+ | COMPUTATION (exp,_) -> fprintf fmt "%a;" print_expression exp
+ | BLOCK (blk, _,_) -> print_block fmt blk
+ | SEQUENCE (s1, s2,_) ->
+ fprintf fmt "%a;@ %a" print_statement s1 print_statement s2
+ | IF (exp, s1, s2, _) ->
+ fprintf fmt "@[<hov 2>if@ (@[%a@])@ %a@."
+ print_expression exp print_substatement s1;
+ (match s2.stmt_node with
+ | NOP(_) -> fprintf fmt "@]"
+ | _ -> fprintf fmt "@ else@ %a@]" print_substatement s2)
+ | WHILE (annot,exp, stat,_) ->
+ fprintf fmt "%a@[<hov 2>while@ (@[%a@])@ %a@]"
+ (pp_list ~pre:"/*@@ @[" ~sep:"@\n" ~suf:"@]*/" print_code_annot)
+ annot
+ print_expression exp print_substatement stat
+ | DOWHILE (annot,exp, stat, _) ->
+ fprintf fmt "%a@[<hov 2>do@ %a@ while@ (@[%a@])@]"
+ (pp_list ~pre:"/*@@ @[" ~sep:"@\n" ~suf:"@]*/" print_code_annot)
+ annot
+ print_substatement stat print_expression exp
+ | FOR (annot,fc1, exp2, exp3, stat, _) ->
+ fprintf fmt "%a@[<hov 2>for(@[%a;@ %a;@ %a@])@ %a@]"
+ (pp_list ~pre:"/*@@ @[" ~sep:"@\n" ~suf:"@]*/" print_code_annot)
+ annot
+ print_for_init fc1
+ print_expression exp2
+ print_expression exp3
+ print_substatement stat
+ | BREAK _ -> pp_print_string fmt "break;"
+ | CONTINUE _ -> pp_print_string fmt "continue;"
+ | RETURN (exp, _) ->
+ let has_paren exp =
+ match exp.expr_node with
+ | PAREN _ -> true
+ | _ -> false in
+ fprintf fmt "return%a%a;"
+ (pp_cond (not (exp.expr_node = NOTHING || has_paren exp))) "@ "
+ print_expression exp
+ | SWITCH (exp, stat,_) ->
+ fprintf fmt "@[<hov 2>switch@ (@[%a@])@ %a@]"
+ print_expression exp print_substatement stat
+ | CASE (exp, stat, _) ->
+ fprintf fmt "@[<2>case@ %a:@ %a@]"
+ print_expression exp print_substatement stat
+ | CASERANGE (expl, exph, stat, _) ->
+ fprintf fmt "@[<2>case@ %a@;...@;%a:@ %a@]"
+ print_expression expl
+ print_expression exph
+ print_substatement stat
+ | DEFAULT (stat,_) ->
+ fprintf fmt "@[<2>default:@ %a@]" print_substatement stat
+ | LABEL (name, stat, _) ->
+ fprintf fmt "@.@[<2>%s:@ %a@]" name print_substatement stat
+ | GOTO (name, _) -> fprintf fmt "goto %s;" name
+ | COMPGOTO (exp, _) ->
+ fprintf fmt "goto@ @[*%a@];" print_expression exp
+ | DEFINITION d -> print_def fmt d
+ | ASM (attrs, tlist, details, _) ->
+ let print_asm_operand fmt (_identop,cnstr, e) =
+ fprintf fmt "@[%s@ (@[%a@])@]" cnstr print_expression e
+ in
+ if !msvcMode then begin
+ fprintf fmt "__asm@ {@[%a@]}"
+ (pp_list ~sep:"@\n" pp_print_string) tlist
+ end else begin
+ let print_details
+ fmt { aoutputs = outs; ainputs = ins; aclobbers = clobs } =
+ pp_list ~sep:",@ " print_asm_operand fmt outs;
+ pp_cond (ins<>[]||clobs<>[]) fmt ":@ ";
+ pp_list ~sep:",@ " print_asm_operand fmt ins;
+ pp_cond (clobs<>[]) fmt ":@ ";
+ pp_list ~sep:",@ " pp_print_string fmt clobs
in
- fprintf fmt "@[<v 2>@[try %a {@]@;%a@]@;}@;"
+ fprintf fmt "@[__asm__%a@;(@[%a%a])@]"
+ print_attributes attrs
+ (pp_list ~sep:"@ " pp_print_string) tlist
+ (pp_opt ~pre:":@ " print_details) details
+ end
+ | THROW(e,_) ->
+ fprintf fmt "@[<hov 2>throw%a@]"
+ (Pretty_utils.pp_opt ~pre:" (@;" ~suf:")" print_expression) e
+ | TRY_CATCH(s,l,_) ->
+ let print_one_catch fmt (e,s) =
+ fprintf fmt "@[<v 2>@[catch %a {@]@;%a@]@;}@;"
+ (Pretty_utils.pp_opt print_single_name) e
print_statement s
- (Pretty_utils.pp_list ~sep:"@;" print_one_catch) l
- | TRY_FINALLY (b, h, _) ->
- fprintf fmt "__try@ @[%a@]@ __finally@ @[%a@]"
- print_block b print_block h
- | TRY_EXCEPT (b, e, h, _) ->
- fprintf fmt "__try@ @[%a@]@ __except(@[%a@])@ @[%a@]"
- print_block b print_expression e print_block h
- | CODE_ANNOT (a, _) ->
- fprintf fmt "/*@@@ @[%a@]@ */"
- Logic_print.print_code_annot a
- | CODE_SPEC (a, _) ->
- fprintf fmt "/*@@@ @[%a@]@ */" Logic_print.print_spec a
+ in
+ fprintf fmt "@[<v 2>@[try %a {@]@;%a@]@;}@;"
+ print_statement s
+ (Pretty_utils.pp_list ~sep:"@;" print_one_catch) l
+ | TRY_FINALLY (b, h, _) ->
+ fprintf fmt "__try@ @[%a@]@ __finally@ @[%a@]"
+ print_block b print_block h
+ | TRY_EXCEPT (b, e, h, _) ->
+ fprintf fmt "__try@ @[%a@]@ __except(@[%a@])@ @[%a@]"
+ print_block b print_expression e print_block h
+ | CODE_ANNOT (a, _) ->
+ fprintf fmt "/*@@@ @[%a@]@ */"
+ Logic_print.print_code_annot a
+ | CODE_SPEC (a, _) ->
+ fprintf fmt "/*@@@ @[%a@]@ */" Logic_print.print_spec a
and print_block fmt blk =
fprintf fmt "@ {@ @[<hov>%a%a%a@]@ }"
@@ -533,27 +533,27 @@ and print_substatement fmt stat =
IF _
| SEQUENCE _
| DOWHILE _ ->
- fprintf fmt "@ {@ @[%a@]@ }" print_statement stat
+ fprintf fmt "@ {@ @[%a@]@ }" print_statement stat
| _ ->
- print_statement fmt stat
+ print_statement fmt stat
(*
** GCC Attributes
*)
and print_attribute fmt (name,args) =
match args with
- [] -> pp_print_string fmt name
- | _ ->
- let cond = name = "__attribute__" in
- let print_args fmt = function
- [{expr_node = VARIABLE "aconst"}] ->
- pp_print_string fmt "const"
- | [{expr_node = VARIABLE "restrict"}] ->
- pp_print_string fmt "restrict"
- | args -> pp_list ~sep:",@ " print_expression fmt args
- in
- fprintf fmt "%s(%a@[%a@]%a)"
- name (pp_cond cond) "(" print_args args (pp_cond cond) ")"
+ [] -> pp_print_string fmt name
+ | _ ->
+ let cond = name = "__attribute__" in
+ let print_args fmt = function
+ [{expr_node = VARIABLE "aconst"}] ->
+ pp_print_string fmt "const"
+ | [{expr_node = VARIABLE "restrict"}] ->
+ pp_print_string fmt "restrict"
+ | args -> pp_list ~sep:",@ " print_expression fmt args
+ in
+ fprintf fmt "%s(%a@[%a@]%a)"
+ name (pp_cond cond) "(" print_args args (pp_cond cond) ")"
(* Print attributes. *)
and print_attributes fmt attrs =
@@ -566,11 +566,11 @@ and print_defs fmt defs =
let prev = ref false in
List.iter
(fun (ghost,def) ->
- (match def with
- DECDEF _ -> prev := false
- | _ ->
- if not !prev then pp_print_newline fmt ();
- prev := true);
+ (match def with
+ DECDEF _ -> prev := false
+ | _ ->
+ if not !prev then pp_print_newline fmt ();
+ prev := true);
if ghost then fprintf fmt "/*@@@ @[ghost@ %a@]@ */" print_def def
else print_def fmt def
)
@@ -580,54 +580,54 @@ and print_def fmt def =
Cil_const.CurrentLoc.set (Cabshelper.get_definitionloc def);
match def with
FUNDEF (spec, proto, body, loc, _) ->
- if !printCounters then begin
- try
- let fname =
- match proto with
- (_, (n, _, _, _)) -> n
- in
- print_def fmt (DECDEF (None,([SpecType Tint],
- [(fname ^ "__counter", JUSTBASE, [], loc),
- NO_INIT]), loc));
- with Not_found ->
- pp_print_string fmt "/* can't print the counter */"
- end;
- fprintf fmt "@[%a%a@\n%a@]@\n"
- (Pretty_utils.pp_opt ~pre:"/*@@ @[" ~suf:"@]@\n */@\n"
- (fun fmt (spec,_) -> Logic_print.print_spec fmt spec))
- spec
- print_single_name proto print_block body
+ if !printCounters then begin
+ try
+ let fname =
+ match proto with
+ (_, (n, _, _, _)) -> n
+ in
+ print_def fmt (DECDEF (None,([SpecType Tint],
+ [(fname ^ "__counter", JUSTBASE, [], loc),
+ NO_INIT]), loc));
+ with Not_found ->
+ pp_print_string fmt "/* can't print the counter */"
+ end;
+ fprintf fmt "@[%a%a@\n%a@]@\n"
+ (Pretty_utils.pp_opt ~pre:"/*@@ @[" ~suf:"@]@\n */@\n"
+ (fun fmt (spec,_) -> Logic_print.print_spec fmt spec))
+ spec
+ print_single_name proto print_block body
| DECDEF (spec,names, _) ->
- fprintf fmt "@[%a%a;@]@\n"
- (Pretty_utils.pp_opt ~pre:"/*@@ @[" ~suf:"@]@\n */@\n"
- (fun fmt (spec,_) -> Logic_print.print_spec fmt spec))
- spec
- print_init_name_group names
+ fprintf fmt "@[%a%a;@]@\n"
+ (Pretty_utils.pp_opt ~pre:"/*@@ @[" ~suf:"@]@\n */@\n"
+ (fun fmt (spec,_) -> Logic_print.print_spec fmt spec))
+ spec
+ print_init_name_group names
| TYPEDEF (names, _) ->
- fprintf fmt "@[%a;@\n@]" print_name_group names
+ fprintf fmt "@[%a;@\n@]" print_name_group names
| ONLYTYPEDEF (specs, _) ->
- fprintf fmt "@[%a;@\n@]" print_specifiers specs
+ fprintf fmt "@[%a;@\n@]" print_specifiers specs
| GLOBASM (asm, _) ->
- fprintf fmt "@[__asm__(%s);@\n@]" asm
+ fprintf fmt "@[__asm__(%s);@\n@]" asm
| GLOBANNOT (annot) ->
- fprintf fmt "@[/*@@@ @[%a@]@ */@]@\n"
- (pp_list ~sep:"@\n" Logic_print.print_decl) annot
+ fprintf fmt "@[/*@@@ @[%a@]@ */@]@\n"
+ (pp_list ~sep:"@\n" Logic_print.print_decl) annot
| CUSTOM _ -> fprintf fmt "<custom annot>"
| PRAGMA (a,_) ->
- fprintf fmt "@[#pragma %a@]@\n" print_expression a
+ fprintf fmt "@[#pragma %a@]@\n" print_expression a
| LINKAGE (n, _, dl) ->
- fprintf fmt "@[<2>extern@ %s@ {%a@;}@]" n (pp_list print_def) dl
+ fprintf fmt "@[<2>extern@ %s@ {%a@;}@]" n (pp_list print_def) dl
(* print abstrac_syntax -> ()
-** Pretty printing the given abstract syntax program.
+ ** Pretty printing the given abstract syntax program.
*)
let printFile fmt ((_fname, defs) : file) = print_defs fmt defs
diff --git a/src/kernel_services/ast_printing/cprint.mli b/src/kernel_services/ast_printing/cprint.mli
index 7efec3e0231..9ea4e8d86a6 100644
--- a/src/kernel_services/ast_printing/cprint.mli
+++ b/src/kernel_services/ast_printing/cprint.mli
@@ -51,7 +51,7 @@ val printCounters : bool ref
val printComments : bool ref
val get_operator : Cabs.expression -> (string * int)
-
+
val print_specifiers : Format.formatter -> Cabs.specifier -> unit
val print_type_spec : Format.formatter -> Cabs.typeSpecifier -> unit
val print_struct_name_attr :
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index c4fe1d6cdfd..6f92b4e6369 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -33,74 +33,74 @@ let pp_opt doit pp fmt x = if doit then pp fmt x
let goto_stmt stmt =
let rec goto_label = function
| [] -> Printf.sprintf "s%04d" stmt.sid
- | Label(a,_,true)::_ -> a
+ | Label(a,_,true)::_ -> a
| _::labels -> goto_label labels
in goto_label stmt.labels
let rec stmt_labels = function
| Label(a,_,true) :: ls -> a :: stmt_labels ls
| Label _ :: ls -> stmt_labels ls
- | Case(e,_) :: ls ->
- let cvalue = (Cil.constFold true e) in
- Format.asprintf "case %a" Printer.pp_exp cvalue
- :: stmt_labels ls
+ | Case(e,_) :: ls ->
+ let cvalue = (Cil.constFold true e) in
+ Format.asprintf "case %a" Printer.pp_exp cvalue
+ :: stmt_labels ls
| Default _ :: ls ->
- "default" :: stmt_labels ls
+ "default" :: stmt_labels ls
| [] -> []
let pp_labels fmt stmt =
match stmt_labels stmt.labels with
- | [] -> ()
- | ls -> Format.fprintf fmt " '%s'" (String.concat "," ls)
+ | [] -> ()
+ | ls -> Format.fprintf fmt " '%s'" (String.concat "," ls)
let pp_idpred kloc fmt idpred =
let np = idpred.ip_content in
- if np.pred_name <> []
+ if np.pred_name <> []
then Format.fprintf fmt " '%s'" (String.concat "," np.pred_name)
else pp_kloc kloc fmt np.pred_loc
let pp_allocation kloc fmt (allocation:identified_term list) =
if allocation = [] then Format.fprintf fmt "nothing"
else
- let names =
+ let names =
List.fold_left
- (fun names x -> names @ x.it_content.term_name)
- [] allocation in
+ (fun names x -> names @ x.it_content.term_name)
+ [] allocation in
match names with
- | [] ->
- if kloc then
- let x = List.hd allocation in
- Format.fprintf fmt "(%a)" pp_loc x.it_content.term_loc
- else Format.fprintf fmt "..."
- | _ ->
- Format.fprintf fmt "'%s'" (String.concat "," names)
+ | [] ->
+ if kloc then
+ let x = List.hd allocation in
+ Format.fprintf fmt "(%a)" pp_loc x.it_content.term_loc
+ else Format.fprintf fmt "..."
+ | _ ->
+ Format.fprintf fmt "'%s'" (String.concat "," names)
let pp_region kloc fmt (region:from list) =
if region = [] then Format.fprintf fmt "nothing"
else
- let names =
+ let names =
List.fold_left
- (fun names (x,_) -> names @ x.it_content.term_name)
- [] region in
+ (fun names (x,_) -> names @ x.it_content.term_name)
+ [] region in
match names with
- | [] ->
- if kloc then
- let x = fst (List.hd region) in
- Format.fprintf fmt "(%a)" pp_loc x.it_content.term_loc
- else Format.fprintf fmt "..."
- | _ ->
- Format.fprintf fmt "'%s'" (String.concat "," names)
+ | [] ->
+ if kloc then
+ let x = fst (List.hd region) in
+ Format.fprintf fmt "(%a)" pp_loc x.it_content.term_loc
+ else Format.fprintf fmt "..."
+ | _ ->
+ Format.fprintf fmt "'%s'" (String.concat "," names)
let pp_bhv fmt bhv =
- if not (Cil.is_default_behavior bhv) then
+ if not (Cil.is_default_behavior bhv) then
Format.fprintf fmt " for '%s'" bhv.b_name
let pp_bhvs fmt = function
| [] -> ()
| b::bs ->
- Format.fprintf fmt " @[<hov 0>'%s'" b ;
- List.iter (fun b -> Format.fprintf fmt ",@ '%s'" b) bs ;
- Format.fprintf fmt "@]"
+ Format.fprintf fmt " @[<hov 0>'%s'" b ;
+ List.iter (fun b -> Format.fprintf fmt ",@ '%s'" b) bs ;
+ Format.fprintf fmt "@]"
let pp_for fmt = function
| [] -> ()
@@ -112,42 +112,42 @@ let pp_named fmt nx =
let pp_code_annot fmt ca =
match ca.annot_content with
- | AAssert(bs,np) -> Format.fprintf fmt "assertion%a%a" pp_for bs pp_named np
- | AInvariant(bs,_,np) ->
- Format.fprintf fmt "invariant%a%a" pp_for bs pp_named np
- | AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
- | AAllocation(bs,_) -> Format.fprintf fmt "allocates_frees%a" pp_for bs
- | APragma _ -> Format.pp_print_string fmt "pragma"
- | AVariant _ -> Format.pp_print_string fmt "variant"
- | AStmtSpec _ -> Format.pp_print_string fmt "block contract"
- | AExtended _ -> Format.pp_print_string fmt "extension"
+ | AAssert(bs,np) -> Format.fprintf fmt "assertion%a%a" pp_for bs pp_named np
+ | AInvariant(bs,_,np) ->
+ Format.fprintf fmt "invariant%a%a" pp_for bs pp_named np
+ | AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
+ | AAllocation(bs,_) -> Format.fprintf fmt "allocates_frees%a" pp_for bs
+ | APragma _ -> Format.pp_print_string fmt "pragma"
+ | AVariant _ -> Format.pp_print_string fmt "variant"
+ | AStmtSpec _ -> Format.pp_print_string fmt "block contract"
+ | AExtended _ -> Format.pp_print_string fmt "extension"
let pp_stmt kloc fmt stmt =
match stmt.skind with
- | Instr (Local_init (v,_,loc)) ->
- Format.fprintf fmt "initialization of '%s'%a" v.vname (pp_kloc kloc) loc
- | Instr (Call(_,{enode=Lval(Var v,_)},_,loc)) ->
- Format.fprintf fmt "call '%s'%a" v.vname (pp_kloc kloc) loc
- | Instr (Set(_,_,loc)|Call(_,_,_,loc)) ->
- Format.fprintf fmt "instruction%a" (pp_kloc kloc) loc
- | Instr (Asm(_,_,_,loc)) ->
- Format.fprintf fmt "assembly%a%a" pp_labels stmt (pp_kloc kloc) loc
- | Instr (Skip(_,loc)) ->
- Format.fprintf fmt "program point%a%a" pp_labels stmt (pp_kloc kloc) (loc,loc)
- | Instr (Code_annot(ca,loc)) ->
- Format.fprintf fmt "%a%a" pp_code_annot ca (pp_kloc kloc) loc
- | Return(_,loc) -> Format.fprintf fmt "return%a" (pp_kloc kloc) loc
- | Goto(s,loc) -> Format.fprintf fmt "goto %s%a" (goto_stmt !s) (pp_kloc kloc) loc
- | Break loc -> Format.fprintf fmt "break%a" (pp_kloc kloc) loc
- | Continue loc -> Format.fprintf fmt "continue%a" (pp_kloc kloc) loc
- | If(_,_,_,loc) -> Format.fprintf fmt "if-then-else%a" (pp_kloc kloc) loc
- | Switch(_,_,_,loc) -> Format.fprintf fmt "switch%a" (pp_kloc kloc) loc
- | Loop(_,_,loc,_,_) -> Format.fprintf fmt "loop%a" (pp_kloc kloc) loc
- | Block _ -> Format.fprintf fmt "block%a" pp_labels stmt
- | UnspecifiedSequence _ -> Format.fprintf fmt "instruction%a" pp_labels stmt
- | Throw(_,loc) -> Format.fprintf fmt "throw%a" (pp_kloc kloc) loc
- | TryFinally(_,_,loc) | TryExcept(_,_,_,loc) | TryCatch(_,_,loc)->
- Format.fprintf fmt "try-catch%a" (pp_kloc kloc) loc
+ | Instr (Local_init (v,_,loc)) ->
+ Format.fprintf fmt "initialization of '%s'%a" v.vname (pp_kloc kloc) loc
+ | Instr (Call(_,{enode=Lval(Var v,_)},_,loc)) ->
+ Format.fprintf fmt "call '%s'%a" v.vname (pp_kloc kloc) loc
+ | Instr (Set(_,_,loc)|Call(_,_,_,loc)) ->
+ Format.fprintf fmt "instruction%a" (pp_kloc kloc) loc
+ | Instr (Asm(_,_,_,loc)) ->
+ Format.fprintf fmt "assembly%a%a" pp_labels stmt (pp_kloc kloc) loc
+ | Instr (Skip(_,loc)) ->
+ Format.fprintf fmt "program point%a%a" pp_labels stmt (pp_kloc kloc) (loc,loc)
+ | Instr (Code_annot(ca,loc)) ->
+ Format.fprintf fmt "%a%a" pp_code_annot ca (pp_kloc kloc) loc
+ | Return(_,loc) -> Format.fprintf fmt "return%a" (pp_kloc kloc) loc
+ | Goto(s,loc) -> Format.fprintf fmt "goto %s%a" (goto_stmt !s) (pp_kloc kloc) loc
+ | Break loc -> Format.fprintf fmt "break%a" (pp_kloc kloc) loc
+ | Continue loc -> Format.fprintf fmt "continue%a" (pp_kloc kloc) loc
+ | If(_,_,_,loc) -> Format.fprintf fmt "if-then-else%a" (pp_kloc kloc) loc
+ | Switch(_,_,_,loc) -> Format.fprintf fmt "switch%a" (pp_kloc kloc) loc
+ | Loop(_,_,loc,_,_) -> Format.fprintf fmt "loop%a" (pp_kloc kloc) loc
+ | Block _ -> Format.fprintf fmt "block%a" pp_labels stmt
+ | UnspecifiedSequence _ -> Format.fprintf fmt "instruction%a" pp_labels stmt
+ | Throw(_,loc) -> Format.fprintf fmt "throw%a" (pp_kloc kloc) loc
+ | TryFinally(_,_,loc) | TryExcept(_,_,_,loc) | TryCatch(_,_,loc)->
+ Format.fprintf fmt "try-catch%a" (pp_kloc kloc) loc
let pp_stmt_loc kloc fmt s = Format.fprintf fmt " at %a" (pp_stmt kloc) s
@@ -155,22 +155,22 @@ let pp_kinstr kloc fmt = function
| Kglobal -> () | Kstmt s -> pp_stmt_loc kloc fmt s
let pp_predicate fmt = function
- | PKRequires bhv ->
- Format.fprintf fmt "Pre-condition%a" pp_bhv bhv
- | PKAssumes bhv ->
- Format.fprintf fmt "Assumption%a" pp_bhv bhv
+ | PKRequires bhv ->
+ Format.fprintf fmt "Pre-condition%a" pp_bhv bhv
+ | PKAssumes bhv ->
+ Format.fprintf fmt "Assumption%a" pp_bhv bhv
| PKEnsures(bhv,Normal) ->
- Format.fprintf fmt "Post-condition%a" pp_bhv bhv
+ Format.fprintf fmt "Post-condition%a" pp_bhv bhv
| PKEnsures(bhv,Breaks) ->
- Format.fprintf fmt "Breaking-condition%a" pp_bhv bhv
+ Format.fprintf fmt "Breaking-condition%a" pp_bhv bhv
| PKEnsures(bhv,Continues) ->
- Format.fprintf fmt "Continue-condition%a" pp_bhv bhv
+ Format.fprintf fmt "Continue-condition%a" pp_bhv bhv
| PKEnsures(bhv,Returns) ->
- Format.fprintf fmt "Return-condition%a" pp_bhv bhv
+ Format.fprintf fmt "Return-condition%a" pp_bhv bhv
| PKEnsures(bhv,Exits) ->
- Format.fprintf fmt "Exit-condition%a" pp_bhv bhv
+ Format.fprintf fmt "Exit-condition%a" pp_bhv bhv
| PKTerminates ->
- Format.fprintf fmt "Termination-condition"
+ Format.fprintf fmt "Termination-condition"
let pp_kf_context kfopt fmt kf =
match kfopt with
@@ -218,14 +218,14 @@ let rec pp_prop kfopt kiopt kloc fmt = function
| IPOther(s,le) ->
Format.fprintf fmt "%s%a" s (pp_other_loc kfopt kiopt kloc) le
| IPPredicate(kind,kf,Kglobal,idpred) ->
- Format.fprintf fmt "%a%a%a"
- pp_predicate kind
- (pp_idpred kloc) idpred
+ Format.fprintf fmt "%a%a%a"
+ pp_predicate kind
+ (pp_idpred kloc) idpred
(pp_context kfopt) (Some kf)
| IPPredicate(kind,_,ki,idpred) ->
- Format.fprintf fmt "%a%a%a"
- pp_predicate kind
- (pp_idpred kloc) idpred
+ Format.fprintf fmt "%a%a%a"
+ pp_predicate kind
+ (pp_idpred kloc) idpred
(pp_kinstr kloc) ki
| IPExtended(le,(_,_,loc,_ as pred)) ->
Format.fprintf fmt "%a%a"
@@ -236,67 +236,67 @@ let rec pp_prop kfopt kiopt kloc fmt = function
Format.fprintf fmt "Default behavior%a%a"
(pp_opt kiopt (pp_kinstr kloc)) ki (pp_opt kiopt pp_active) active
else
- Format.fprintf fmt "Behavior '%s'%a"
- bhv.b_name
- (pp_opt kiopt (pp_kinstr kloc)) ki
+ Format.fprintf fmt "Behavior '%s'%a"
+ bhv.b_name
+ (pp_opt kiopt (pp_kinstr kloc)) ki
| IPComplete(_,ki,active, bs) ->
- Format.fprintf fmt "Complete behaviors%a%a%a"
+ Format.fprintf fmt "Complete behaviors%a%a%a"
pp_bhvs bs
(pp_opt kiopt (pp_kinstr kloc)) ki (pp_opt kiopt pp_active) active
| IPDisjoint(_,ki,active, bs) ->
- Format.fprintf fmt "Disjoint behaviors%a%a%a"
+ Format.fprintf fmt "Disjoint behaviors%a%a%a"
pp_bhvs bs
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPCodeAnnot(_,_,{annot_content=AAssert(bs,np)}) ->
- Format.fprintf fmt "Assertion%a%a%a"
- pp_for bs
- pp_named np
+ Format.fprintf fmt "Assertion%a%a%a"
+ pp_for bs
+ pp_named np
(pp_kloc kloc) np.pred_loc
| IPCodeAnnot(_,_,{annot_content=AInvariant(bs,_,np)}) ->
- Format.fprintf fmt "Invariant%a%a%a"
- pp_for bs
- pp_named np
+ Format.fprintf fmt "Invariant%a%a%a"
+ pp_for bs
+ pp_named np
(pp_kloc kloc) np.pred_loc
| IPCodeAnnot(_,stmt,_) ->
Format.fprintf fmt "Annotation %a" (pp_stmt kloc) stmt
| IPAllocation(kf,Kglobal,Id_contract (_,bhv),(frees,allocates)) ->
- Format.fprintf fmt "Frees/Allocates%a %a/%a %a"
- pp_bhv bhv
+ Format.fprintf fmt "Frees/Allocates%a %a/%a %a"
+ pp_bhv bhv
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
(pp_context kfopt) (Some kf)
| IPAssigns(kf,Kglobal,Id_contract(_, bhv),region) ->
- Format.fprintf fmt "Assigns%a %a%a"
- pp_bhv bhv
- (pp_region kloc) region
- (pp_context kfopt) (Some kf)
+ Format.fprintf fmt "Assigns%a %a%a"
+ pp_bhv bhv
+ (pp_region kloc) region
+ (pp_context kfopt) (Some kf)
| IPFrom (kf,Kglobal,Id_contract(_,bhv),depend) ->
Format.fprintf fmt "Froms%a %a%a"
- pp_bhv bhv
- (pp_region kloc) [depend]
- (pp_context kfopt) (Some kf)
+ pp_bhv bhv
+ (pp_region kloc) [depend]
+ (pp_context kfopt) (Some kf)
| IPAllocation(_,ki,Id_contract (active,bhv),(frees,allocates)) ->
- Format.fprintf fmt "Frees/Allocates%a %a/%a %a%a"
- pp_bhv bhv
+ Format.fprintf fmt "Frees/Allocates%a %a/%a %a%a"
+ pp_bhv bhv
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPAssigns(_,ki,Id_contract (active,bhv),region) ->
Format.fprintf fmt "Assigns%a %a%a%a"
- pp_bhv bhv
- (pp_region kloc) region
+ pp_bhv bhv
+ (pp_region kloc) region
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPFrom (_,ki,Id_contract (active,bhv),depend) ->
- Format.fprintf fmt "Froms%a %a%a%a"
- pp_bhv bhv
- (pp_region kloc) [depend]
+ Format.fprintf fmt "Froms%a %a%a%a"
+ pp_bhv bhv
+ (pp_region kloc) [depend]
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
| IPAllocation(_,_,Id_loop _,(frees,allocates)) ->
- Format.fprintf fmt "Loop frees%a Loop allocates%a"
+ Format.fprintf fmt "Loop frees%a Loop allocates%a"
(pp_allocation kloc) frees
(pp_allocation kloc) allocates
| IPAssigns(_,_,Id_loop _,region) ->
@@ -307,14 +307,14 @@ let rec pp_prop kfopt kiopt kloc fmt = function
Format.fprintf fmt "Recursion variant"
| IPDecrease(_,Kstmt stmt,_,_) ->
Format.fprintf fmt "Loop variant at %a" (pp_stmt kloc) stmt
- | IPReachable (None, Kglobal, Before) ->
+ | IPReachable (None, Kglobal, Before) ->
(* print "Unreachable": it seems that it is what the user want to see *)
Format.fprintf fmt "Unreachable entry point"
| IPReachable (None, Kglobal, After)
| IPReachable (None, Kstmt _, _) -> assert false
| IPReachable (Some _, Kstmt stmt, ba) ->
(* print "Unreachable": it seems that it is what the user want to see *)
- Format.fprintf fmt "Unreachable %a%s"
+ Format.fprintf fmt "Unreachable %a%s"
(pp_stmt kloc) stmt
(match ba with Before -> "" | After -> " (after it)")
| IPReachable (Some kf, Kglobal, _) ->
@@ -343,18 +343,18 @@ let to_string pp elt =
Buffer.contents b
let code_annot_kind_and_node code_annot = match code_annot.annot_content with
- | AAssert (_, {pred_content; pred_name}) ->
- let kind = match Alarms.find code_annot with
- | Some alarm -> Alarms.get_name alarm
- | None ->
- if List.exists ((=) "missing_return") pred_name
- then "missing_return"
- else "user assertion"
- in
- Some (kind, to_string Printer.pp_predicate_node pred_content)
- | AInvariant (_, _, {pred_content}) ->
- Some ("loop invariant", to_string Printer.pp_predicate_node pred_content)
- | _ -> None
+ | AAssert (_, {pred_content; pred_name}) ->
+ let kind = match Alarms.find code_annot with
+ | Some alarm -> Alarms.get_name alarm
+ | None ->
+ if List.exists ((=) "missing_return") pred_name
+ then "missing_return"
+ else "user assertion"
+ in
+ Some (kind, to_string Printer.pp_predicate_node pred_content)
+ | AInvariant (_, _, {pred_content}) ->
+ Some ("loop invariant", to_string Printer.pp_predicate_node pred_content)
+ | _ -> None
let property_kind_and_node property =
let default kind = Some (kind, to_string Property.pretty property) in
@@ -414,13 +414,13 @@ let cmp_order a b = match a , b with
| F _ , _ -> (-1)
| _ , F _ -> 1
| B a , B b ->
- begin
- match Cil.is_default_behavior a , Cil.is_default_behavior b with
- | true , true -> 0
- | true , false -> (-1)
- | false , true -> 1
- | false , false -> String.compare a.b_name b.b_name
- end
+ begin
+ match Cil.is_default_behavior a , Cil.is_default_behavior b with
+ | true , true -> 0
+ | true , false -> (-1)
+ | false , true -> 1
+ | false , false -> String.compare a.b_name b.b_name
+ end
| B _ , _ -> (-1)
| _ , B _ -> 1
| K a , K b -> Cil_datatype.Kinstr.compare a b
@@ -433,8 +433,8 @@ let rec cmp xs ys = match xs,ys with
| [],_ -> (-1)
| _,[] -> 1
| x::xs,y::ys ->
- let c = cmp_order x y in
- if c<>0 then c else cmp xs ys
+ let c = cmp_order x y in
+ if c<>0 then c else cmp xs ys
let kind_order = function
| PKRequires bhv -> [B bhv;I 1]
@@ -447,8 +447,8 @@ let kind_order = function
| PKTerminates -> [I 8]
let named_order xs = List.map (fun x -> S x) xs
-let for_order k = function
- | [] -> [I k]
+let for_order k = function
+ | [] -> [I k]
| bs -> I (succ k) :: named_order bs
let annot_order = function
| {annot_content=AAssert(bs,np)} ->
@@ -459,7 +459,7 @@ let annot_order = function
let loop_order = function
| Id_contract (active,b) -> [B b; A active]
| Id_loop _ -> []
-
+
let rec ip_order = function
| IPAxiomatic(a,_) -> [I 0;S a]
| IPAxiom(a,_,_,_,_) | IPLemma(a,_,_,_,_) -> [I 1;S a]
diff --git a/src/kernel_services/ast_printing/description.mli b/src/kernel_services/ast_printing/description.mli
index a27280f88ac..6dbb4b79118 100644
--- a/src/kernel_services/ast_printing/description.mli
+++ b/src/kernel_services/ast_printing/description.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Describe items of Source and Properties.
+(** Describe items of Source and Properties.
@since Nitrogen-20111001 *)
open Cil_types
@@ -36,7 +36,7 @@ val pp_idpred : bool -> Format.formatter -> identified_predicate -> unit
val pp_region : bool -> Format.formatter -> from list -> unit
(** prints message "nothing" or the "'<names>'" or the "(<location>)" of the
- relation *)
+ relation *)
val pp_named: Format.formatter -> predicate -> unit
(** prints the name of a named logic structure (if any), separated by ','. *)
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index c81c74c97ee..1de61b50372 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -43,49 +43,49 @@ let rec print_logic_type name fmt typ =
| None -> (fun _ -> ())
in
match typ with
- | LTattribute (t,attr) ->
- let pname fmt =
- fprintf fmt "%a" Cil_printer.pp_attribute attr
- in
- print_logic_type (Some pname) fmt t
- | LTvoid -> fprintf fmt "void%t" pname
- | LTinteger ->
- fprintf fmt "%s%t"
- (if Kernel.Unicode.get () then Utf8_logic.integer else "integer")
- pname
- | LTreal ->
- fprintf fmt "%s%t"
- (if Kernel.Unicode.get () then Utf8_logic.real else "real")
- pname
- | LTint i -> fprintf fmt "%a%t" Cil_printer.pp_ikind i pname
- | LTfloat f -> fprintf fmt "%a%t" Cil_printer.pp_fkind f pname
- | LTarray (t,c) ->
- let pname fmt =
- fprintf fmt "%t[@[%a@]]" pname print_array_size c
- in
- print_logic_type (Some pname) fmt t
- | LTpointer t ->
- let needs_paren = match t with LTarray _ -> true | _ -> false in
- let pname fmt =
- Format.fprintf fmt "%a*%t%a"
- (pp_cond needs_paren) "(" pname (pp_cond needs_paren) ")"
- in
- print_logic_type (Some pname) fmt t
- | LTunion s -> fprintf fmt "union@ %s%t" s pname
- | LTenum s -> fprintf fmt "enum@ %s%t" s pname
- | LTstruct s -> fprintf fmt "struct@ %s%t" s pname
- | LTnamed (s,l) ->
- fprintf fmt "%s%a%t"
- s
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@]>"
- (print_logic_type None)) l
- pname
- | LTarrow(args,ret) ->
- let pname fmt =
- fprintf fmt "%t(@[%a@])" pname
- (pp_list ~sep:",@ " (print_logic_type None)) args
- in
- print_logic_type (Some pname) fmt ret
+ | LTattribute (t,attr) ->
+ let pname fmt =
+ fprintf fmt "%a" Cil_printer.pp_attribute attr
+ in
+ print_logic_type (Some pname) fmt t
+ | LTvoid -> fprintf fmt "void%t" pname
+ | LTinteger ->
+ fprintf fmt "%s%t"
+ (if Kernel.Unicode.get () then Utf8_logic.integer else "integer")
+ pname
+ | LTreal ->
+ fprintf fmt "%s%t"
+ (if Kernel.Unicode.get () then Utf8_logic.real else "real")
+ pname
+ | LTint i -> fprintf fmt "%a%t" Cil_printer.pp_ikind i pname
+ | LTfloat f -> fprintf fmt "%a%t" Cil_printer.pp_fkind f pname
+ | LTarray (t,c) ->
+ let pname fmt =
+ fprintf fmt "%t[@[%a@]]" pname print_array_size c
+ in
+ print_logic_type (Some pname) fmt t
+ | LTpointer t ->
+ let needs_paren = match t with LTarray _ -> true | _ -> false in
+ let pname fmt =
+ Format.fprintf fmt "%a*%t%a"
+ (pp_cond needs_paren) "(" pname (pp_cond needs_paren) ")"
+ in
+ print_logic_type (Some pname) fmt t
+ | LTunion s -> fprintf fmt "union@ %s%t" s pname
+ | LTenum s -> fprintf fmt "enum@ %s%t" s pname
+ | LTstruct s -> fprintf fmt "struct@ %s%t" s pname
+ | LTnamed (s,l) ->
+ fprintf fmt "%s%a%t"
+ s
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@]>"
+ (print_logic_type None)) l
+ pname
+ | LTarrow(args,ret) ->
+ let pname fmt =
+ fprintf fmt "%t(@[%a@])" pname
+ (pp_list ~sep:",@ " (print_logic_type None)) args
+ in
+ print_logic_type (Some pname) fmt ret
let print_typed_ident fmt (t,s) =
print_logic_type (Some (fun fmt -> pp_print_string fmt s)) fmt t
@@ -112,43 +112,43 @@ let get_unop_string = function
let getParenthLevel e =
match e.lexpr_node with
- | PLnamed _ -> 95
- | PLlambda _ | PLlet _ | PLrange _ -> 90
- | PLforall _ | PLexists _ -> 87
- | PLimplies _ | PLiff _ -> 85
- | PLand _ | PLor _ | PLxor _ -> 80
- | PLif _ -> 77
- | PLbinop (_,(Bbw_and | Bbw_or | Bbw_xor),_) -> 75
- | PLrepeat _ -> 72
- | PLrel _ -> 70
- | PLbinop (_,(Badd|Bsub|Blshift|Brshift),_) -> 60
- | PLbinop (_,(Bmul|Bdiv|Bmod),_) -> 40
- | PLunop ((Uamp|Uminus|Ubw_not),_) | PLcast _ | PLnot _ -> 30
- | PLcoercion _ | PLcoercionE _ -> 25
- | PLunop (Ustar,_) | PLdot _ | PLarrow _ | PLarrget _
- | PLsizeof _ | PLsizeofE _ -> 20
- | PLapp _ | PLold _ | PLat _
- | PLoffset _ | PLbase_addr _ | PLblock_length _
- | PLupdate _ | PLinitField _ | PLinitIndex _
- | PLvalid _ | PLvalid_read _ | PLvalid_function _
- | PLinitialized _ | PLdangling _
- | PLallocable _ | PLfreeable _ | PLfresh _
- | PLseparated _ | PLsubtype _ | PLunion _ | PLinter _ -> 10
- | PLvar _ | PLconstant _ | PLresult | PLnull | PLtypeof _ | PLtype _
- | PLfalse | PLtrue | PLcomprehension _ | PLempty | PLset _ | PLlist _ -> 0
+ | PLnamed _ -> 95
+ | PLlambda _ | PLlet _ | PLrange _ -> 90
+ | PLforall _ | PLexists _ -> 87
+ | PLimplies _ | PLiff _ -> 85
+ | PLand _ | PLor _ | PLxor _ -> 80
+ | PLif _ -> 77
+ | PLbinop (_,(Bbw_and | Bbw_or | Bbw_xor),_) -> 75
+ | PLrepeat _ -> 72
+ | PLrel _ -> 70
+ | PLbinop (_,(Badd|Bsub|Blshift|Brshift),_) -> 60
+ | PLbinop (_,(Bmul|Bdiv|Bmod),_) -> 40
+ | PLunop ((Uamp|Uminus|Ubw_not),_) | PLcast _ | PLnot _ -> 30
+ | PLcoercion _ | PLcoercionE _ -> 25
+ | PLunop (Ustar,_) | PLdot _ | PLarrow _ | PLarrget _
+ | PLsizeof _ | PLsizeofE _ -> 20
+ | PLapp _ | PLold _ | PLat _
+ | PLoffset _ | PLbase_addr _ | PLblock_length _
+ | PLupdate _ | PLinitField _ | PLinitIndex _
+ | PLvalid _ | PLvalid_read _ | PLvalid_function _
+ | PLinitialized _ | PLdangling _
+ | PLallocable _ | PLfreeable _ | PLfresh _
+ | PLseparated _ | PLsubtype _ | PLunion _ | PLinter _ -> 10
+ | PLvar _ | PLconstant _ | PLresult | PLnull | PLtypeof _ | PLtype _
+ | PLfalse | PLtrue | PLcomprehension _ | PLempty | PLset _ | PLlist _ -> 0
let rec print_path_elt fmt = function
- | PLpathField s -> fprintf fmt ".%s" s
- | PLpathIndex i -> fprintf fmt "[@[%a@]]" print_lexpr i
+ | PLpathField s -> fprintf fmt ".%s" s
+ | PLpathIndex i -> fprintf fmt "[@[%a@]]" print_lexpr i
and print_path_val fmt (path, v) =
match v with
- | PLupdateTerm e ->
- fprintf fmt "@[%a@ =@ %a@]"
- (pp_list ~sep:"@;" print_path_elt) path print_lexpr e
- | PLupdateCont path_val_list ->
- fprintf fmt "{ \\with %a@ }"
- (pp_list ~sep:",@ " print_path_val) path_val_list
+ | PLupdateTerm e ->
+ fprintf fmt "@[%a@ =@ %a@]"
+ (pp_list ~sep:"@;" print_path_elt) path print_lexpr e
+ | PLupdateCont path_val_list ->
+ fprintf fmt "{ \\with %a@ }"
+ (pp_list ~sep:",@ " print_path_val) path_val_list
and print_init_index fmt (i,v) =
print_path_val fmt ([PLpathIndex i], PLupdateTerm v)
@@ -159,14 +159,14 @@ and print_init_field fmt (s,v) =
and print_lexpr fmt e = print_lexpr_level 100 fmt e
and print_label_1 fmt l =
- match l with
- | None -> ()
- | Some s -> fprintf fmt "{%s}" s
+ match l with
+ | None -> ()
+ | Some s -> fprintf fmt "{%s}" s
and print_label_2 fmt l =
- match l with
- | None -> ()
- | Some (s1,s2) -> fprintf fmt "{%s,%s}" s1 s2
+ match l with
+ | None -> ()
+ | Some (s1,s2) -> fprintf fmt "{%s,%s}" s1 s2
and print_lexpr_level n fmt e =
let n' = getParenthLevel e in
@@ -174,134 +174,134 @@ and print_lexpr_level n fmt e =
let print_lexpr_plain fmt e = print_lexpr_level 100 fmt e in
let aux fmt e =
match e.lexpr_node with
- PLvar s -> pp_print_string fmt s
- | PLapp(s,tv,args) ->
- fprintf fmt "%s@;%a@;(@[%a@])"
- s
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@]>" pp_print_string) tv
- (pp_list ~sep:",@ " print_lexpr_plain) args
- | PLlambda (quant,e) ->
- fprintf fmt "@[<2>\\lambda@ @[%a@];@ %a@]"
- print_quantifiers quant print_lexpr e
- | PLlet (n,def,body) ->
- fprintf fmt "@[@[<2>\\let@ %s@ =@ %a;@]@\n%a@]"
- n print_lexpr def print_lexpr body
- | PLconstant c -> print_constant fmt c
- | PLunop(op,e) -> fprintf fmt "%s%a" (get_unop_string op) print_lexpr e
- | PLbinop(e1,op,e2) ->
- fprintf fmt "%a@ %s@ %a"
- print_lexpr e1 (get_binop_string op) print_lexpr e2
- | PLdot(e,f) -> fprintf fmt "%a.%s" print_lexpr e f
- | PLarrow(e,f) -> fprintf fmt "%a->%s" print_lexpr e f
- | PLarrget(b,i) ->
- fprintf fmt "%a[@;@[%a@]@;]" print_lexpr b print_lexpr i
- | PLlist(args) ->
- fprintf fmt "[@[%a@]]"
- (pp_list ~sep:",@ " print_lexpr_plain) args
- | PLrepeat(e1,e2) ->
- fprintf fmt "%a@ *^@ %a"
- print_lexpr e1 print_lexpr e2
- | PLold(e) -> fprintf fmt "\\old(@;@[%a@]@;)" print_lexpr_plain e
- | PLat(e,s) -> fprintf fmt "\\at(@;@[%a,@ %s@]@;)" print_lexpr_plain e s
- | PLbase_addr (l,e) -> fprintf fmt "\\base_addr%a(@;@[%a@])" print_label_1 l print_lexpr_plain e
- | PLblock_length (l,e) ->
- fprintf fmt "\\block_length%a(@;@[%a@])" print_label_1 l print_lexpr_plain e
- | PLoffset (l,e) ->
- fprintf fmt "\\offset%a(@;@[%a@])" print_label_1 l print_lexpr_plain e
- | PLresult -> pp_print_string fmt "\\result"
- | PLnull -> pp_print_string fmt "\\null"
- | PLcast (t,e) -> fprintf fmt "(@[%a@])@;%a"
- (print_logic_type None) t print_lexpr e
- | PLrange(e1,e2) ->
- fprintf fmt "%a@;..@;%a"
- (pp_opt print_lexpr) e1 (pp_opt print_lexpr) e2
- | PLsizeof t -> fprintf fmt "sizeof(@;@[%a@]@;)" (print_logic_type None) t
- | PLsizeofE e -> fprintf fmt "sizeof(@;@[%a@]@;)" print_lexpr_plain e
- | PLcoercion(e,t) ->
- fprintf fmt "%a@ :>@ %a" print_lexpr e (print_logic_type None) t
- | PLcoercionE(e1,e2) ->
- fprintf fmt "%a@ :>@ %a" print_lexpr e1 print_lexpr e2
- | PLupdate(e1,path,e2) ->
- fprintf fmt "{@ @[%a@ \\with@ %a@]}"
- print_lexpr_plain e1 print_path_val (path, e2)
- | PLinitField(init_field_list) ->
- fprintf fmt "{@ %a@}"
- (pp_list ~sep:",@ " print_init_field) init_field_list
- | PLinitIndex(init_index_list) ->
- fprintf fmt "{@ %a@}"
- (pp_list ~sep:",@ " print_init_index) init_index_list
- | PLtypeof e -> fprintf fmt "typeof(@;@[%a@]@;)" print_lexpr_plain e
- | PLtype t -> fprintf fmt "\\type(@;@[%a@]@;" (print_logic_type None) t
- | PLfalse -> pp_print_string fmt "\\false"
- | PLtrue -> pp_print_string fmt "\\true"
- | PLrel (e1,rel,e2) ->
- fprintf fmt "%a@ %s@ %a"
- print_lexpr e1 (get_relation_string rel) print_lexpr e2
- | PLand(e1,e2) -> fprintf fmt "%a@ &&@ %a" print_lexpr e1 print_lexpr e2
- | PLor(e1,e2) -> fprintf fmt "%a@ ||@ %a" print_lexpr e1 print_lexpr e2
- | PLxor(e1,e2) -> fprintf fmt "%a@ ^^@ %a" print_lexpr e1 print_lexpr e2
- | PLimplies(e1,e2) ->
- fprintf fmt "%a@ ==>@ %a" print_lexpr e1 print_lexpr e2
- | PLiff(e1,e2) ->
- fprintf fmt "%a@ <==>@ %a" print_lexpr e1 print_lexpr e2
- | PLnot e -> fprintf fmt "!@;%a" print_lexpr e
- | PLif (e1,e2,e3) ->
- fprintf fmt "%a@ ?@ %a@ :@ %a"
- print_lexpr e1 print_lexpr e2 print_lexpr e3
- | PLforall(q,e) ->
- fprintf fmt "@[\\forall@ @[%a@];@ %a@]"
- print_quantifiers q print_lexpr e
- | PLexists(q,e) ->
- fprintf fmt "@[\\exists@ @[%a@];@ %a@]"
- print_quantifiers q print_lexpr e
- | PLvalid (l,e) -> fprintf fmt "\\valid%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
- | PLvalid_read (l,e) -> fprintf fmt "\\valid_read%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
- | PLvalid_function e ->
- fprintf fmt "\\valid_function(@;@[%a@]@;)" print_lexpr_plain e
- | PLinitialized (l,e) ->
- fprintf fmt "\\initialized%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
- | PLdangling (l,e) ->
- fprintf fmt "\\dangling%a(@;@[%a@]@;)"
- print_label_1 l print_lexpr_plain e
- | PLseparated l ->
- fprintf fmt "\\separated(@;@[%a@]@;)"
- (pp_list ~sep:",@ " print_lexpr_plain) l
- | PLfreeable (l,e) ->
- fprintf fmt "\\freeable%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
- | PLallocable (l,e) ->
- fprintf fmt "\\allocable%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
- | PLfresh (l2,e1,e2) ->
- fprintf fmt "\\fresh%a(@;@[%a@],@[%a@]@;)" print_label_2 l2 print_lexpr_plain e1 print_lexpr_plain e2
- | PLnamed(s,e) -> fprintf fmt "%s:@ %a" s print_lexpr e
- | PLsubtype (e1,e2) ->
- fprintf fmt "%a@ <:@ %a" print_lexpr e1 print_lexpr e2
- | PLcomprehension(e,q,p) ->
- fprintf fmt "{@ @[%a;@ %a%a@]@ }"
- print_lexpr e print_quantifiers q
- (pp_opt ~pre:"@ |@ " print_lexpr) p
- | PLset l ->
- fprintf fmt "{@ @[%a@]@ }"
- (pp_list ~pre:"@;@[" ~sep:",@ " ~suf:"@]@;" print_lexpr_plain) l
- | PLempty -> pp_print_string fmt "\\empty"
- | PLunion l->
- fprintf fmt "\\union(%a)"
- (pp_list ~pre:"@;@[" ~sep:",@ " ~suf:"@]@;" print_lexpr_plain) l
- | PLinter l->
- fprintf fmt "\\inter(%a)"
- (pp_list ~pre:"@;@[" ~sep:",@ " ~suf:"@]@;" print_lexpr_plain) l
+ PLvar s -> pp_print_string fmt s
+ | PLapp(s,tv,args) ->
+ fprintf fmt "%s@;%a@;(@[%a@])"
+ s
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@]>" pp_print_string) tv
+ (pp_list ~sep:",@ " print_lexpr_plain) args
+ | PLlambda (quant,e) ->
+ fprintf fmt "@[<2>\\lambda@ @[%a@];@ %a@]"
+ print_quantifiers quant print_lexpr e
+ | PLlet (n,def,body) ->
+ fprintf fmt "@[@[<2>\\let@ %s@ =@ %a;@]@\n%a@]"
+ n print_lexpr def print_lexpr body
+ | PLconstant c -> print_constant fmt c
+ | PLunop(op,e) -> fprintf fmt "%s%a" (get_unop_string op) print_lexpr e
+ | PLbinop(e1,op,e2) ->
+ fprintf fmt "%a@ %s@ %a"
+ print_lexpr e1 (get_binop_string op) print_lexpr e2
+ | PLdot(e,f) -> fprintf fmt "%a.%s" print_lexpr e f
+ | PLarrow(e,f) -> fprintf fmt "%a->%s" print_lexpr e f
+ | PLarrget(b,i) ->
+ fprintf fmt "%a[@;@[%a@]@;]" print_lexpr b print_lexpr i
+ | PLlist(args) ->
+ fprintf fmt "[@[%a@]]"
+ (pp_list ~sep:",@ " print_lexpr_plain) args
+ | PLrepeat(e1,e2) ->
+ fprintf fmt "%a@ *^@ %a"
+ print_lexpr e1 print_lexpr e2
+ | PLold(e) -> fprintf fmt "\\old(@;@[%a@]@;)" print_lexpr_plain e
+ | PLat(e,s) -> fprintf fmt "\\at(@;@[%a,@ %s@]@;)" print_lexpr_plain e s
+ | PLbase_addr (l,e) -> fprintf fmt "\\base_addr%a(@;@[%a@])" print_label_1 l print_lexpr_plain e
+ | PLblock_length (l,e) ->
+ fprintf fmt "\\block_length%a(@;@[%a@])" print_label_1 l print_lexpr_plain e
+ | PLoffset (l,e) ->
+ fprintf fmt "\\offset%a(@;@[%a@])" print_label_1 l print_lexpr_plain e
+ | PLresult -> pp_print_string fmt "\\result"
+ | PLnull -> pp_print_string fmt "\\null"
+ | PLcast (t,e) -> fprintf fmt "(@[%a@])@;%a"
+ (print_logic_type None) t print_lexpr e
+ | PLrange(e1,e2) ->
+ fprintf fmt "%a@;..@;%a"
+ (pp_opt print_lexpr) e1 (pp_opt print_lexpr) e2
+ | PLsizeof t -> fprintf fmt "sizeof(@;@[%a@]@;)" (print_logic_type None) t
+ | PLsizeofE e -> fprintf fmt "sizeof(@;@[%a@]@;)" print_lexpr_plain e
+ | PLcoercion(e,t) ->
+ fprintf fmt "%a@ :>@ %a" print_lexpr e (print_logic_type None) t
+ | PLcoercionE(e1,e2) ->
+ fprintf fmt "%a@ :>@ %a" print_lexpr e1 print_lexpr e2
+ | PLupdate(e1,path,e2) ->
+ fprintf fmt "{@ @[%a@ \\with@ %a@]}"
+ print_lexpr_plain e1 print_path_val (path, e2)
+ | PLinitField(init_field_list) ->
+ fprintf fmt "{@ %a@}"
+ (pp_list ~sep:",@ " print_init_field) init_field_list
+ | PLinitIndex(init_index_list) ->
+ fprintf fmt "{@ %a@}"
+ (pp_list ~sep:",@ " print_init_index) init_index_list
+ | PLtypeof e -> fprintf fmt "typeof(@;@[%a@]@;)" print_lexpr_plain e
+ | PLtype t -> fprintf fmt "\\type(@;@[%a@]@;" (print_logic_type None) t
+ | PLfalse -> pp_print_string fmt "\\false"
+ | PLtrue -> pp_print_string fmt "\\true"
+ | PLrel (e1,rel,e2) ->
+ fprintf fmt "%a@ %s@ %a"
+ print_lexpr e1 (get_relation_string rel) print_lexpr e2
+ | PLand(e1,e2) -> fprintf fmt "%a@ &&@ %a" print_lexpr e1 print_lexpr e2
+ | PLor(e1,e2) -> fprintf fmt "%a@ ||@ %a" print_lexpr e1 print_lexpr e2
+ | PLxor(e1,e2) -> fprintf fmt "%a@ ^^@ %a" print_lexpr e1 print_lexpr e2
+ | PLimplies(e1,e2) ->
+ fprintf fmt "%a@ ==>@ %a" print_lexpr e1 print_lexpr e2
+ | PLiff(e1,e2) ->
+ fprintf fmt "%a@ <==>@ %a" print_lexpr e1 print_lexpr e2
+ | PLnot e -> fprintf fmt "!@;%a" print_lexpr e
+ | PLif (e1,e2,e3) ->
+ fprintf fmt "%a@ ?@ %a@ :@ %a"
+ print_lexpr e1 print_lexpr e2 print_lexpr e3
+ | PLforall(q,e) ->
+ fprintf fmt "@[\\forall@ @[%a@];@ %a@]"
+ print_quantifiers q print_lexpr e
+ | PLexists(q,e) ->
+ fprintf fmt "@[\\exists@ @[%a@];@ %a@]"
+ print_quantifiers q print_lexpr e
+ | PLvalid (l,e) -> fprintf fmt "\\valid%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+ | PLvalid_read (l,e) -> fprintf fmt "\\valid_read%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+ | PLvalid_function e ->
+ fprintf fmt "\\valid_function(@;@[%a@]@;)" print_lexpr_plain e
+ | PLinitialized (l,e) ->
+ fprintf fmt "\\initialized%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+ | PLdangling (l,e) ->
+ fprintf fmt "\\dangling%a(@;@[%a@]@;)"
+ print_label_1 l print_lexpr_plain e
+ | PLseparated l ->
+ fprintf fmt "\\separated(@;@[%a@]@;)"
+ (pp_list ~sep:",@ " print_lexpr_plain) l
+ | PLfreeable (l,e) ->
+ fprintf fmt "\\freeable%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+ | PLallocable (l,e) ->
+ fprintf fmt "\\allocable%a(@;@[%a@]@;)" print_label_1 l print_lexpr_plain e
+ | PLfresh (l2,e1,e2) ->
+ fprintf fmt "\\fresh%a(@;@[%a@],@[%a@]@;)" print_label_2 l2 print_lexpr_plain e1 print_lexpr_plain e2
+ | PLnamed(s,e) -> fprintf fmt "%s:@ %a" s print_lexpr e
+ | PLsubtype (e1,e2) ->
+ fprintf fmt "%a@ <:@ %a" print_lexpr e1 print_lexpr e2
+ | PLcomprehension(e,q,p) ->
+ fprintf fmt "{@ @[%a;@ %a%a@]@ }"
+ print_lexpr e print_quantifiers q
+ (pp_opt ~pre:"@ |@ " print_lexpr) p
+ | PLset l ->
+ fprintf fmt "{@ @[%a@]@ }"
+ (pp_list ~pre:"@;@[" ~sep:",@ " ~suf:"@]@;" print_lexpr_plain) l
+ | PLempty -> pp_print_string fmt "\\empty"
+ | PLunion l->
+ fprintf fmt "\\union(%a)"
+ (pp_list ~pre:"@;@[" ~sep:",@ " ~suf:"@]@;" print_lexpr_plain) l
+ | PLinter l->
+ fprintf fmt "\\inter(%a)"
+ (pp_list ~pre:"@;@[" ~sep:",@ " ~suf:"@]@;" print_lexpr_plain) l
in
if n <= n' then fprintf fmt "(@[%a@])" aux e else aux fmt e
let print_typedef fmt = function
- | TDsum l ->
- let print_const fmt (s,args) =
- fprintf fmt "%s%a" s
- (pp_list ~pre:"@ (@[" ~sep:",@ " ~suf:"@])"
- (print_logic_type None))
- args
- in
- pp_list ~sep:"@ |@ " print_const fmt l
- | TDsyn t -> print_logic_type None fmt t
+ | TDsum l ->
+ let print_const fmt (s,args) =
+ fprintf fmt "%s%a" s
+ (pp_list ~pre:"@ (@[" ~sep:",@ " ~suf:"@])"
+ (print_logic_type None))
+ args
+ in
+ pp_list ~sep:"@ |@ " print_const fmt l
+ | TDsyn t -> print_logic_type None fmt t
let print_type_annot fmt ty =
fprintf fmt "@[type@ invariant@ %s(@;@[%a@ %s]@;)@ =@ %a;@]"
@@ -310,109 +310,109 @@ let print_type_annot fmt ty =
let print_model_annot fmt ty =
fprintf fmt "@[model@ %a {@;@[%a@ %s]@;}@ @]"
- (print_logic_type None) ty.model_for_type
- (print_logic_type None) ty.model_type
+ (print_logic_type None) ty.model_for_type
+ (print_logic_type None) ty.model_type
ty.model_name
let rec print_decl fmt d =
match d.decl_node with
- | LDlogic_def(name,labels,tvar,rt,prms,body) ->
- fprintf fmt "@[<2>logic@ %a@ %s%a%a%a@ =@ %a;@]"
- (print_logic_type None) rt name
- (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
- print_lexpr body
- | LDlogic_reads(name,labels,tvar,rt,prms,reads) ->
- fprintf fmt "@[<2>logic@ %a@ %s%a%a%a@ =@ %a;@]"
- (print_logic_type None) rt name
- (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
- (pp_opt ~pre:"@[<2>reads@ " (pp_list ~sep:",@ " print_lexpr)) reads
- | LDtype(name,tvar,def) ->
- fprintf fmt "@[<2>type@ %s%a%a;@]" name
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- (pp_opt ~pre:"@ =@ " print_typedef) def
- | LDpredicate_reads(name,labels,tvar,prms,reads) ->
- fprintf fmt "@[<2>predicate@ %s%a%a%a@ =@ %a;@]" name
- (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
- (pp_opt ~pre:"@[<2>reads@ " (pp_list ~sep:",@ " print_lexpr)) reads
- | LDpredicate_def(name,labels,tvar,prms,body) ->
- fprintf fmt "@[<2>predicate@ %s%a%a%a@ =@ %a;@]" name
- (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
- print_lexpr body
- | LDinductive_def(name,labels,tvar,prms,cases) ->
- let print_case fmt (name,labels,tvar,body) =
- fprintf fmt "@[<2>case@ %s%a%a:@ %a;@]" name
- (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- print_lexpr body
- in
- fprintf fmt "@[<2>inductive@ %s%a%a@;(%a)@ {@\n%a@]@\n}" name
- (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- (pp_list ~sep:",@ " print_typed_ident) prms
- (pp_list ~sep:"@\n" print_case) cases
- | LDlemma(name,is_axiom,labels,tvar,body) ->
- fprintf fmt "@[<2>%a@ %s%a%a:@ %a;@]"
- (pp_cond ~pr_false:"lemma" is_axiom) "axiom" name
- (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
- (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
- print_lexpr body
- | LDaxiomatic (s,d) ->
- fprintf fmt "@[<2>axiomatic@ %s@ {@\n%a@]@\n}" s
- (pp_list ~sep:"@\n" print_decl) d
- | LDinvariant (s,e) ->
- fprintf fmt "@[<2>invariant@ %s:@ %a;@]" s print_lexpr e
- | LDtype_annot ty -> print_type_annot fmt ty
- | LDmodel_annot ty -> print_model_annot fmt ty
- | LDvolatile(tsets,(read,write)) ->
- fprintf fmt "@[<2>volatile@ %a%a%a;@]"
- (pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" print_lexpr) tsets
- (pp_opt ~pre:"@ reads@ " pp_print_string) read
- (pp_opt ~pre:"@ writes@ " pp_print_string) write
- | LDextended (s,l) ->
- fprintf fmt "@[<2>%s@ %a@]" s (pp_list ~sep:",@ " print_lexpr) l
+ | LDlogic_def(name,labels,tvar,rt,prms,body) ->
+ fprintf fmt "@[<2>logic@ %a@ %s%a%a%a@ =@ %a;@]"
+ (print_logic_type None) rt name
+ (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
+ print_lexpr body
+ | LDlogic_reads(name,labels,tvar,rt,prms,reads) ->
+ fprintf fmt "@[<2>logic@ %a@ %s%a%a%a@ =@ %a;@]"
+ (print_logic_type None) rt name
+ (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
+ (pp_opt ~pre:"@[<2>reads@ " (pp_list ~sep:",@ " print_lexpr)) reads
+ | LDtype(name,tvar,def) ->
+ fprintf fmt "@[<2>type@ %s%a%a;@]" name
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ (pp_opt ~pre:"@ =@ " print_typedef) def
+ | LDpredicate_reads(name,labels,tvar,prms,reads) ->
+ fprintf fmt "@[<2>predicate@ %s%a%a%a@ =@ %a;@]" name
+ (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
+ (pp_opt ~pre:"@[<2>reads@ " (pp_list ~sep:",@ " print_lexpr)) reads
+ | LDpredicate_def(name,labels,tvar,prms,body) ->
+ fprintf fmt "@[<2>predicate@ %s%a%a%a@ =@ %a;@]" name
+ (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ (pp_list ~pre:"(@[" ~sep:",@ " ~suf:"@])" print_typed_ident) prms
+ print_lexpr body
+ | LDinductive_def(name,labels,tvar,prms,cases) ->
+ let print_case fmt (name,labels,tvar,body) =
+ fprintf fmt "@[<2>case@ %s%a%a:@ %a;@]" name
+ (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ print_lexpr body
+ in
+ fprintf fmt "@[<2>inductive@ %s%a%a@;(%a)@ {@\n%a@]@\n}" name
+ (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ (pp_list ~sep:",@ " print_typed_ident) prms
+ (pp_list ~sep:"@\n" print_case) cases
+ | LDlemma(name,is_axiom,labels,tvar,body) ->
+ fprintf fmt "@[<2>%a@ %s%a%a:@ %a;@]"
+ (pp_cond ~pr_false:"lemma" is_axiom) "axiom" name
+ (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
+ (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
+ print_lexpr body
+ | LDaxiomatic (s,d) ->
+ fprintf fmt "@[<2>axiomatic@ %s@ {@\n%a@]@\n}" s
+ (pp_list ~sep:"@\n" print_decl) d
+ | LDinvariant (s,e) ->
+ fprintf fmt "@[<2>invariant@ %s:@ %a;@]" s print_lexpr e
+ | LDtype_annot ty -> print_type_annot fmt ty
+ | LDmodel_annot ty -> print_model_annot fmt ty
+ | LDvolatile(tsets,(read,write)) ->
+ fprintf fmt "@[<2>volatile@ %a%a%a;@]"
+ (pp_list ~pre:"@[" ~sep:",@ " ~suf:"@]" print_lexpr) tsets
+ (pp_opt ~pre:"@ reads@ " pp_print_string) read
+ (pp_opt ~pre:"@ writes@ " pp_print_string) write
+ | LDextended (s,l) ->
+ fprintf fmt "@[<2>%s@ %a@]" s (pp_list ~sep:",@ " print_lexpr) l
let print_deps fmt deps =
match deps with
- FromAny -> ()
- | From l ->
- pp_list ~pre:"@ @[<2>\\from@ " ~sep:",@ " ~suf:"@]" print_lexpr fmt l
+ FromAny -> ()
+ | From l ->
+ pp_list ~pre:"@ @[<2>\\from@ " ~sep:",@ " ~suf:"@]" print_lexpr fmt l
let print_assigns fmt a =
match a with
- WritesAny -> ()
- | Writes l ->
- pp_list ~pre:"" ~sep:"" ~suf:""
- (fun fmt (loc,deps) ->
- fprintf fmt "@\nassigns@ %a%a;"
- print_lexpr loc
- print_deps deps)
- fmt l
-
-let print_allocation ~isloop fmt fa =
+ WritesAny -> ()
+ | Writes l ->
+ pp_list ~pre:"" ~sep:"" ~suf:""
+ (fun fmt (loc,deps) ->
+ fprintf fmt "@\nassigns@ %a%a;"
+ print_lexpr loc
+ print_deps deps)
+ fmt l
+
+let print_allocation ~isloop fmt fa =
match fa with
- | FreeAllocAny -> ()
- | FreeAlloc([],[]) ->
- let prefix = if isloop then "loop " else "" in
- fprintf fmt "@\n%sallocates@ \\nothing;" prefix
- | FreeAlloc(f,a) ->
- let prefix = if isloop then "loop " else "" in
- let pFreeAlloc kw fmt af =
- match af with
- | [] -> ()
- | _ -> fprintf fmt "@\n%s%s@ %a;" prefix kw (pp_list ~sep:",@ " print_lexpr) a
- in fprintf fmt "%a%a" (pFreeAlloc "frees") f (pFreeAlloc "allocates") a
+ | FreeAllocAny -> ()
+ | FreeAlloc([],[]) ->
+ let prefix = if isloop then "loop " else "" in
+ fprintf fmt "@\n%sallocates@ \\nothing;" prefix
+ | FreeAlloc(f,a) ->
+ let prefix = if isloop then "loop " else "" in
+ let pFreeAlloc kw fmt af =
+ match af with
+ | [] -> ()
+ | _ -> fprintf fmt "@\n%s%s@ %a;" prefix kw (pp_list ~sep:",@ " print_lexpr) a
+ in fprintf fmt "%a%a" (pFreeAlloc "frees") f (pFreeAlloc "allocates") a
let print_clause name fmt e = fprintf fmt "@\n%s@ %a;" name print_lexpr e
-let print_post fmt (k,e) =
+let print_post fmt (k,e) =
print_clause (Cil_printer.get_termination_kind_name k) fmt e
let print_behavior fmt bhv =
@@ -423,7 +423,7 @@ let print_behavior fmt bhv =
(pp_list ~pre:"" ~suf:"" print_post) bhv.b_post_cond
(print_allocation ~isloop:false) bhv.b_allocation
print_assigns bhv.b_assigns
- (* TODO: prints extensions *)
+(* TODO: prints extensions *)
let print_variant fmt (v,cmp) =
fprintf fmt "%a%a;" print_lexpr v
@@ -443,28 +443,28 @@ let print_spec fmt spec =
let print_loop_pragma fmt p =
match p with
- Unroll_specs l -> fprintf fmt "UNROLL@ %a" (pp_list ~sep:",@ " print_lexpr) l
- | Widen_hints l ->
- fprintf fmt "WIDEN_HINTS@ %a" (pp_list ~sep:",@ " print_lexpr) l
- | Widen_variables l ->
- fprintf fmt "WIDEN_VARIABLES@ %a" (pp_list ~sep:",@ " print_lexpr) l
+ Unroll_specs l -> fprintf fmt "UNROLL@ %a" (pp_list ~sep:",@ " print_lexpr) l
+ | Widen_hints l ->
+ fprintf fmt "WIDEN_HINTS@ %a" (pp_list ~sep:",@ " print_lexpr) l
+ | Widen_variables l ->
+ fprintf fmt "WIDEN_VARIABLES@ %a" (pp_list ~sep:",@ " print_lexpr) l
let print_slice_pragma fmt p =
match p with
- | SPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
- | SPctrl -> pp_print_string fmt "ctrl"
- | SPstmt -> pp_print_string fmt "stmt"
+ | SPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
+ | SPctrl -> pp_print_string fmt "ctrl"
+ | SPstmt -> pp_print_string fmt "stmt"
let print_impact_pragma fmt p =
match p with
- | IPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
- | IPstmt -> pp_print_string fmt "stmt"
+ | IPexpr e -> fprintf fmt "expr@ %a" print_lexpr e
+ | IPstmt -> pp_print_string fmt "stmt"
let print_pragma fmt p =
match p with
- Loop_pragma p -> fprintf fmt "loop@ pragma@ %a;" print_loop_pragma p
- | Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
- | Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
+ Loop_pragma p -> fprintf fmt "loop@ pragma@ %a;" print_loop_pragma p
+ | Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
+ | Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
let print_extension fmt (name, ext) =
fprintf fmt "%s %a" name (pp_list ~sep:",@ " print_lexpr) ext
@@ -474,26 +474,26 @@ let print_code_annot fmt ca =
(pp_list ~pre:"for@ " ~sep:",@ " ~suf:":@ " pp_print_string) fmt bhvs
in
match ca with
- AAssert(bhvs,e) ->
- fprintf fmt "%aassert@ %a;" print_behaviors bhvs print_lexpr e
- | AStmtSpec (bhvs,s) ->
- fprintf fmt "%a%a"
- print_behaviors bhvs
- print_spec s
- | AInvariant (bhvs,loop,e) ->
- fprintf fmt "%a%ainvariant@ %a;"
- print_behaviors bhvs (pp_cond loop) "loop@ " print_lexpr e
- | AVariant e -> fprintf fmt "loop@ variant@ %a;" print_variant e
- | AAssigns (bhvs,a) ->
- fprintf fmt "%aloop@ %a" print_behaviors bhvs print_assigns a
- | AAllocation (bhvs,fa) ->
- fprintf fmt "%a%a" print_behaviors bhvs (print_allocation ~isloop:true) fa
- | APragma p -> print_pragma fmt p
- | AExtended (bhvs, is_loop, e) ->
- fprintf fmt "%a%s%a"
- print_behaviors bhvs
- (if is_loop then " loop " else "")
- print_extension e
+ AAssert(bhvs,e) ->
+ fprintf fmt "%aassert@ %a;" print_behaviors bhvs print_lexpr e
+ | AStmtSpec (bhvs,s) ->
+ fprintf fmt "%a%a"
+ print_behaviors bhvs
+ print_spec s
+ | AInvariant (bhvs,loop,e) ->
+ fprintf fmt "%a%ainvariant@ %a;"
+ print_behaviors bhvs (pp_cond loop) "loop@ " print_lexpr e
+ | AVariant e -> fprintf fmt "loop@ variant@ %a;" print_variant e
+ | AAssigns (bhvs,a) ->
+ fprintf fmt "%aloop@ %a" print_behaviors bhvs print_assigns a
+ | AAllocation (bhvs,fa) ->
+ fprintf fmt "%a%a" print_behaviors bhvs (print_allocation ~isloop:true) fa
+ | APragma p -> print_pragma fmt p
+ | AExtended (bhvs, is_loop, e) ->
+ fprintf fmt "%a%s%a"
+ print_behaviors bhvs
+ (if is_loop then " loop " else "")
+ print_extension e
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 27c8a438e07..a0b54818601 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -101,18 +101,18 @@ class printer_with_annot () = object (self)
print_spec <- false
method private current_kf = match self#current_function with
- | None -> assert false
- | Some vi -> Globals.Functions.get vi
+ | None -> assert false
+ | Some vi -> Globals.Functions.get vi
method private current_kinstr = match self#current_stmt with
- | None -> Kglobal
- | Some st -> Kstmt st
+ | None -> Kglobal
+ | Some st -> Kstmt st
method private current_sid = match self#current_stmt with
- | None -> assert false
- | Some st -> st.sid
+ | None -> assert false
+ | Some st -> st.sid
- method! private may_be_skipped s =
+ method! private may_be_skipped s =
super#may_be_skipped s && not (Annotations.has_code_annot s)
method private pretty_funspec fmt kf =
@@ -126,14 +126,14 @@ class printer_with_annot () = object (self)
method! private inline_block ctxt blk =
super#inline_block ctxt blk
- && (match blk.bstmts with
- | [] -> true
- | [ s ] ->
- not (Annotations.has_code_annot s && logic_printer_enabled)
- && (match s.skind with
- | Block blk -> self#inline_block ctxt blk
- | _ -> true)
- | _ :: _ -> false)
+ && (match blk.bstmts with
+ | [] -> true
+ | [ s ] ->
+ not (Annotations.has_code_annot s && logic_printer_enabled)
+ && (match s.skind with
+ | Block blk -> self#inline_block ctxt blk
+ | _ -> true)
+ | _ :: _ -> false)
method! varinfo fmt v =
if Kernel.is_debug_key_enabled Kernel.dkey_print_vid then begin
@@ -165,9 +165,9 @@ class printer_with_annot () = object (self)
declared_globs <- Cil_datatype.Varinfo.Set.add vi declared_globs;
(* pretty prints the spec, but not for built-ins*)
if not (Cil.Builtin_functions.mem vi.vname) then
- self#pretty_funspec fmt kf
+ self#pretty_funspec fmt kf
end
- with Not_found ->
+ with Not_found ->
());
print_spec <- false;
super#vdecl fmt vi;
@@ -176,8 +176,8 @@ class printer_with_annot () = object (self)
method! global fmt glob =
if Kernel.PrintComments.get () && Cil_printer.print_global glob then begin
let comments = Globals.get_comments_global glob in
- Pretty_utils.pp_list
- ~sep:"@\n" ~suf:"@\n"
+ Pretty_utils.pp_list
+ ~sep:"@\n" ~suf:"@\n"
(fun fmt s -> Format.fprintf fmt "/* %s */" s) fmt comments
end;
(* Out of tree global annotations are pretty printed before the first
@@ -216,15 +216,15 @@ class printer_with_annot () = object (self)
(* To debug location setting:
(let loc = fst (Cil_datatype.Stmt.loc s.skind) in
Format.fprintf fmt "/*Loc=%s:%d*/" loc.Lexing.pos_fname
- loc.Lexing.pos_lnum); *)
+ loc.Lexing.pos_lnum); *)
Format.pp_open_hvbox fmt 0;
(* print the labels *)
self#stmt_labels fmt s;
if Kernel.PrintComments.get () then begin
let comments = Globals.get_comments_stmt s in
if comments <> [] then
- Pretty_utils.pp_list ~sep:"@\n" ~suf:"@]@\n"
- (fun fmt s -> Format.fprintf fmt "@[/* %s */@]" s)
+ Pretty_utils.pp_list ~sep:"@\n" ~suf:"@]@\n"
+ (fun fmt s -> Format.fprintf fmt "@[/* %s */@]" s)
fmt comments
end;
if verbose || Kernel.is_debug_key_enabled Kernel.dkey_print_sid then
@@ -232,43 +232,43 @@ class printer_with_annot () = object (self)
(* print the annotations *)
if logic_printer_enabled then begin
let all_annot =
- List.sort
- Cil_datatype.Code_annotation.compare
- (Annotations.code_annot s)
+ List.sort
+ Cil_datatype.Code_annotation.compare
+ (Annotations.code_annot s)
in
let pGhost fmt s =
- let was_ghost = is_ghost in
- if not was_ghost && s.ghost then begin
+ let was_ghost = is_ghost in
+ if not was_ghost && s.ghost then begin
Format.fprintf fmt "%t %a "
(fun fmt -> self#pp_open_annotation ~pre:"@[/*@@" fmt)
self#pp_acsl_keyword "ghost";
is_ghost <- true
- end;
- self#stmtkind s.sattr next fmt s.skind;
- if not was_ghost && s.ghost then begin
+ end;
+ self#stmtkind s.sattr next fmt s.skind;
+ if not was_ghost && s.ghost then begin
self#pp_close_annotation ~suf:"@,*/@]" fmt;
is_ghost <- false;
- end
+ end
in
(match all_annot with
- | [] -> pGhost fmt s
- | [ a ] when Cil.is_skip s.skind && not s.ghost ->
- Format.fprintf fmt "@[<hv>@[%t@ %a@;<1 1>%t@]@ %a@]"
- (fun fmt -> self#pp_open_annotation ~block:false fmt)
- self#code_annotation a
- (fun fmt -> self#pp_close_annotation ~block:false fmt)
- (self#stmtkind s.sattr next) s.skind;
- | _ ->
- let loop_annot, stmt_annot =
- List.partition Logic_utils.is_loop_annot all_annot
- in
- self#annotations fmt stmt_annot;
- self#loop_annotations fmt loop_annot;
- pGhost fmt s)
+ | [] -> pGhost fmt s
+ | [ a ] when Cil.is_skip s.skind && not s.ghost ->
+ Format.fprintf fmt "@[<hv>@[%t@ %a@;<1 1>%t@]@ %a@]"
+ (fun fmt -> self#pp_open_annotation ~block:false fmt)
+ self#code_annotation a
+ (fun fmt -> self#pp_close_annotation ~block:false fmt)
+ (self#stmtkind s.sattr next) s.skind;
+ | _ ->
+ let loop_annot, stmt_annot =
+ List.partition Logic_utils.is_loop_annot all_annot
+ in
+ self#annotations fmt stmt_annot;
+ self#loop_annotations fmt loop_annot;
+ pGhost fmt s)
end else
self#stmtkind s.sattr next fmt s.skind;
Format.pp_close_box fmt ()
-
+
method! stmtkind sattr (next: stmt) fmt skind =
super#stmtkind sattr next fmt
begin
@@ -277,7 +277,7 @@ class printer_with_annot () = object (self)
when Kernel.PrintReturn.get () -> return
| _ -> skind
end
-
+
end (* class printer_with_annot *)
include Printer_builder.Make(struct class printer = printer_with_annot end)
@@ -302,11 +302,11 @@ 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.Label.pretty_ref := pp_label
let () = Cil_datatype.Compinfo.pretty_ref := pp_compinfo
let () = Cil_datatype.Fieldinfo.pretty_ref := (fun fmt f -> pp_varname fmt f.fname)
-let () = Cil_datatype.Builtin_logic_info.pretty_ref := pp_builtin_logic_info
+let () = Cil_datatype.Builtin_logic_info.pretty_ref := pp_builtin_logic_info
let () = Cil_datatype.Logic_type_info.pretty_ref := pp_logic_type_info
let () = Cil_datatype.Logic_ctor_info.pretty_ref := pp_logic_ctor_info
let () = Cil_datatype.Initinfo.pretty_ref := pp_initinfo
@@ -320,8 +320,8 @@ let () = Cil_datatype.Global.pretty_ref := pp_global
let () = Cil_datatype.Predicate.pretty_ref := pp_predicate
let () = Cil_datatype.Identified_predicate.pretty_ref := pp_identified_predicate
let () = Cil_datatype.Fundec.pretty_ref := pp_fundec
-
-
+
+
(*
Local Variables:
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 979b7389058..78de7bf3606 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -67,7 +67,7 @@ class type extensible_printer_type = object
method private current_function: varinfo option
(** @return the [varinfo] corresponding to the function being printed *)
-
+
method private current_behavior: funbehavior option
(** @return the [funbehavior] being pretty-printed. *)
@@ -107,7 +107,7 @@ class type extensible_printer_type = object
print sequences of instructions separated by comma *)
method private set_instr_terminator: string -> unit
-
+
method private opt_funspec: Format.formatter -> funspec -> unit
(* ******************************************************************* *)
@@ -149,9 +149,9 @@ class type extensible_printer_type = object
method ikind: Format.formatter -> ikind -> unit
method fkind: Format.formatter -> fkind -> unit
- method typ:
+ method typ:
?fundecl:varinfo ->
- (Format.formatter -> unit) option -> Format.formatter -> typ -> unit
+ (Format.formatter -> unit) option -> Format.formatter -> typ -> unit
(** Use of some type in some declaration. [fundecl] is the name of the
function which is declared with the corresponding type. The second
argument is used to print the declared element, or is None if we are just
@@ -164,7 +164,7 @@ class type extensible_printer_type = object
method attribute: Format.formatter -> attribute -> bool
(** Attribute. Also return an indication whether this attribute must be
printed inside the __attribute__ list or not. *)
-
+
method attributes: Format.formatter -> attributes -> unit
(** Attribute lists *)
@@ -172,9 +172,9 @@ class type extensible_printer_type = object
method compinfo: Format.formatter -> compinfo -> unit
method initinfo: Format.formatter -> initinfo -> unit
method fundec: Format.formatter -> fundec -> unit
-
- method line_directive:
+
+ method line_directive:
?forcefile:bool -> Format.formatter -> location -> unit
(** Print a line-number. This is assumed to come always on an empty line. If
the forcefile argument is present and is true then the file name will be
@@ -228,8 +228,8 @@ class type extensible_printer_type = object
method logic_constant: Format.formatter -> logic_constant -> unit
method logic_type:
- (Format.formatter -> unit) option -> Format.formatter -> logic_type
- -> unit
+ (Format.formatter -> unit) option -> Format.formatter -> logic_type
+ -> unit
method logic_type_def: Format.formatter -> logic_type_def -> unit
method model_info: Format.formatter -> model_info -> unit
method term_binop: Format.formatter -> binop -> unit
@@ -251,7 +251,7 @@ class type extensible_printer_type = object
method quantifiers: Format.formatter -> quantifiers -> unit
method predicate_node: Format.formatter -> predicate_node -> unit
method predicate: Format.formatter -> predicate -> unit
- method identified_predicate:
+ method identified_predicate:
Format.formatter -> identified_predicate -> unit
method behavior: Format.formatter -> funbehavior -> unit
method requires: Format.formatter -> identified_predicate -> unit
@@ -259,7 +259,7 @@ class type extensible_printer_type = object
method disjoint_behaviors: Format.formatter -> string list -> unit
method terminates: Format.formatter -> identified_predicate -> unit
- method post_cond:
+ method post_cond:
Format.formatter -> (termination_kind * identified_predicate) -> unit
(** pretty prints a post condition according to the exit kind it represents
@modify Boron-20100401 replaces [pEnsures] *)
@@ -309,8 +309,8 @@ class type extensible_printer_type = object
method without_annot:
'a.
(Format.formatter -> 'a -> unit) ->
- Format.formatter ->
- 'a ->
+ Format.formatter ->
+ 'a ->
unit
(** [self#without_annot printer fmt x] pretty prints [x] by using [printer],
without pretty-printing its function contracts and code annotations. *)
@@ -318,11 +318,11 @@ class type extensible_printer_type = object
method force_brace:
'a.
(Format.formatter -> 'a -> unit) ->
- Format.formatter ->
- 'a ->
+ Format.formatter ->
+ 'a ->
unit
-(** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
- but add some extra braces '\{' and '\}' which are hidden by default. *)
+ (** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
+ but add some extra braces '\{' and '\}' which are hidden by default. *)
end
@@ -342,25 +342,25 @@ type line_directive_style =
| Line_preprocessor_output (** Use # nnn directives (in gcc mode) *)
type state =
- { (** How to print line directives *)
- mutable line_directive_style: line_directive_style option;
- (** Whether we print something that will only be used as input to Cil's
- parser. In that case we are a bit more liberal in what we print. *)
- mutable print_cil_input: bool;
- (** Whether to print the CIL as they are, without trying to be smart and
- print nicer code. Normally this is false, in which case the pretty
- printer will turn the while(1) loops of CIL into nicer loops, will not
- print empty "else" blocks, etc. These is one case however in which if
- you turn this on you will get code that does not compile: if you use
- varargs the __builtin_va_arg function will be printed in its internal
- form. *)
- mutable print_cil_as_is: bool;
- (** The length used when wrapping output lines. Setting this variable to
- a large integer will prevent wrapping and make #line directives more
- accurate. *)
- mutable line_length: int;
- (** Emit warnings when truncating integer constants (default true) *)
- mutable warn_truncate: bool }
+ { (** How to print line directives *)
+ mutable line_directive_style: line_directive_style option;
+ (** Whether we print something that will only be used as input to Cil's
+ parser. In that case we are a bit more liberal in what we print. *)
+ mutable print_cil_input: bool;
+ (** Whether to print the CIL as they are, without trying to be smart and
+ print nicer code. Normally this is false, in which case the pretty
+ printer will turn the while(1) loops of CIL into nicer loops, will not
+ print empty "else" blocks, etc. These is one case however in which if
+ you turn this on you will get code that does not compile: if you use
+ varargs the __builtin_va_arg function will be printed in its internal
+ form. *)
+ mutable print_cil_as_is: bool;
+ (** The length used when wrapping output lines. Setting this variable to
+ a large integer will prevent wrapping and make #line directives more
+ accurate. *)
+ mutable line_length: int;
+ (** Emit warnings when truncating integer constants (default true) *)
+ mutable warn_truncate: bool }
(* ********************************************************************* *)
(** {2 Functions for pretty printing} *)
@@ -417,7 +417,7 @@ module type S_pp = sig
(** @since Oxygen-20120901 *)
val pp_term_lval: Format.formatter -> term_lval -> unit
- val pp_term_lhost: Format.formatter -> term_lhost -> unit
+ val pp_term_lhost: Format.formatter -> term_lhost -> unit
val pp_logic_var: Format.formatter -> logic_var -> unit
val pp_logic_type: Format.formatter -> logic_type -> unit
val pp_identified_term: Format.formatter -> identified_term -> unit
@@ -449,7 +449,7 @@ module type S_pp = sig
val pp_loop_allocation: Format.formatter -> allocation -> unit
(** @since Oxygen-20120901 *)
- val pp_post_cond:
+ val pp_post_cond:
Format.formatter -> (termination_kind * identified_predicate) -> unit
(* ********************************************************************* *)
@@ -463,26 +463,26 @@ module type S_pp = sig
val without_annot:
(Format.formatter -> 'a -> unit) ->
- Format.formatter ->
- 'a ->
+ Format.formatter ->
+ 'a ->
unit
(** [without_annot printer fmt x] pretty prints [x] by using [printer],
without pretty-printing its function contracts and code annotations. *)
val force_brace:
(Format.formatter -> 'a -> unit) ->
- Format.formatter ->
- 'a ->
+ Format.formatter ->
+ 'a ->
unit
- (** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
- but add some extra braces '\{' and '\}' which are hidden by default. *)
+ (** [self#force_brace printer fmt x] pretty prints [x] by using [printer],
+ but add some extra braces '\{' and '\}' which are hidden by default. *)
end
module type S = sig
include S_pp
-
+
(* ********************************************************************* *)
(** {3 Extensible printer} *)
(* ********************************************************************* *)
@@ -507,17 +507,17 @@ module type S = sig
This is how this function should be used:
-{[
-module PrinterClassDeferred (X: Printer.PrinterClass) = struct
- class printer : Printer.extensible_printer = object(self)
- inherit X.printer as super
- (* Override the standard methods *)
- end
-end
-let () = Printer.update_printer
- (module PrinterClassDeferred: Printer.PrinterExtension)
-]}
-*)
+ {[
+ module PrinterClassDeferred (X: Printer.PrinterClass) = struct
+ class printer : Printer.extensible_printer = object(self)
+ inherit X.printer as super
+ (* Override the standard methods *)
+ end
+ end
+ let () = Printer.update_printer
+ (module PrinterClassDeferred: Printer.PrinterExtension)
+ ]}
+ *)
val current_printer: unit -> (module PrinterClass)
(** Returns the current pretty-printer, with all the extensions added
diff --git a/src/kernel_services/ast_printing/printer_builder.ml b/src/kernel_services/ast_printing/printer_builder.ml
index c4a67ab0372..bba10960ff4 100644
--- a/src/kernel_services/ast_printing/printer_builder.ml
+++ b/src/kernel_services/ast_printing/printer_builder.ml
@@ -95,7 +95,7 @@ end
module Make
- (P: sig class printer: unit -> Printer_api.extensible_printer_type end) =
+ (P: sig class printer: unit -> Printer_api.extensible_printer_type end) =
struct
module type PrinterClass = sig
diff --git a/src/kernel_services/ast_printing/printer_builder.mli b/src/kernel_services/ast_printing/printer_builder.mli
index 6d6f3a670c6..1816cc0ec42 100644
--- a/src/kernel_services/ast_printing/printer_builder.mli
+++ b/src/kernel_services/ast_printing/printer_builder.mli
@@ -24,14 +24,14 @@
object obtained by (P()) *)
module Make_pp
- (P: sig val printer: unit -> Printer_api.extensible_printer_type end):
+ (P: sig val printer: unit -> Printer_api.extensible_printer_type end):
Printer_api.S_pp
-(** Build a full pretty-printer from a pretty-printing class.
+(** Build a full pretty-printer from a pretty-printing class.
@since Fluorine-20130401 *)
module Make
- (P: sig class printer: unit -> Printer_api.extensible_printer_type end):
+ (P: sig class printer: unit -> Printer_api.extensible_printer_type end):
Printer_api.S
(*
--
GitLab