package codex

You can search for identifiers within the package.

in-package search v0.2.0

The Codex library for building static analysers based on abstract interpretation

Install

dune-project

Dependency

codex.top Edit opam file Versions (1)

Authors

Maintainers

M

Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz

md5=bc7266a140c6886add673ede90e335d3

sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/src/codex.codex_log/codex_log.ml.html

Source file `codex_log.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
(**************************************************************************)
(*  This file is part of the Codex semantics library.                     *)
(*                                                                        *)
(*  Copyright (C) 2013-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

type category = string
let register_category x = x

module type S = sig
  val result:  ('a, Format.formatter, unit) format -> 'a  
  val warning:  ('a, Format.formatter, unit) format -> 'a
  val error:  ('a, Format.formatter, unit) format -> 'a
  val feedback:  ('a, Format.formatter, unit) format -> 'a  
  val performance_warning:  ('a, Format.formatter, unit) format -> 'a
  val imprecision_warning:  ('a, Format.formatter, unit) format -> 'a    
  (* val debug: ?level:int -> ?category:string -> ('a, Format.formatter, unit) format -> 'a *)
  val fatal: ('a, Format.formatter, unit, 'b) format4 -> 'a
end


module Default:S = struct
  let logwith x = Format.kfprintf (fun fmt ->
      Format.pp_print_newline fmt ();
      Format.pp_print_flush fmt ()
    ) Format.err_formatter x
  ;;

  let warning = logwith
  let error = logwith
  let result = logwith    
  let _alarm a = logwith "%s" (Operator.Alarm.show a)
  let feedback = logwith
  let performance_warning = logwith
  let imprecision_warning = logwith
  let fatal str = Format.kfprintf (fun fmt ->
      Format.pp_print_newline fmt ();
      Format.pp_print_flush fmt ();
      assert false)
      Format.err_formatter str ;;
end

let r = ref (module Default:S);;
let register (module X:S) = r:= (module X);;

(* Does not print anything (except fatal errors). *)
module Null:S = struct
  let logwith x = Format.ikfprintf  (fun fmt ->
      Format.pp_print_newline fmt ();
      Format.pp_print_flush fmt ()
    ) Format.err_formatter x
  ;;

  let warning = logwith
  let error = logwith
  let result = logwith    
  let feedback = logwith
  let performance_warning = logwith
  let imprecision_warning = logwith
  let fatal str = Format.kfprintf (fun fmt ->
      Format.pp_print_newline fmt ();
      Format.pp_print_flush fmt ();
      assert false)
      Format.err_formatter str ;;
end


module Dynamic:S = struct
  (* let register_category = let module X:S = (val !r) in X.register_category;; *)
  let warning fmt = let module X:S = (val !r) in X.warning fmt;;
  let error fmt = let module X:S = (val !r) in X.error fmt;;
  let result fmt = let module X:S = (val !r) in X.result fmt;;  
  let performance_warning fmt = let module X:S = (val !r) in X.performance_warning fmt;;
  let imprecision_warning fmt = let module X:S = (val !r) in X.imprecision_warning fmt;;
  (* let debug ?level ?category fmt = *)
  (*   let _ = level and _ = category in *)
  (*   let module X:S = (val !r) in X.debug ?category fmt;; *)
  let fatal fmt = let module X:S = (val !r) in X.fatal fmt;;
  let feedback fmt = let module X:S = (val !r) in X.feedback fmt;;  
end


module Tracelog_Instance = Tracelog.Make(struct let category = "codex" end);;

module Tracelog_Log:S = struct
  let result fmt = Format.kasprintf (fun str -> Tracelog_Instance.notice (fun m -> m "%s" str)) fmt;;  
  let feedback fmt = Format.kasprintf (fun str -> Tracelog_Instance.info (fun m -> m "%s" str)) fmt;;
  let error fmt = Format.kasprintf (fun str -> Tracelog_Instance.error (fun m -> m "%s" str)) fmt;;
  let warning fmt = Format.kasprintf (fun str -> Tracelog_Instance.warning (fun m -> m "%s" str)) fmt;;
  let performance_warning = warning
  let imprecision_warning = warning
  let fatal fmt = Format.kasprintf (fun str -> Tracelog_Instance.fatal (fun m -> m "%s" str)) fmt;;
end


module Used = Dynamic

include Used