Gil_logic_gen (gillian-c.Cgil_lib.Gil_logic

module Str_set = Gillian.Utils.Containers.SS

module CoreP = Constr.Core

val id_of_string : string -> Compcert.Camlcoq.atom

val true_name : Compcert.Camlcoq.atom -> string

val loc_param_name : string

val ofs_param_name : string

val pred_name_of_struct : string -> string

val rec_pred_name_of_struct : string -> string

val opt_rec_pred_name_of_struct : string -> string

val fresh_lvar : ?fname:string -> unit -> string

val split3_expr_comp : 
  ('a list * 'b list * 'c) list ->
  'a list * 'b list * 'c list

val (++) : 
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t

val to_assrt_of_gen_form : 
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Asrt.atom

val (#==) : 
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Asrt.atom

val types : 
  Gillian.Gil_syntax.Type.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Asrt.atom

type gil_annots = {

preds : Gillian.Gil_syntax.Pred.t list;
specs : Gillian.Gil_syntax.Spec.t list;
onlyspecs : Gillian.Gil_syntax.Spec.t list;
lemmas : Gillian.Gil_syntax.Lemma.t list;
bispecs : Gillian.Gil_syntax.BiSpec.t list;
cenv : Compcert.Ctypes.composite_env;
imports : (string * bool) list;

}

val empty : gil_annots

val get_structs_not_annot : 
  Compcert.Ctypes.composite_definition list ->
  Str_set.elt list

val access_mode_by_value : Compcert.Ctypes.coq_type -> Chunk.t option

val assert_of_member : 
  Compcert.Ctypes.composite_env ->
  Compcert.Ctypes.members ->
  Compcert.Camlcoq.atom ->
  Compcert.Ctypes.coq_type ->
  Gillian.Gil_syntax.Asrt.atom list

val assert_of_hole : (Z.t * Z.t) -> Gillian.Gil_syntax.Asrt.atom

val gen_pred_of_struct : 
  Compcert.Ctypes.composite Compcert.Maps.PTree.tree ->
  gil_annots ->
  string ->
  gil_annots

val trans_binop : CLogic.CBinOp.t -> Gillian.Gil_syntax.BinOp.t

val trans_unop : CLogic.CUnOp.t -> Gillian.Gil_syntax.UnOp.t

val trans_nop : CLogic.CNOp.t -> Gillian.Gil_syntax.NOp.t

val trans_simpl_expr : CLogic.CSimplExpr.t -> Gillian.Gil_syntax.Expr.t

val trans_sval : 
  CLogic.CSVal.t ->
  Gillian.Gil_syntax.Asrt.t
  * Gillian.Gil_syntax.Var.t list
  * Gillian.Gil_syntax.Expr.t

val trans_expr : 
  CLogic.CExpr.t ->
  Gillian.Gil_syntax.Asrt.t
  * Gillian.Gil_syntax.Var.t list
  * Gillian.Gil_syntax.Expr.t

Returns assertions that are necessary to define the expression, the created variable for binding when necessary, and the used expression

val trans_form : 
  CLogic.CFormula.t ->
  Gillian.Gil_syntax.Asrt.t
  * Gillian.Gil_syntax.Var.t list
  * Gillian.Gil_syntax.Expr.t

val malloc_chunk_asrt : 
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  Z.t ->
  Gillian.Gil_syntax.Asrt.atom

val trans_constr : 
  ?fname:'a ->
  typ:CLogic.CAssert.points_to_type ->
  gil_annots ->
  CLogic.CExpr.t ->
  CLogic.CConstructor.t ->
  Gillian.Gil_syntax.Asrt.atom list

val trans_asrt : 
  fname:'a ->
  ann:gil_annots ->
  CLogic.CAssert.t ->
  Gillian.Gil_syntax.Asrt.atom list

val trans_lcmd : 
  fname:'a ->
  ann:gil_annots ->
  CLogic.CLCmd.t ->
  [ `Invariant of Gillian.Gil_syntax.SLCmd.t
  | `Normal of Gillian.Gil_syntax.LCmd.t list ]

val trans_asrt_annot : 
  CLogic.assert_annot ->
  Gillian.Gil_syntax.Asrt.atom list * (string * string list)

val trans_abs_pred : 
  filepath:string ->
  CLogic.CAbsPred.t ->
  Gillian.Gil_syntax.Pred.t

val trans_pred : 
  ann:gil_annots ->
  filepath:string ->
  CLogic.CPred.t ->
  Gillian.Gil_syntax.Pred.t

val add_trans_pred : string -> gil_annots -> CLogic.CPred.t -> gil_annots

val add_trans_abs_pred : 
  string ->
  gil_annots ->
  CLogic.CAbsPred.t ->
  gil_annots

val trans_sspec : 
  ann:gil_annots ->
  'a ->
  CLogic.CSpec.st ->
  Gillian.Gil_syntax.Spec.st

val trans_lemma : 
  ann:gil_annots ->
  filepath:string ->
  CLogic.CLemma.t ->
  Gillian.Gil_syntax.Lemma.t

val trans_spec : 
  ann:gil_annots ->
  ?only_spec:bool ->
  CLogic.CSpec.t ->
  Gillian.Gil_syntax.Spec.t

val add_trans_spec : gil_annots -> CLogic.CSpec.t -> gil_annots

val add_trans_only_spec : gil_annots -> CLogic.CSpec.t -> gil_annots

val add_trans_lemma : string -> gil_annots -> CLogic.CLemma.t -> gil_annots

val trans_annots : 
  'a Compcert.Ctypes.program ->
  CLogic.CProg.t ->
  string ->
  gil_annots

val get_clight_fun : 
  'a Compcert.Ctypes.program ->
  Compcert.BinNums.positive ->
  'a

val bit_size : Compcert.Ctypes.intsize -> int

val bounds : 
  Compcert.Ctypes.signedness ->
  int ->
  Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t

val predicate_from_triple : 
  (Gillian.Gil_syntax.Expr.t * Compcert.AST.typ * Compcert.Ctypes.coq_type) ->
  Gillian.Gil_syntax.Asrt.atom

val simple_predicate_from_triple : 
  (string * 'a * 'b) ->
  Gillian.Gil_syntax.Asrt.atom

val generate_bispec : 
  Compcert.Clight.coq_function Compcert.Ctypes.program ->
  string ->
  Compcert.BinNums.positive ->
  Compcert.Csharpminor.coq_function ->
  Gillian.Gil_syntax.BiSpec.t

val add_bispec : 
  gil_annots ->
  Compcert.Clight.coq_function Compcert.Ctypes.program ->
  string ->
  Compcert.BinNums.positive ->
  Compcert.Csharpminor.coq_function ->
  gil_annots