apronAnalysis.apron.ml

(** {{!RelationAnalysis} Relational integer value analysis} using {!Apron} domains ([apron]). *)

open Analyses

include RelationAnalysis

let spec_module: (module MCPSpec) Lazy.t =
  lazy (
    let module Man = (val ApronDomain.get_manager ()) in
    let module AD = ApronDomain.D2 (Man) in
    let module Priv = (val RelationPriv.get_priv ()) in
    let module Spec =
    struct
      include SpecFunctor (Priv) (AD) (ApronPrecCompareUtil.Util)
      let name () = "apron"
    end
    in
    let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas"
    in
    if (narrowing_gas > 0) then
      let module Narrowed =
      struct
        module PolyhedraChainParams: Printable.ChainParams =
        struct
          let n () = narrowing_gas
          let names = string_of_int
        end
        include NarrowingGas.DLifter (Spec) (PolyhedraChainParams)
        module A = Spec.A
        let access = Spec.access
        let name = Spec.name
      end
      in
      (module Narrowed)
    else
      (module Spec)
  )

let get_spec (): (module MCPSpec) =
  Lazy.force spec_module

let after_config () =
  let module Spec = (val get_spec ()) in
  MCP.register_analysis (module Spec : MCPSpec);
  GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())

let _ =
  AfterConfig.register after_config


let () =
  Printexc.register_printer
    (function
      | Apron.Manager.Error e ->
        Apron.Manager.print_exclog Format.str_formatter e;
        Some (Printf.sprintf "Apron.Manager.Error\n %s" (Format.flush_str_formatter ()))
      | _ -> None (* for other exceptions *)
    )