diff --git a/.Makefile.lint b/.Makefile.lint
index f213229e55714480b8766486a7538600f510672a..d8fa9b5fba9e21245a6e031ee37d63282566011a 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -101,8 +101,6 @@ 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
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index a0a4d8a5f593408da8aff26db007b1dad4f83a4d..a11da2374c6b44c88d7057ab12dc5a929e85e7f1 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -41,17 +41,17 @@ 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
+ 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
@@ -64,32 +64,32 @@ let pp_allocation kloc fmt (allocation:identified_term list) =
else
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 =
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
@@ -98,9 +98,9 @@ let pp_bhv fmt bhv =
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
@@ -156,21 +156,21 @@ let pp_kinstr kloc fmt = function
let pp_predicate fmt = function
| PKRequires bhv ->
- Format.fprintf fmt "Pre-condition%a" pp_bhv bhv
+ Format.fprintf fmt "Pre-condition%a" pp_bhv bhv
| PKAssumes bhv ->
- Format.fprintf fmt "Assumption%a" pp_bhv 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
@@ -239,8 +239,8 @@ let rec pp_prop kfopt kiopt kloc fmt = function
(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
+ bhv.b_name
+ (pp_opt kiopt (pp_kinstr kloc)) ki
| IPComplete(_,ki,active, bs) ->
Format.fprintf fmt "Complete behaviors%a%a%a"
pp_bhvs bs
@@ -345,18 +345,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
@@ -416,13 +416,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
@@ -435,8 +435,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]
diff --git a/src/kernel_services/ast_printing/description.mli b/src/kernel_services/ast_printing/description.mli
index 02b1ea479eef6d4c1174fd8e2bb51393d9284250..08c578f325304e09db5fe1f5f42a5ca3dcefa87a 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 ','. *)