Gilgen (gillian-c.Cgil

type symbol

val is_def_sym : symbol -> bool

val sym_name : symbol -> string

type compilation_data = {

genv_defs : (string * Global_env.def) list;
genv_init_cmds : string Gillian.Gil_syntax.Cmd.t list;
symbols : symbol list;

}

Data exported during compilation and used during linking.

val make_init_proc : 
  string Gillian.Gil_syntax.Cmd.t list ->
  (Gillian.Gil_syntax.Annot.Basic.t, string) Gillian.Gil_syntax.Proc.t

val trans_program : 
  ?exec_mode:Cgil_lib.CConstants.Exec_mode.t ->
  ?gil_annot:Gil_logic_gen.gil_annots ->
  clight_prog:Compcert.Clight.program ->
  filepath:string ->
  mangled_syms:(string, string) Stdlib.Hashtbl.t ->
  Compcert.Csharpminor.program ->
  (Gillian.Gil_syntax.Annot.Basic.t, string) Gillian.Gil_syntax.Prog.t
  * compilation_data

val trans_program_with_annots : 
  exec_mode:Cgil_lib.CConstants.Exec_mode.t ->
  clight_prog:Compcert.Clight.program ->
  filepath:string ->
  mangled_syms:(string, string) Stdlib.Hashtbl.t ->
  Compcert.Csharpminor.program ->
  CLogic.CProg.t ->
  (Gillian.Gil_syntax.Annot.Basic.t, string) Gillian.Gil_syntax.Prog.t
  * compilation_data