path: root/abstract/relational_apron.ml

open Apron
open Util
open Environment_domain

module RelationalDomain : ENVIRONMENT_DOMAIN = struct

    (* manager *)
    type man = Polka.loose Polka.t
    let manager = Polka.manager_alloc_loose ()

    (* abstract elements *)
    type t = man Abstract1.t

    (* implementation *)
    let init = Abstract1.top manager (Environment.make  [||] [||])
    let bottom = Abstract1.bottom manager (Environment.make [||] [||])
    let is_bot = Abstract1.is_bottom manager

    let addvar x id = x (* TODO *)
    let rmvar x id = x (* TODO *)
    let vars x =
        List.map Var.to_string @@
        Array.to_list @@ snd @@ Environment.vars @@ Abstract1.env x

    let assign x id e = x (* TODO *)
    let compare x e1 e2 = x (* TODO *)

    let join = Abstract1.join manager
    let meet = Abstract1.meet manager
    let widen = Abstract1.widening manager

    let subset = Abstract1.is_leq manager

    let var_str x idl = "" (* TODO *)

end