JSSpec (gillian-js.Jslogic.JSSpec)

type st = {

pre : JSAsrt.t;
post : JSAsrt.t list;
flag : Gillian.Gil_syntax.Flag.t;
label : (string * Jslogic.JSLogicCommon.SS.t) option;

}

type t = {

name : string;
params : string list;
sspecs : st list;

}

val js2jsil_st : 
  JSAsrt.t ->
  JSAsrt.t list ->
  JSLogicCommon.cc_tbl_type ->
  JSLogicCommon.vis_tbl_type ->
  JSLogicCommon.pre_fun_tbl_type ->
  string ->
  string list ->
  Jsil_syntax.Asrt.t * Jsil_syntax.Asrt.t list