Revision 15c3e4e7
Added by LĂ©lio Brun almost 4 years ago
src/backends/C/c_backend_spec.ml | ||
---|---|---|
135 | 135 |
let preprocess_acsl machines = machines, [] |
136 | 136 |
|
137 | 137 |
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *) |
138 |
let pp_acsl_preamble fmt preamble = |
|
138 |
let pp_acsl_preamble fmt _preamble =
|
|
139 | 139 |
Format.fprintf fmt ""; |
140 | 140 |
() |
141 | 141 |
|
... | ... | |
224 | 224 |
pp_v |
225 | 225 |
fmt |
226 | 226 |
|
227 |
let pp_ite pp_c pp_t pp_f fmt (c, t, f) = |
|
228 |
fprintf fmt "%a @[<hov>? %a@ : %a@]" |
|
229 |
pp_c c |
|
230 |
pp_t t |
|
231 |
pp_f f |
|
232 |
|
|
227 | 233 |
let pp_machine_decl fmt (id, mem_type, var) = |
228 | 234 |
fprintf fmt "struct %s_%s %s" id mem_type var |
229 | 235 |
|
230 | 236 |
let pp_mem_ghost pp_mem pp_self ?i fmt (name, mem, self) = |
231 |
fprintf fmt "%s_ghost%a(%a, %a)"
|
|
237 |
fprintf fmt "%s_ghost%a(@[<hov>%a,@ %a@])"
|
|
232 | 238 |
name |
233 | 239 |
(pp_print_option pp_print_int) i |
234 | 240 |
pp_mem mem |
... | ... | |
236 | 242 |
|
237 | 243 |
let pp_mem_ghost' = pp_mem_ghost pp_print_string pp_print_string |
238 | 244 |
|
239 |
let pp_mem_init fmt (name, mem) = |
|
240 |
fprintf fmt "%s_init(%s)" name mem |
|
245 |
let pp_mem_init pp_mem fmt (name, mem) = |
|
246 |
fprintf fmt "%s_init(%a)" name pp_mem mem |
|
247 |
|
|
248 |
let pp_mem_init' = pp_mem_init pp_print_string |
|
241 | 249 |
|
242 | 250 |
let pp_var_decl fmt v = |
243 | 251 |
pp_print_string fmt v.var_id |
... | ... | |
245 | 253 |
let pp_ptr_decl fmt v = |
246 | 254 |
fprintf fmt "*%s" v.var_id |
247 | 255 |
|
248 |
let pp_mem_trans ?i fmt (m, mem_in, mem_out) = |
|
249 |
fprintf fmt "%s_trans%a(@[<h>%s, %a%s%a@])" |
|
250 |
m.mname.node_id |
|
256 |
let pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_input pp_output fmt |
|
257 |
(name, inputs, outputs, mem_in, mem_out) = |
|
258 |
fprintf fmt "%s_trans%a(@[<hov>%a,@ %a%a%a@])" |
|
259 |
name |
|
251 | 260 |
(pp_print_option pp_print_int) i |
252 |
mem_in |
|
261 |
pp_mem_in mem_in
|
|
253 | 262 |
(pp_print_list |
254 | 263 |
~pp_epilogue:pp_print_comma |
255 | 264 |
~pp_sep:pp_print_comma |
256 |
pp_var_decl) m.mstep.step_inputs
|
|
257 |
mem_out |
|
265 |
pp_input) inputs
|
|
266 |
pp_mem_out mem_out
|
|
258 | 267 |
(pp_print_list |
259 | 268 |
~pp_prologue:pp_print_comma |
260 | 269 |
~pp_sep:pp_print_comma |
261 |
pp_ptr_decl) m.mstep.step_outputs |
|
270 |
pp_output) outputs |
|
271 |
|
|
272 |
let pp_mem_trans ?i pp_mem_in pp_mem_out fmt (m, mem_in, mem_out) = |
|
273 |
pp_mem_trans_aux ?i pp_mem_in pp_mem_out pp_var_decl pp_ptr_decl fmt |
|
274 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, mem_in, mem_out) |
|
275 |
|
|
276 |
let pp_mem_trans' ?i fmt = pp_mem_trans ?i pp_print_string pp_print_string fmt |
|
262 | 277 |
|
263 | 278 |
let pp_nothing fmt () = |
264 | 279 |
pp_print_string fmt "\\nothing" |
... | ... | |
349 | 364 |
(print_machine_ghost_simulation_aux m |
350 | 365 |
(pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self) |
351 | 366 |
|
367 |
let print_machine_core_annotations dependencies fmt m = |
|
368 |
if not (fst (Machine_code_common.get_stateless_status m)) then |
|
369 |
let name = m.mname.node_id in |
|
370 |
let self = mk_self m in |
|
371 |
let mem = mk_mem m in |
|
372 |
fprintf fmt "%a@,%a@,%a%a" |
|
373 |
print_machine_ghost_struct m |
|
374 |
(print_machine_ghost_simulation_aux m pp_true ~i:0) () |
|
375 |
(pp_print_list_i |
|
376 |
~pp_epilogue:pp_print_cut |
|
377 |
~pp_open_box:pp_open_vbox0 |
|
378 |
(print_machine_ghost_simulation dependencies m)) |
|
379 |
m.mstep.step_instrs |
|
380 |
(print_machine_ghost_simulation_aux m |
|
381 |
(pp_mem_ghost' ~i:(List.length m.mstep.step_instrs))) (name, mem, self) |
|
382 |
|
|
352 | 383 |
let pp_at pp_p fmt (p, l) = |
353 | 384 |
fprintf fmt "\\at(%a, %s)" pp_p p l |
354 | 385 |
|
... | ... | |
357 | 388 |
let pp_at_pre pp_p fmt p = |
358 | 389 |
pp_at pp_p fmt (p, label_pre) |
359 | 390 |
|
391 |
module VarDecl = struct |
|
392 |
type t = var_decl |
|
393 |
let compare v1 v2 = compare v1.var_id v2.var_id |
|
394 |
end |
|
395 |
module VDSet = Set.Make(VarDecl) |
|
396 |
|
|
397 |
let pp_arrow_spec fmt () = |
|
398 |
let name = "_arrow" in |
|
399 |
let mem_in = "mem_in" in |
|
400 |
let mem_out = "mem_out" in |
|
401 |
let reg_first = "_reg", "_first" in |
|
402 |
let mem_in_first = mem_in, reg_first in |
|
403 |
let mem_out_first = mem_out, reg_first in |
|
404 |
let mem = "mem" in |
|
405 |
let self = "self" in |
|
406 |
fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a" |
|
407 |
(pp_spec_line (pp_ghost pp_print_string)) |
|
408 |
"struct _arrow_mem_ghost {struct _arrow_reg _reg;};" |
|
409 |
(pp_spec_cut |
|
410 |
(pp_predicate |
|
411 |
(pp_mem_init pp_machine_decl) |
|
412 |
(pp_equal |
|
413 |
(pp_access pp_access') |
|
414 |
pp_print_string))) |
|
415 |
((name, (name, "mem_ghost", mem_in)), |
|
416 |
(mem_in_first, "true")) |
|
417 |
(pp_spec_cut |
|
418 |
(pp_predicate |
|
419 |
(pp_mem_trans_aux |
|
420 |
pp_machine_decl pp_machine_decl pp_print_string pp_print_string) |
|
421 |
(pp_and |
|
422 |
(pp_equal |
|
423 |
pp_print_string |
|
424 |
(pp_access pp_access')) |
|
425 |
(pp_ite |
|
426 |
(pp_access pp_access') |
|
427 |
(pp_equal |
|
428 |
(pp_access pp_access') |
|
429 |
pp_print_string) |
|
430 |
(pp_equal |
|
431 |
(pp_access pp_access') |
|
432 |
(pp_access pp_access')))))) |
|
433 |
((name, [], ["_Bool out"], (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)), |
|
434 |
(("out", mem_in_first), |
|
435 |
(mem_in_first, (mem_out_first, "false"), (mem_out_first, mem_in_first)))) |
|
436 |
(pp_spec_cut |
|
437 |
(pp_predicate |
|
438 |
(pp_mem_ghost pp_machine_decl pp_machine_decl) |
|
439 |
(pp_equal |
|
440 |
(pp_access pp_access') |
|
441 |
(pp_indirect pp_access')))) |
|
442 |
((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)), |
|
443 |
((mem, reg_first), (self, reg_first))) |
|
444 |
|
|
360 | 445 |
module SrcMod = struct |
361 | 446 |
|
362 | 447 |
let pp_predicates dependencies fmt machines = |
363 | 448 |
fprintf fmt |
364 |
"%a%a" |
|
449 |
"%a@,%a%a%a" |
|
450 |
pp_arrow_spec () |
|
365 | 451 |
(pp_print_list |
366 | 452 |
~pp_open_box:pp_open_vbox0 |
367 | 453 |
~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */") |
... | ... | |
370 | 456 |
(pp_print_list |
371 | 457 |
~pp_open_box:pp_open_vbox0 |
372 | 458 |
~pp_sep:pp_print_cutcut |
373 |
~pp_prologue:(fun fmt () -> fprintf fmt |
|
374 |
"/* ACSL ghost simulations */@,%a" |
|
375 |
(pp_spec_line (pp_ghost pp_print_string)) |
|
376 |
"struct _arrow_mem_ghost {struct _arrow_reg _reg;};") |
|
459 |
~pp_prologue:(pp_print_endcut "/* ACSL ghost simulations */") |
|
377 | 460 |
(print_machine_ghost_simulations dependencies) |
378 | 461 |
~pp_epilogue:pp_print_cutcut) machines |
462 |
(pp_print_list |
|
463 |
~pp_open_box:pp_open_vbox0 |
|
464 |
~pp_sep:pp_print_cutcut |
|
465 |
~pp_prologue:(pp_print_endcut "/* ACSL core annotations */") |
|
466 |
(print_machine_core_annotations dependencies) |
|
467 |
~pp_epilogue:pp_print_cutcut) machines |
|
379 | 468 |
|
380 | 469 |
let pp_reset_spec fmt self m = |
381 | 470 |
let name = m.mname.node_id in |
... | ... | |
395 | 484 |
pp_machine_decl |
396 | 485 |
(pp_implies |
397 | 486 |
pp_mem_ghost' |
398 |
pp_mem_init))) |
|
487 |
pp_mem_init')))
|
|
399 | 488 |
((name, "mem_ghost", mem), |
400 | 489 |
((name, mem, self), (name, mem)))) |
401 | 490 |
fmt () |
... | ... | |
433 | 522 |
(pp_at_pre pp_mem_ghost') |
434 | 523 |
(pp_implies |
435 | 524 |
pp_mem_ghost' |
436 |
pp_mem_trans)))) |
|
525 |
pp_mem_trans'))))
|
|
437 | 526 |
((), |
438 | 527 |
((name, mem_in, self), |
439 | 528 |
((name, mem_out, self), |
440 | 529 |
(m, mem_in, mem_out))))) |
441 | 530 |
fmt () |
442 | 531 |
|
443 |
let pp_step_instr_spec m self fmt (i, instr) = |
|
532 |
let pp_step_instr_spec m self fmt (i, _instr) =
|
|
444 | 533 |
let name = m.mname.node_id in |
445 | 534 |
let mem_in = mk_mem_in m in |
446 | 535 |
let mem_out = mk_mem_out m in |
... | ... | |
456 | 545 |
(pp_at_pre pp_mem_ghost') |
457 | 546 |
(pp_implies |
458 | 547 |
(pp_mem_ghost' ~i:(i+1)) |
459 |
(pp_mem_trans ~i:(i+1))))))) |
|
548 |
(pp_mem_trans' ~i:(i+1)))))))
|
|
460 | 549 |
((), |
461 | 550 |
((name, mem_in, self), |
462 | 551 |
((name, mem_out, self), |
src/causality.ml | ||
---|---|---|
544 | 544 |
maybe removing shorter branches *) |
545 | 545 |
type disjoint_map = (ident, CISet.t) Hashtbl.t |
546 | 546 |
|
547 |
let pp_ciset fmt t = |
|
548 |
begin |
|
549 |
Format.fprintf fmt "{@ "; |
|
550 |
CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t; |
|
551 |
Format.fprintf fmt "}@." |
|
552 |
end |
|
547 |
let pp_ciset fmt t = let open Format in |
|
548 |
pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt |
|
549 |
(CISet.elements t) |
|
553 | 550 |
|
554 | 551 |
let clock_disjoint_map vdecls = |
555 | 552 |
let map = Hashtbl.create 23 in |
... | ... | |
602 | 599 |
end |
603 | 600 |
|
604 | 601 |
let pp_disjoint_map fmt map = |
605 |
begin |
|
606 |
Format.fprintf fmt "{ /* disjoint map */@."; |
|
607 |
Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; |
|
608 |
Format.fprintf fmt "}@." |
|
609 |
end |
|
602 |
Format.(fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }" |
|
603 |
(fun fmt -> |
|
604 |
Hashtbl.iter (fun k v -> |
|
605 |
fprintf fmt "@,%s # %a" |
|
606 |
k (pp_print_braced' Printers.pp_var_name) |
|
607 |
(CISet.elements v)) map)) |
|
610 | 608 |
end |
611 | 609 |
|
612 | 610 |
|
613 | 611 |
let pp_dep_graph fmt g = |
614 |
begin |
|
615 |
Format.fprintf fmt "{ /* graph */@."; |
|
616 |
IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g; |
|
617 |
Format.fprintf fmt "}@." |
|
618 |
end |
|
612 |
Format.fprintf fmt "@[<v 2>{ /* graph */%t@] }" |
|
613 |
(fun fmt -> |
|
614 |
IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "@,%s -> %s" s t) g) |
|
619 | 615 |
|
620 | 616 |
let pp_error fmt err = |
621 | 617 |
match err with |
src/checks/liveness.ml | ||
---|---|---|
141 | 141 |
end |
142 | 142 |
|
143 | 143 |
let pp_reuse_policy fmt policy = |
144 |
begin |
|
145 |
Format.fprintf fmt "{ /* reuse policy */@."; |
|
146 |
Hashtbl.iter (fun s t -> Format.fprintf fmt "%s -> %s@." s t.var_id) policy; |
|
147 |
Format.fprintf fmt "}@." |
|
148 |
end |
|
144 |
Format.(fprintf fmt "@[<v 2>{ /* reuse policy */%t@] }" |
|
145 |
(fun fmt -> Hashtbl.iter (fun s t -> fprintf fmt "@,%s -> %s" s t.var_id) policy)) |
|
149 | 146 |
|
150 | 147 |
let pp_context fmt ctx = |
151 |
begin |
|
152 |
Format.fprintf fmt "{ /*BEGIN context */@."; |
|
153 |
Format.fprintf fmt "eval=%a;@." Disjunction.pp_ciset ctx.evaluated; |
|
154 |
Format.fprintf fmt "graph=%a;@." pp_dep_graph ctx.dep_graph; |
|
155 |
Format.fprintf fmt "disjoint=%a;@." Disjunction.pp_disjoint_map ctx.disjoint; |
|
156 |
Format.fprintf fmt "policy=%a;@." pp_reuse_policy ctx.policy; |
|
157 |
Format.fprintf fmt "/* END context */ }@."; |
|
158 |
end |
|
148 |
Format.fprintf fmt |
|
149 |
"@[<v 2>{ /*BEGIN context */@,\ |
|
150 |
eval = %a;@,\ |
|
151 |
graph = %a;@,\ |
|
152 |
disjoint = %a;@,\ |
|
153 |
policy = %a;@,\ |
|
154 |
/* END context */ }@]" |
|
155 |
Disjunction.pp_ciset ctx.evaluated |
|
156 |
pp_dep_graph ctx.dep_graph |
|
157 |
Disjunction.pp_disjoint_map ctx.disjoint |
|
158 |
pp_reuse_policy ctx.policy |
|
159 | 159 |
|
160 | 160 |
(* computes the reusable dependencies of variable [var] in graph [g], |
161 | 161 |
once [var] has been evaluated |
... | ... | |
197 | 197 |
let locally_reusable v = |
198 | 198 |
IdentDepGraph.fold_pred (fun p r -> r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint) ctx.dep_graph v.var_id true in |
199 | 199 |
let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in |
200 |
Log.report ~level:7 (fun fmt -> Format.fprintf fmt "eligibles:%a@." Disjunction.pp_ciset eligibles); |
|
201 | 200 |
let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in |
202 |
Log.report ~level:7 (fun fmt -> Format.fprintf fmt "live:%a@." Disjunction.pp_ciset live);
|
|
203 |
try
|
|
204 |
let disjoint_live = Disjunction.CISet.inter disjoint live in
|
|
205 |
Log.report ~level:7 (fun fmt -> Format.fprintf fmt "disjoint live:%a@." Disjunction.pp_ciset disjoint_live);
|
|
206 |
let reuse = Disjunction.CISet.max_elt disjoint_live in
|
|
207 |
begin
|
|
208 |
IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
|
|
209 |
Hashtbl.add ctx.policy var.var_id reuse;
|
|
210 |
ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
|
|
211 |
(*Format.eprintf "%s reused by live@." var.var_id;*)
|
|
212 |
end
|
|
213 |
with Not_found ->
|
|
214 |
try
|
|
215 |
let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in
|
|
216 |
Log.report ~level:7 (fun fmt -> Format.fprintf fmt "dead:%a@." Disjunction.pp_ciset dead);
|
|
217 |
let reuse = Disjunction.CISet.choose dead in
|
|
218 |
begin
|
|
201 |
let disjoint_live = Disjunction.CISet.inter disjoint live in
|
|
202 |
let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in
|
|
203 |
Log.report ~level:7 (fun fmt ->
|
|
204 |
Format.fprintf fmt
|
|
205 |
"@[<v>\
|
|
206 |
eligibles : %a@,\
|
|
207 |
live : %a@,\
|
|
208 |
disjoint live: %a@,\
|
|
209 |
dead : %a@,@]"
|
|
210 |
Disjunction.pp_ciset eligibles
|
|
211 |
Disjunction.pp_ciset live
|
|
212 |
Disjunction.pp_ciset disjoint_live
|
|
213 |
Disjunction.pp_ciset dead);
|
|
214 |
begin try
|
|
215 |
let reuse = match Disjunction.CISet.max_elt_opt disjoint_live with
|
|
216 |
| Some reuse -> reuse
|
|
217 |
| None -> Disjunction.CISet.choose dead in
|
|
219 | 218 |
IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id; |
220 |
Hashtbl.add ctx.policy var.var_id reuse; |
|
221 |
ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated; |
|
222 |
(*Format.eprintf "%s reused by dead %s@." var.var_id reuse.var_id;*) |
|
223 |
end |
|
224 |
with Not_found -> |
|
225 |
begin |
|
226 |
Hashtbl.add ctx.policy var.var_id var; |
|
227 |
ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated; |
|
228 |
end |
|
219 |
Hashtbl.add ctx.policy var.var_id reuse |
|
220 |
with Not_found -> Hashtbl.add ctx.policy var.var_id var |
|
221 |
end; |
|
222 |
ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated |
|
229 | 223 |
|
230 | 224 |
let compute_reuse_policy node schedule disjoint g = |
231 |
let sort = ref schedule in |
|
232 | 225 |
let ctx = { evaluated = Disjunction.CISet.empty; |
233 |
dep_graph = g; |
|
234 |
disjoint = disjoint; |
|
235 |
policy = Hashtbl.create 23; } in |
|
236 |
while !sort <> [] |
|
237 |
do |
|
238 |
Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx); |
|
239 |
let heads = List.map (fun v -> get_node_var v node) (List.hd !sort) in |
|
240 |
Log.report ~level:6 (fun fmt -> Format.fprintf fmt "NEW HEADS:"); |
|
241 |
List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq (get_node_eq head.var_id node))) heads; |
|
242 |
Log.report ~level:6 (fun fmt -> Format.fprintf fmt "@."); |
|
243 |
Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_DEPENDENCIES@."); |
|
244 |
compute_dependencies heads ctx; |
|
245 |
Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx); |
|
246 |
Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_REUSE@."); |
|
247 |
List.iter (compute_reuse node ctx heads) heads; |
|
248 |
(*compute_evaluated heads ctx;*) |
|
249 |
List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "reuse %s instead of %s@." (Hashtbl.find ctx.policy head.var_id).var_id head.var_id)) heads; |
|
250 |
sort := List.tl !sort; |
|
251 |
done; |
|
226 |
dep_graph = g; |
|
227 |
disjoint = disjoint; |
|
228 |
policy = Hashtbl.create 23; } in |
|
229 |
List.iter (fun heads -> |
|
230 |
let heads = List.map (fun v -> get_node_var v node) heads in |
|
231 |
Log.report ~level:6 (fun fmt -> |
|
232 |
Format.(fprintf fmt |
|
233 |
"@[<v>@[<v 2>new context:@,%a@]@,NEW HEADS:%a@,COMPUTE_DEPENDENCIES@,@]" |
|
234 |
pp_context ctx |
|
235 |
(pp_print_list |
|
236 |
~pp_open_box:pp_open_hbox |
|
237 |
~pp_sep:pp_print_space |
|
238 |
(fun fmt head -> |
|
239 |
fprintf fmt "%s (%a)" |
|
240 |
head.var_id Printers.pp_node_eq |
|
241 |
(get_node_eq head.var_id node))) |
|
242 |
heads)); |
|
243 |
compute_dependencies heads ctx; |
|
244 |
Log.report ~level:6 (fun fmt -> |
|
245 |
Format.fprintf fmt "@[<v>@[<v 2>new context:@,%a@]@,COMPUTE_REUSE@,@]" pp_context ctx); |
|
246 |
List.iter (compute_reuse node ctx heads) heads; |
|
247 |
(*compute_evaluated heads ctx;*) |
|
248 |
Log.report ~level:6 (fun fmt -> |
|
249 |
Format.(fprintf fmt "@[<v>%a@,@]" |
|
250 |
(pp_print_list |
|
251 |
~pp_open_box:pp_open_vbox0 |
|
252 |
(fun fmt head -> fprintf fmt "reuse %s instead of %s" |
|
253 |
(Hashtbl.find ctx.policy head.var_id).var_id head.var_id)) |
|
254 |
heads))) |
|
255 |
schedule; |
|
252 | 256 |
IdentDepGraph.clear ctx.dep_graph; |
253 | 257 |
ctx.policy |
254 | 258 |
|
src/log.ml | ||
---|---|---|
9 | 9 |
(* *) |
10 | 10 |
(********************************************************************) |
11 | 11 |
|
12 |
let report ?plugin:(modulename="") ?(verbose_level=Options.verbose_level) ~level:level p = |
|
12 |
let report |
|
13 |
?plugin:(modulename="") |
|
14 |
?(verbose_level=Options.verbose_level) |
|
15 |
~level:level p = |
|
13 | 16 |
if !verbose_level >= level then |
14 |
begin |
|
15 |
if modulename="" then |
|
16 |
Format.eprintf "%t@?" p |
|
17 |
else |
|
18 |
Format.eprintf "[%s] @[%t@]@?" modulename p |
|
19 |
end |
|
17 |
if modulename="" then |
|
18 |
Format.eprintf "%t@?" p |
|
19 |
else |
|
20 |
Format.eprintf "[%s] @[%t@]@?" modulename p |
|
20 | 21 |
|
21 | 22 |
(* Local Variables: *) |
22 | 23 |
(* compile-command:"make -C .." *) |
src/utils/utils.ml | ||
---|---|---|
278 | 278 |
let pp_print_cpar fmt () = pp_print_string fmt ")" |
279 | 279 |
let pp_print_obrace fmt () = pp_print_string fmt "{" |
280 | 280 |
let pp_print_cbrace fmt () = pp_print_string fmt "}" |
281 |
let pp_print_opar' fmt () = pp_print_string fmt "( " |
|
282 |
let pp_print_cpar' fmt () = pp_print_string fmt " )" |
|
283 |
let pp_print_obrace' fmt () = pp_print_string fmt "{ " |
|
284 |
let pp_print_cbrace' fmt () = pp_print_string fmt " }" |
|
281 | 285 |
|
282 | 286 |
let pp_print_comma fmt () = fprintf fmt ",@ " |
283 | 287 |
let pp_print_semicolon fmt () = fprintf fmt ";@ " |
... | ... | |
337 | 341 |
~pp_cl:pp_print_cbrace |
338 | 342 |
~pp_sep |
339 | 343 |
|
344 |
let pp_print_braced' ?(pp_sep=pp_print_comma) = |
|
345 |
pp_print_list |
|
346 |
~pp_op:pp_print_obrace' |
|
347 |
~pp_cl:pp_print_cbrace' |
|
348 |
~pp_sep |
|
340 | 349 |
end |
341 | 350 |
|
342 | 351 |
let fprintf_list ?(eol:('a, formatter, unit) format = "") ~sep:sep f fmt l = |
Also available in: Unified diff
generic ACSL spec generation