JSAsrt (gillian-js.Jslogic.JSAsrt)

type pt =

| And of pt * pt
| Or of pt * pt
| Not of pt
| True
| False
| Eq of JSExpr.t * JSExpr.t
| Less of JSExpr.t * JSExpr.t
| LessEq of JSExpr.t * JSExpr.t
| StrLess of JSExpr.t * JSExpr.t
| ForAll of (string * Gillian.Gil_syntax.Type.t) list * pt
| SetMem of JSExpr.t * JSExpr.t
| SetSub of JSExpr.t * JSExpr.t
| IsInt of JSExpr.t

type t =

| Pure of pt
| Star of t * t
| PointsTo of JSExpr.t * JSExpr.t * JSExpr.t
| MetaData of JSExpr.t * JSExpr.t
| Emp
| Pred of string * JSExpr.t list
| Types of (string * Gillian.Gil_syntax.Type.t) list
| Scope of string * JSExpr.t
| VarSChain of string * string * JSExpr.t * JSExpr.t
| OSChains of string * JSExpr.t * string * JSExpr.t
| Closure of (string * JSExpr.t) list * (string * JSExpr.t) list
| SChain of string * JSExpr.t
| EmptyFields of JSExpr.t * JSExpr.t

val star : t list -> t

val js2jsil_pure : 
  Jslogic.JSLogicCommon.Expr.t option ->
  pt ->
  Jslogic.JSLogicCommon.Expr.t

val js2jsil : 
  string option ->
  JSLogicCommon.cc_tbl_type ->
  JSLogicCommon.vis_tbl_type ->
  JSLogicCommon.pre_fun_tbl_type ->
  Jslogic.JSLogicCommon.Expr.t option ->
  t ->
  Jsil_syntax.Asrt.t

val errors_assertion : unit -> Jsil_syntax.Asrt.t

val js2jsil_tactic : 
  JSLogicCommon.cc_tbl_type ->
  JSLogicCommon.vis_tbl_type ->
  JSLogicCommon.pre_fun_tbl_type ->
  string ->
  string ->
  t ->
  Jsil_syntax.Asrt.t