CExprEval (gillian.Engine.CExprEval)

module CStore : sig ... end

exception TypeError of string

exception EvaluationError of string

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

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

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

val binary_num_thing : 
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (float -> float -> float) ->
  string ->
  Gillian.Concrete.Values.t

val binary_int_thing : 
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (Z.t -> Z.t -> Z.t) ->
  string ->
  Gillian.Concrete.Values.t

val binary_int_bool_thing : 
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (Z.t -> Z.t -> bool) ->
  string ->
  Gillian.Concrete.Values.t

val binary_num_bool_thing : 
  Gillian.Concrete.Values.t ->
  Gillian.Concrete.Values.t ->
  (float -> float -> bool) ->
  string ->
  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