CExprEval (gillian.Engine.CExprEval)

module CStore : sig ... end

exception TypeError of string

exception EvaluationError of string

val evalerr : string -> 'a

val typeerr : ?msg:string -> string -> Gillian.Gil_syntax.Literal.t -> 'a

val as_str : ?msg:string -> Gillian.Gil_syntax.Literal.t -> string

val as_bool : ?msg:string -> Gillian.Gil_syntax.Literal.t -> bool

val as_int : ?msg:string -> Gillian.Gil_syntax.Literal.t -> Z.t

val as_num : ?msg:string -> Gillian.Gil_syntax.Literal.t -> float

val as_list : 
  ?msg:string ->
  Gillian.Gil_syntax.Literal.t ->
  Gillian.Gil_syntax.Literal.t list

val unary_int_thing : 
  ?msg:string ->
  Gillian.Concrete.Values.t ->
  (Z.t -> Z.t) ->
  Gillian.Concrete.Values.t

val unary_num_thing : 
  ?msg:string ->
  Gillian.Concrete.Values.t ->
  (float -> float) ->
  Gillian.Concrete.Values.t

val binary_num_thing : 
  ?msg:string ->
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (float -> float -> float) ->
  Gillian.Gil_syntax.Literal.t

val binary_int_thing : 
  ?msg:string ->
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (Z.t -> Z.t -> Z.t) ->
  Gillian.Gil_syntax.Literal.t

val binary_int_bool_thing : 
  ?msg:string ->
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (Z.t -> Z.t -> bool) ->
  Gillian.Gil_syntax.Literal.t

val binary_num_bool_thing : 
  ?msg:string ->
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (float -> float -> bool) ->
  Gillian.Gil_syntax.Literal.t

val evaluate_unop : 
  Gillian.Gil_syntax.UnOp.t ->
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t

val evaluate_binop : 
  CStore.t ->
  Gillian.Gil_syntax.BinOp.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Concrete.Values.t

val evaluate_nop : 
  Gillian.Gil_syntax.NOp.t ->
  Gillian.Concrete.Values.t list ->
  Gillian.Concrete.Values.t

val evaluate_elist : 
  CStore.t ->
  Gillian.Gil_syntax.Expr.t list ->
  Gillian.Concrete.Values.t

val evaluate_lstsub : 
  CStore.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Concrete.Values.t

val evaluate_expr : 
  CStore.t ->
  Gillian.Gil_syntax.Expr.t ->
  Gillian.Concrete.Values.t