Module JS_Parser.Syntax

exception CannotHappen
type comparison_op =
  1. | Equal
  2. | NotEqual
  3. | TripleEqual
  4. | NotTripleEqual
  5. | Lt
  6. | Le
  7. | Gt
  8. | Ge
  9. | In
  10. | InstanceOf
type arith_op =
  1. | Plus
  2. | Minus
  3. | Times
  4. | Div
  5. | Mod
  6. | Ursh
  7. | Lsh
  8. | Rsh
  9. | Bitand
  10. | Bitor
  11. | Bitxor
type bool_op =
  1. | And
  2. | Or
type bin_op =
  1. | Comparison of comparison_op
  2. | Arith of arith_op
  3. | Boolean of bool_op
type unary_op =
  1. | Not
  2. | TypeOf
  3. | Positive
  4. | Negative
  5. | Pre_Decr
  6. | Post_Decr
  7. | Pre_Incr
  8. | Post_Incr
  9. | Bitnot
  10. | Void
type var = string
type annotation_type =
  1. | Import
    (*

    Import a JSIL or GIL file

    *)
  2. | TopRequires
    (*

    Precondition of global

    *)
  3. | TopEnsures
    (*

    Normal postcondition of global

    *)
  4. | TopEnsuresErr
    (*

    Error postcondition of global

    *)
  5. | Requires
    (*

    Precondition of function

    *)
  6. | Ensures
    (*

    Normal postcondition of function

    *)
  7. | EnsuresErr
    (*

    Error postcondition of function

    *)
  8. | Id
    (*

    Function identifier

    *)
  9. | Codename
    (*

    Codename

    *)
  10. | Pred
    (*

    Predicate

    *)
  11. | OnlySpec
    (*

    Specification without function body

    *)
  12. | Invariant
  13. | Lemma
  14. | Tactic
    (*

    General tactic: fold, unfold, recursive unfold, assert, flash, callspec, and many more to come...

    *)
  15. | BiAbduce
    (*

    Bi-abduction indicator

    *)
  16. | Call
    (*

    Function call with substitution

    *)
  17. | JSIL_only
    (*

    Function called in JSIL only

    *)
type annotation = {
  1. annot_type : annotation_type;
  2. annot_formula : string;
}
type propname =
  1. | PropnameId of string
  2. | PropnameString of string
  3. | PropnameNum of float
type proptype =
  1. | PropbodyVal
  2. | PropbodyGet
  3. | PropbodySet
type exp = {
  1. exp_loc : Loc.t;
  2. exp_stx : exp_syntax;
  3. exp_annot : annotation list;
}
and exp_syntax =
  1. | Num of float
  2. | String of string
  3. | Label of string * exp
  4. | Null
  5. | Bool of bool
  6. | Var of var
  7. | If of exp * exp * exp option
  8. | While of exp * exp
  9. | DoWhile of exp * exp
  10. | VarDec of (var * exp option) list
  11. | This
  12. | Delete of exp
  13. | Comma of exp * exp
  14. | Unary_op of unary_op * exp
  15. | BinOp of exp * bin_op * exp
  16. | Access of exp * string
  17. | Call of exp * exp list
  18. | Assign of exp * exp
  19. | AssignOp of exp * arith_op * exp
  20. | FunctionExp of bool * string option * var list * exp
  21. | Function of bool * string option * var list * exp
  22. | New of exp * exp list
  23. | Obj of (propname * proptype * exp) list
  24. | Array of exp option list
  25. | CAccess of exp * exp
  26. | With of exp * exp
  27. | Skip
  28. | Throw of exp
  29. | Return of exp option
  30. | RegExp of string * string
  31. | For of exp option * exp option * exp option * exp
  32. | ForIn of exp * exp * exp
  33. | Break of string option
  34. | Continue of string option
  35. | Try of exp * (string * exp) option * exp option
  36. | Switch of exp * (switch_case * exp) list
  37. | Debugger
  38. | ConditionalOp of exp * exp * exp
  39. | Block of exp list
  40. | Script of bool * exp list
and switch_case =
  1. | Case of exp
  2. | DefaultCase
val mk_exp : exp_syntax -> Loc.t -> annotation list -> exp
val script_and_strict : exp_syntax -> bool