Ail_linking (soteria-c.Soteria_c_lib.Ail

module Sym_set = Symbol_std.Set

module Sym_map = Symbol_std.Map

type extern_idmap =
  (Cerb_frontend.Symbol.identifier, Cerb_frontend.AilSyntax.sigma_extern_id)
    Pmap.map

type redundant_globs =
  (Cerb_frontend.Symbol.sym * Cerb_frontend.Symbol.sym) list

exception LinkError of string

val link_extern : 
  extern_idmap ->
  extern_idmap ->
  Ail_tys.extern_symmap ->
  (extern_idmap * redundant_globs * Ail_tys.extern_symmap, string)
    Stdlib.result

val set_of_bindings : Cerb_frontend.AilSyntax.bindings -> Sym_set.t

val free_syms_expr : 
  Sym_set.t ->
  'a Cerb_frontend.AilSyntax.expression ->
  Sym_set.t

val free_syms_stmt : 
  Sym_set.t ->
  'a Cerb_frontend.AilSyntax.statement ->
  Sym_set.t

val free_syms_object_definition : 
  Sym_set.t ->
  'a Cerb_frontend.AilSyntax.expression ->
  Sym_set.t

val merge_globs : 
  'a Cerb_frontend.AilSyntax.sigma_object_definition list ->
  'a Cerb_frontend.AilSyntax.sigma_object_definition list ->
  (Cerb_frontend.Symbol.sym * Cerb_frontend.Symbol.sym) list ->
  ((Sym_map.key * 'a Cerb_frontend.AilSyntax.expression) list, string)
    Stdlib.result

val link_main : 'a option -> 'a option -> ('a option, string) Stdlib.result

val has_cn_stuff : 'a Cerb_frontend.AilSyntax.sigma -> bool

val link_aux : 
  Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.ail_program ->
  Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.ail_program ->
  Ail_tys.extern_symmap ->
  (Ail_tys.linked_program, string) Stdlib.result

val compress_union_find : Ail_tys.extern_symmap -> Ail_tys.extern_symmap

val link : 
  Ail_tys.program list ->
  (Ail_tys.linked_program,
    [> `LinkError of string ] * 'a Soteria.Terminal.Call_trace.t)
    Stdlib.result