Core (gillian-c.Cgil_lib.Constr.Core)

val pred : 
  LActions.ga ->
  Gillian.Gil_syntax.Expr.t list ->
  Gillian.Gil_syntax.Expr.t list ->
  Gillian.Gil_syntax.Asrt.atom

val single : 
  loc:Gillian.Gil_syntax.Expr.t ->
  ofs:Gillian.Gil_syntax.Expr.t ->
  chunk:Chunk.t ->
  sval:Gillian.Gil_syntax.Expr.t ->
  perm:Compcert.Memtype.permission option ->
  Gillian.Gil_syntax.Asrt.atom

val array : 
  loc:Gillian.Gil_syntax.Expr.t ->
  ofs:Gillian.Gil_syntax.Expr.t ->
  chunk:Chunk.t ->
  size:Gillian.Gil_syntax.Expr.t ->
  sval_arr:Gillian.Gil_syntax.Expr.t ->
  perm:Compcert.Memtype.permission option ->
  Gillian.Gil_syntax.Asrt.atom

val hole : 
  loc:Gillian.Gil_syntax.Expr.t ->
  low:Gillian.Gil_syntax.Expr.t ->
  high:Gillian.Gil_syntax.Expr.t ->
  perm:Compcert.Memtype.permission option ->
  Gillian.Gil_syntax.Asrt.atom

val zeros : 
  loc:Gillian.Gil_syntax.Expr.t ->
  low:Gillian.Gil_syntax.Expr.t ->
  high:Gillian.Gil_syntax.Expr.t ->
  perm:Compcert.Memtype.permission option ->
  Gillian.Gil_syntax.Asrt.atom

val bounds : 
  loc:Gillian.Gil_syntax.Expr.t ->
  low:Gillian.Gil_syntax.Expr.t ->
  high:Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Asrt.atom

val freed : loc:Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Asrt.atom