Kratos2 C API Reference

API for Kratos2.

Data structures and special values

All the data structures in the API are opaque. They can only be accessed using API functions.

Data structures

• kratos_env: Kratos environment.
• kratos_sexp: Kratos S-expression (used to represent symbols and generic structured data).
• kratos_type: Kratos type.
• kratos_expr: Kratos expression.
• kratos_function: Kratos function.
• kratos_program: Kratos program.
• kratos_trace: Kratos counterexample trace.
• kratos_config: Kratos configuration for verification.

Error checking

#define KRATOS_ERROR_OBJ(o)

Error checking macro for kratos opaque data structures.

Enumeratives

• kratos_type_tag: Kratos type tags.

  Value	Description
  KRATOS_TYPE_ERROR	error
  KRATOS_TYPE_VOID	void type
  KRATOS_TYPE_LABEL	label type
  KRATOS_TYPE_BOOL	Boolean type
  KRATOS_TYPE_INT	mathematical integer type
  KRATOS_TYPE_REAL	real (actually rational) type
  KRATOS_TYPE_SYMBOL	generic symbolic type
  KRATOS_TYPE_BV	fixed-size bit-vector type
  KRATOS_TYPE_FP	IEEE floating-point type
  KRATOS_TYPE_MAP	mapping type
  KRATOS_TYPE_FUNCTION	function type
  KRATOS_TYPE_ENUM	symbolic enum type

• kratos_expr_tag: Kratos expression tags.

  Value	Description
  KRATOS_EXPR_ERROR	error
  KRATOS_EXPR_VAR	variable
  KRATOS_EXPR_CONST	constant
  KRATOS_EXPR_OP	operation
  KRATOS_EXPR_CALL	function call
  KRATOS_EXPR_ASSIGN	assignment
  KRATOS_EXPR_ASSUME	assumption
  KRATOS_EXPR_TYPECAST	type conversion
  KRATOS_EXPR_SEQ	sequence of statements
  KRATOS_EXPR_JUMP	jump
  KRATOS_EXPR_LABEL	label
  KRATOS_EXPR_HAVOC	havoc
  KRATOS_EXPR_CONDJUMP	conditional jump

• kratos_op_tag: Kratos operation tags.

  Value	Description
  KRATOS_OP_ERROR	error
  KRATOS_OP_ADD	addition
  KRATOS_OP_SUB	subtraction
  KRATOS_OP_MUL	multiplication
  KRATOS_OP_NEG	negation
  KRATOS_OP_DIV	division
  KRATOS_OP_REM	remainder
  KRATOS_OP_LSHIFT	left shift
  KRATOS_OP_RSHIFT	right shift
  KRATOS_OP_BITAND	bitwise and
  KRATOS_OP_BITOR	bitwise or
  KRATOS_OP_BITXOR	bitwise xor
  KRATOS_OP_BITNOT	bitwise complement
  KRATOS_OP_EQUAL	equality
  KRATOS_OP_AND	logical and
  KRATOS_OP_OR	logical or
  KRATOS_OP_NOT	logical not
  KRATOS_OP_LE	less or equal
  KRATOS_OP_LT	less than
  KRATOS_OP_GE	greater or equal
  KRATOS_OP_GT	greater than
  KRATOS_OP_FLOOR	floor
  KRATOS_OP_ISFINITE	test whether a float is finite
  KRATOS_OP_ISINF	test whether a float is infinite
  KRATOS_OP_ISNAN	test whether a float is NaN
  KRATOS_OP_ISNORMAL	test whether a float is normal
  KRATOS_OP_ISSUBNORMAL	test whether a float is subnormal
  KRATOS_OP_ISZERO	test whether a float is zero
  KRATOS_OP_MAPGET	map read
  KRATOS_OP_MAPSET	map write
  KRATOS_OP_ITE	if-then-else

• kratos_result: Kratos result.

  Value	Description
  KRATOS_RESULT_ERROR	error
  KRATOS_RESULT_UNKNOWN	unknown
  KRATOS_RESULT_SAFE	safe
  KRATOS_RESULT_UNSAFE	unsafe

• kratos_verification_method: Kratos verification method.

  Value	Description
  KRATOS_VERIFICATION_MODEL_CHECKING	(symbolic) model checking
  KRATOS_VERIFICATION_SYMBOLIC_EXECUTION	symbolic execution
  KRATOS_VERIFICATION_SIMULATION	(random) simulation

• kratos_visit_status: Kratos status for the callback passed to kratos_visit_expr().

  Value	Description
  KRATOS_VISIT_PROCESS	continue visiting
  KRATOS_VISIT_ABORT	abort the visit
  KRATOS_VISIT_SKIP	skip this expression and its children

Callback functions

• typedef kratos_visit_status(*)(kratos_env e, kratos_expr x, bool preorder, void *user_data) kratos_visit_callback
  Callback function to visit an expression with kratos_visit_expr().
  This callback function gets called by the visitor for each visited subexpression. The preorder flag tells whether the function is called before or after visiting the children. The return value of this function determines how the visit should continue (see kratos_visit_status). Note that the x expression should not be unreferenced. user_data is a opaque pointer to arbitrary data.

• typedef kratos_expr(*)(kratos_env e, kratos_expr v, kratos_sexp tag, void *user_data) kratos_symexec_constraint_provider
  Custom constraint provider for symbolic execution.

• typedef bool(*)(kratos_env e, kratos_sexp id, size_t key_size, kratos_expr *key, size_t val_size, kratos_expr *val, void *user_data) kratos_symexec_object_monitor
  Custom object monitor for symbolic execution.

function kratos_free

void kratos_free(
    void * mem
)

Function for deallocating the memory accessible by pointers returned by Kratos.

function kratos_get_version

char * kratos_get_version(
    void 
)

Gets the current Kratos version.

Return: A version string, which must be deallocated by the user with kratos_free().

function kratos_last_error_message

const char * kratos_last_error_message(
    kratos_env e
)

Retrieves the last error message generated while operating in the given enviroment.

Parameters:

• e The environment in which the error occurred.

Return: A pointer to the last error message generated.

function kratos_create_env

kratos_env kratos_create_env(
    void 
)

Creates a new Kratos environment.

Return: A new environment. Use KRATOS_ERROR_OBJ() to check for errors.

function kratos_destroy_env

void kratos_destroy_env(
    kratos_env e
)

Destroys the given environment.

Operations on S-expressions (sexps)

function kratos_nil

kratos_sexp kratos_nil(
    kratos_env e
)

Creates a nil sexp.

function kratos_cons

kratos_sexp kratos_cons(
    kratos_env e,
    kratos_sexp a,
    kratos_sexp b
)

Creates a cons sexp.

function kratos_symbol

kratos_sexp kratos_symbol(
    kratos_env e,
    const char * value
)

Creates a symbol sexp.

function kratos_sexp_is_nil

bool kratos_sexp_is_nil(
    kratos_env e,
    kratos_sexp s
)

Test for nil sexps.

function kratos_sexp_is_symbol

bool kratos_sexp_is_symbol(
    kratos_env e,
    kratos_sexp s
)

Test for symbol sexps.

function kratos_sexp_car

kratos_sexp kratos_sexp_car(
    kratos_env e,
    kratos_sexp s
)

Retrieve the car of a cons sexp.

Return: A borrowed reference (i.e. the result should not be unreferenced).

function kratos_sexp_cdr

kratos_sexp kratos_sexp_cdr(
    kratos_env e,
    kratos_sexp s
)

Retrieve the cdr of a cons sexp.

Return: A borrowed reference.

function kratos_sexp_ref

bool kratos_sexp_ref(
    kratos_env e,
    kratos_sexp s
)

Increase the refcount of the given sexp.

Return: false in case of errors.

function kratos_sexp_unref

bool kratos_sexp_unref(
    kratos_env e,
    kratos_sexp s
)

Decrease the refcount of the given sexp.

Return: false in case of errors.

function kratos_symbol_get_value

char * kratos_symbol_get_value(
    kratos_env e,
    kratos_sexp s
)

Get the value of a symbol expression.

Return: a newly allocated string, which must be freed with kratos_free(), or NULL on error.

function kratos_symbol_get_id

size_t kratos_symbol_get_id(
    kratos_env e,
    kratos_sexp s
)

Get the id of the given symbol sexp.

Return: 0 on error.

Types creation and manipulation

function kratos_type_ref

bool kratos_type_ref(
    kratos_env e,
    kratos_type t
)

Increase the refcount of the given type.

Return: false on error.

function kratos_type_unref

bool kratos_type_unref(
    kratos_env e,
    kratos_type t
)

Decrease the refcount of the given type.

Return: false on error.

function kratos_type_get_tag

kratos_type_tag kratos_type_get_tag(
    kratos_env e,
    kratos_type t
)

Get the tag of the given type.

function kratos_symbol_type_get_name

kratos_sexp kratos_symbol_type_get_name(
    kratos_env e,
    kratos_type t
)

Get the name of the given symbol type.

Return: A borrowed reference.

function kratos_bv_type_get_bits

size_t kratos_bv_type_get_bits(
    kratos_env e,
    kratos_type t
)

Get the bit-width of the given bit-vector type.

Return: 0 on error.

function kratos_bv_type_is_signed

bool kratos_bv_type_is_signed(
    kratos_env e,
    kratos_type t
)

Get the signedness of the given bit-vector type.

function kratos_fp_type_get_bits

size_t kratos_fp_type_get_bits(
    kratos_env e,
    kratos_type t
)

Get the bit-width of the given float type.

Return: 0 on error.

function kratos_fp_type_get_exponent

size_t kratos_fp_type_get_exponent(
    kratos_env e,
    kratos_type t
)

Get the exponent size of the given float type.

function kratos_fp_type_get_mantissa

size_t kratos_fp_type_get_mantissa(
    kratos_env e,
    kratos_type t
)

Get the mantissa size of the given float type.

function kratos_map_type_get_index

kratos_type kratos_map_type_get_index(
    kratos_env e,
    kratos_type t
)

Get the index component of the given map type.

Return: A borrowed reference.

function kratos_map_type_get_element

kratos_type kratos_map_type_get_element(
    kratos_env e,
    kratos_type t
)

Get the element component of the given map type.

Return: A borrowed reference.

function kratos_function_type_get_num_args

size_t kratos_function_type_get_num_args(
    kratos_env e,
    kratos_type t
)

Get the number of arguments of the given function type.

function kratos_function_type_get_num_returns

size_t kratos_function_type_get_num_returns(
    kratos_env e,
    kratos_type t
)

Get the number of return values of the given function type.

function kratos_function_type_get_args

kratos_type * kratos_function_type_get_args(
    kratos_env e,
    kratos_type t
)

Get the array of arguments of the given function type.

Return: An array of borrowed references (which must be deallocated with kratos_free()), or NULL on error

function kratos_function_type_get_returns

kratos_type * kratos_function_type_get_returns(
    kratos_env e,
    kratos_type t
)

Get the array of return types of the given function type.

Return: An array of borrowed references (which must be deallocated with kratos_free()), or NULL on error

function kratos_enum_type_get_num_values

size_t kratos_enum_type_get_num_values(
    kratos_env e,
    kratos_type t
)

Get the number of values of the given enum type.

function kratos_enum_type_get_values

kratos_sexp * kratos_enum_type_get_values(
    kratos_env e,
    kratos_type t
)

Get the array of values of the given enum type.

Return: An array of borrowed references (which must be deallocated with kratos_free()), or NULL on error

function kratos_enum_type_is_value

bool kratos_enum_type_is_value(
    kratos_env e,
    kratos_type t,
    kratos_sexp v
)

Checks whether the given symbol is a valid value for the given enum type.

function kratos_void_type

kratos_type kratos_void_type(
    kratos_env e
)

Create a new void type.

function kratos_label_type

kratos_type kratos_label_type(
    kratos_env e
)

Create a new label type.

function kratos_int_type

kratos_type kratos_int_type(
    kratos_env e
)

Create a new int type.

function kratos_real_type

kratos_type kratos_real_type(
    kratos_env e
)

Create a new real type.

function kratos_symbol_type

kratos_type kratos_symbol_type(
    kratos_env e,
    kratos_sexp name
)

Create a new symbolc type.

function kratos_bv_type

kratos_type kratos_bv_type(
    kratos_env e,
    size_t bits,
    bool is_signed
)

Create a new bit-vector type.

function kratos_fp_type

kratos_type kratos_fp_type(
    kratos_env e,
    size_t exponent,
    size_t mantissa
)

Create a new float type type.

function kratos_map_type

kratos_type kratos_map_type(
    kratos_env e,
    kratos_type index,
    kratos_type element
)

Create a new map type.

function kratos_function_type

kratos_type kratos_function_type(
    kratos_env e,
    size_t num_args,
    kratos_type * args,
    size_t num_ret,
    kratos_type * ret
)

Create a new function type.

function kratos_enum_type

kratos_type kratos_enum_type(
    kratos_env e,
    size_t num_values,
    kratos_sexp * values
)

Create a new enum type.

Expressions creation and manipulation

function kratos_expr_ref

bool kratos_expr_ref(
    kratos_env e,
    kratos_expr x
)

Increase the refcount of the given expression.

Return: false in case of errors.

function kratos_expr_unref

bool kratos_expr_unref(
    kratos_env e,
    kratos_expr x
)

Decrease the refcount of the given expression.

Return: false in case of errors.

function kratos_expr_get_tag

kratos_expr_tag kratos_expr_get_tag(
    kratos_env e,
    kratos_expr x
)

Get the tag of the given expression.

function kratos_expr_get_type

kratos_type kratos_expr_get_type(
    kratos_env e,
    kratos_expr x
)

Get the type of the given expression.

Return: A borrowed reference.

function kratos_var_expr_get_var

kratos_sexp kratos_var_expr_get_var(
    kratos_env e,
    kratos_expr x
)

Get the var name of the given var expression.

Return: A borrowed reference.

function kratos_const_expr_get_value

kratos_sexp kratos_const_expr_get_value(
    kratos_env e,
    kratos_expr x
)

Get the value of the given const expression.

Return: A borrowed reference.

function kratos_op_expr_get_tag

kratos_op_tag kratos_op_expr_get_tag(
    kratos_env e,
    kratos_expr x
)

Get op tag of the given op expression.

function kratos_op_expr_get_num_args

size_t kratos_op_expr_get_num_args(
    kratos_env e,
    kratos_expr x
)

Get the number of arguments of the given op expression.

function kratos_op_expr_get_args

kratos_expr * kratos_op_expr_get_args(
    kratos_env e,
    kratos_expr x
)

Get the list of arguments of the given op expression.

Return: A list of borrowed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_call_expr_get_function

kratos_expr kratos_call_expr_get_function(
    kratos_env e,
    kratos_expr x
)

Get the function of the given call expression.

Return: A borrowed reference.

function kratos_call_expr_get_num_args

size_t kratos_call_expr_get_num_args(
    kratos_env e,
    kratos_expr x
)

Get the number of arguments of the given call expression.

function kratos_call_expr_get_args

kratos_expr * kratos_call_expr_get_args(
    kratos_env e,
    kratos_expr x
)

Get the list of arguments of the given call expression.

Return: A list of borrowed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_call_expr_get_num_returns

size_t kratos_call_expr_get_num_returns(
    kratos_env e,
    kratos_expr x
)

Get the number of return vars of the given call expression.

function kratos_call_expr_get_returns

kratos_expr * kratos_call_expr_get_returns(
    kratos_env e,
    kratos_expr x
)

Get the list of return vars of the given call expression.

Return: A list of borrowed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_assign_expr_get_var

kratos_expr kratos_assign_expr_get_var(
    kratos_env e,
    kratos_expr x
)

Get the var that is the lhs of the given assign expression.

Return: A borrwed reference.

function kratos_assign_expr_get_value

kratos_expr kratos_assign_expr_get_value(
    kratos_env e,
    kratos_expr x
)

Get the value that is the rhs of the given assign expression.

Return: A borrwed reference.

function kratos_assume_expr_get_cond

kratos_expr kratos_assume_expr_get_cond(
    kratos_env e,
    kratos_expr x
)

Get the condition of the given assume expression.

Return: A borrowed reference.

function kratos_typecast_expr_get_expr

kratos_expr kratos_typecast_expr_get_expr(
    kratos_env e,
    kratos_expr x
)

Get the child expression of the given typecast expression.

Return: A borrowed reference.

function kratos_typecast_expr_is_bitcast

bool kratos_typecast_expr_is_bitcast(
    kratos_env e,
    kratos_expr x
)

Check whether the given typecast expression is a bitcast.

function kratos_seq_expr_get_num_args

size_t kratos_seq_expr_get_num_args(
    kratos_env e,
    kratos_expr x
)

Get the number of arguments of the given seq expression.

function kratos_seq_expr_get_args

kratos_expr * kratos_seq_expr_get_args(
    kratos_env e,
    kratos_expr x
)

Get the list of arguments of the given seq expression.

Return: A list of borrowed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_jump_expr_get_num_args

size_t kratos_jump_expr_get_num_args(
    kratos_env e,
    kratos_expr x
)

Get the number of arguments of the given jump expression.

function kratos_jump_expr_get_args

kratos_expr * kratos_jump_expr_get_args(
    kratos_env e,
    kratos_expr x
)

Get the list of arguments of the given jump expression.

Return: A list of borrowed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_label_expr_get_name

kratos_sexp kratos_label_expr_get_name(
    kratos_env e,
    kratos_expr x
)

Get the name of the given label expression.

Return: A borrowed reference.

function kratos_havoc_expr_get_var

kratos_expr kratos_havoc_expr_get_var(
    kratos_env e,
    kratos_expr x
)

Get the target of the given havoc expression.

Return: A borrowed reference.

function kratos_condjump_expr_get_cond

kratos_expr kratos_condjump_expr_get_cond(
    kratos_env e,
    kratos_expr x
)

Get the condition of the given condjump expression.

Return: A borrowed reference.

function kratos_condjump_expr_get_target

kratos_expr kratos_condjump_expr_get_target(
    kratos_env e,
    kratos_expr x
)

Get the target of the given condjump expression.

Return: A borrowed reference.

function kratos_var

kratos_expr kratos_var(
    kratos_env e,
    kratos_type t,
    kratos_sexp n
)

Create a new var expression.

Parameters:

• e The environment in which to operate.
• t The type of the expression.
• n The name of the variable.

Return: A new reference.

function kratos_const

kratos_expr kratos_const(
    kratos_env e,
    kratos_type t,
    kratos_sexp v
)

Create a new const expression.

Parameters:

• e The environment in which to operate.
• t The type of the expression.
• v The value of the constant.

Return: A new reference.

function kratos_op

kratos_expr kratos_op(
    kratos_env e,
    kratos_op_tag t,
    size_t num_args,
    kratos_expr * args
)

Create a new op expression.

Parameters:

• e The environment in which to operate.
• t The op tag.
• num_args The number of arguments.
• args The op arguments.

Return: A new reference.

function kratos_call

kratos_expr kratos_call(
    kratos_env e,
    kratos_expr f,
    size_t num_args,
    kratos_expr * args,
    size_t num_ret,
    kratos_expr * ret
)

Create a new call expression.

Parameters:

• e The environment in which to operate.
• f The function to call.
• num_args The number of arguments.
• args The call arguments.
• num_ret The number of returns.
• ret The call return vars.

Return: A new reference.

function kratos_assign

kratos_expr kratos_assign(
    kratos_env e,
    kratos_expr l,
    kratos_expr r
)

Create a new assign expression.

Parameters:

• e The environment in which to operate.
• l The var to assign to.
• r The value to assign.

Return: A new reference.

function kratos_assume

kratos_expr kratos_assume(
    kratos_env e,
    kratos_expr c
)

Create a new assume expression.

Parameters:

• e The environment in which to operate.
• c The condition to assume.

Return: A new reference.

function kratos_typecast

kratos_expr kratos_typecast(
    kratos_env e,
    kratos_type t,
    kratos_expr x,
    bool is_bitcast
)

Create a new assume expression.

Parameters:

• e The environment in which to operate.
• c The condition to assume.

Return: A new reference.

function kratos_seq

kratos_expr kratos_seq(
    kratos_env e,
    size_t num_args,
    kratos_expr * args
)

Create a new sequence expression.

Parameters:

• e The environment in which to operate.
• num_args The number of arguments.
• args The arguments.

Return: A new reference.

function kratos_jump

kratos_expr kratos_jump(
    kratos_env e,
    size_t num_args,
    kratos_expr * args
)

Create a new sequence expression.

Parameters:

• e The environment in which to operate.
• num_args The number of arguments.
• args The arguments (must be labels).

Return: A new reference.

function kratos_label

kratos_expr kratos_label(
    kratos_env e,
    kratos_sexp n
)

Create a new label expression.

Parameters:

• e The environment in which to operate.
• n The name of the label.

Return: A new reference.

function kratos_havoc

kratos_expr kratos_havoc(
    kratos_env e,
    kratos_expr v
)

Create a new havoc expression.

Parameters:

• e The environment in which to operate.
• v The var to havoc.

Return: A new reference.

function kratos_condjump

kratos_expr kratos_condjump(
    kratos_env e,
    kratos_expr c,
    kratos_expr t
)

Create a new condjump expression.

Parameters:

• e The environment in which to operate.
• c The condition for the jump.
• t The target label.

Return: A new reference.

function kratos_expr_set_annotation

bool kratos_expr_set_annotation(
    kratos_env e,
    kratos_expr x,
    kratos_sexp a
)

Set the annotation for the given expression.

Parameters:

• e The environment in which to operate.
• x The expression to annotate.
• a The annotation. Must be a list of cons cells of the form (key . value)

Return: false on error.

function kratos_expr_get_annotation

kratos_sexp kratos_expr_get_annotation(
    kratos_env e,
    kratos_expr x
)

Get the annotation for the given expression.

Parameters:

• e The environment in which to operate.
• x An expression.

Return: A new reference to the annotation for x, in the form of a list of (key . value) cons-cells. If x has no annotation, an error object is returned.

function kratos_visit_expr

bool kratos_visit_expr(
    kratos_env e,
    kratos_expr x,
    kratos_visit_callback cb,
    void * user_data
)

visits the given expression x, calling the callback cb for every subexpression.

Parameters:

• e The environment in which to operate.
• x The expression to visit.
• cb The callback function.
• user_data Generic data pointer which will be passed to cb. Can be anything, its value will not be interpreted.

Return: false on error.

Programs creation and manipulation

function kratos_new_function

kratos_function kratos_new_function(
    kratos_env e,
    kratos_sexp name,
    size_t num_params,
    kratos_expr * params,
    size_t num_ret,
    kratos_expr * ret,
    size_t num_locals,
    kratos_expr * locals,
    kratos_expr body
)

Create a new function.

Parameters:

• e The environment on which to operate.
• name The name of the function.
• num_params The number of formal parameters.
• params The formal parameters (must be var expressions).
• num_ret The number of return vars.
• ret The return vars (must be var expressions).
• num_locals The number of local variables.
• locals The local variables (must be var expressions).
• body The function body.

Return: The new function created. Use KRATOS_ERROR_OBJ() to check for errors.

function kratos_function_unref

bool kratos_function_unref(
    kratos_env e,
    kratos_function f
)

Decrease the refcount of the given function.

Return: false on error.

function kratos_function_get_num_params

size_t kratos_function_get_num_params(
    kratos_env e,
    kratos_function f
)

Get the number of parameters of the given function.

function kratos_function_get_num_locals

size_t kratos_function_get_num_locals(
    kratos_env e,
    kratos_function f
)

Get the number of local vars of the given function.

function kratos_function_get_num_returns

size_t kratos_function_get_num_returns(
    kratos_env e,
    kratos_function f
)

Get the number of return vars of the given function.

function kratos_function_get_name

kratos_sexp kratos_function_get_name(
    kratos_env e,
    kratos_function f
)

Get the name of the given function.

Return: A borrowed reference.

function kratos_function_get_params

kratos_expr * kratos_function_get_params(
    kratos_env e,
    kratos_function f
)

Get the array of parameters of the given function.

Return: An array of borrwed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_function_get_locals

kratos_expr * kratos_function_get_locals(
    kratos_env e,
    kratos_function f
)

Get the array of local vars of the given function.

Return: An array of borrwed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_function_get_returns

kratos_expr * kratos_function_get_returns(
    kratos_env e,
    kratos_function f
)

Get the array of return vars of the given function.

Return: An array of borrwed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_function_get_body

kratos_expr kratos_function_get_body(
    kratos_env e,
    kratos_function f
)

Get the body of the given function.

Return: A borrowed reference.

function kratos_function_get_type

kratos_type kratos_function_get_type(
    kratos_env e,
    kratos_function f
)

Get the type of the given function.

Return: A borrowed reference.

function kratos_function_set_annotation

bool kratos_function_set_annotation(
    kratos_env e,
    kratos_function f,
    kratos_sexp a
)

Set the annotation for the given function.

Return: false on error.

The annotation must be a list of (key, value) pairs.

function kratos_function_get_annotation

kratos_sexp kratos_function_get_annotation(
    kratos_env e,
    kratos_function f
)

Get the annotation for the given function.

Return: A new reference. If the function has no annotation, an error object will be returned.

function kratos_new_program

kratos_program kratos_new_program(
    kratos_env e,
    kratos_sexp entrypoint,
    size_t num_globals,
    kratos_expr * globals,
    size_t num_funcs,
    kratos_function * funcs,
    kratos_expr init
)

Create a new program.

Parameters:

• e The environment in which to operate.
• entrypoint The name of the entry point.
• num_globals The number of global vars.
• globals The list of global vars (must be var expressions).
• num_funcs The number of functions.
• funcs The list of functions.
• init The init expression (can be an error object if not needed).

Return: A new program.

function kratos_program_unref

bool kratos_program_unref(
    kratos_env e,
    kratos_program p
)

Decrease the refcount for the given program.

Return: false on error.

function kratos_program_get_num_functions

size_t kratos_program_get_num_functions(
    kratos_env e,
    kratos_program p
)

Get the number of functions in the given program.

function kratos_program_get_functions

kratos_function * kratos_program_get_functions(
    kratos_env e,
    kratos_program p
)

Get the list of functions in the given program.

Return: An array of references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_program_get_init

kratos_expr kratos_program_get_init(
    kratos_env e,
    kratos_program p
)

Get the init expression for the given program.

Return: A borrowed reference.

function kratos_program_get_num_globals

size_t kratos_program_get_num_globals(
    kratos_env e,
    kratos_program p
)

Get the number of global vars in the given program.

function kratos_program_get_globals

kratos_expr * kratos_program_get_globals(
    kratos_env e,
    kratos_program p
)

Get the list of global vars of the given program.

Return: An array of borrowed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_program_get_entry_point

kratos_sexp kratos_program_get_entry_point(
    kratos_env e,
    kratos_program p
)

Get the entry point of the given program.

Return: A borrowed reference.

Parsing and printing

function kratos_parse_type

kratos_type kratos_parse_type(
    kratos_env e,
    const char * s
)

Parse a type from the given string.

Return: A new reference.

function kratos_parse_expr

kratos_expr kratos_parse_expr(
    kratos_env e,
    const char * s
)

Parse an expression from the given string.

Return: A new reference.

function kratos_parse_program

kratos_program kratos_parse_program(
    kratos_env e,
    const char * s
)

Parse a program from the given string.

Return: A new reference.

function kratos_print_type

char * kratos_print_type(
    kratos_env e,
    kratos_type t
)

Get the string representation of the given type.

Return: A dynamically allocated string, which must be deallocated with kratos_free(), or NULL on error.

function kratos_print_expr

char * kratos_print_expr(
    kratos_env e,
    kratos_expr x
)

Get the string representation of the given expression.

Return: A dynamically allocated string, which must be deallocated with kratos_free(), or NULL on error.

function kratos_print_program

char * kratos_print_program(
    kratos_env e,
    kratos_program p
)

Get the string representation of the given program.

Return: A dynamically allocated string, which must be deallocated with kratos_free(), or NULL on error.

Verification

function kratos_new_config

kratos_config kratos_new_config(
    kratos_env e
)

Create a new configuration for verification.

function kratos_config_set_option

bool kratos_config_set_option(
    kratos_env e,
    kratos_config c,
    const char * opt,
    const char * val
)

Set an option for the given configuration. See here for the list of configuration options.

Return: false on error.

function kratos_config_unref

bool kratos_config_unref(
    kratos_env e,
    kratos_config c
)

Decrease the refcount of the given configuration.

Return: false on error.

function kratos_config_set_symexec_constraint_provider

bool kratos_config_set_symexec_constraint_provider(
    kratos_env e,
    kratos_config c,
    kratos_symexec_constraint_provider f,
    void * data
)

Set the custom constraint provider for symbolic execution. See kratos_symexec_constraint_provider.

Return: false on error.

function kratos_config_set_symexec_object_monitor

bool kratos_config_set_symexec_object_monitor(
    kratos_env e,
    kratos_config c,
    kratos_symexec_object_monitor f,
    void * data
)

Set the custom object monitor for symbolic execution. See kratos_symexec_object_monitor.

Return: false on error.

function kratos_verify

kratos_result kratos_verify(
    kratos_env e,
    kratos_verification_method method,
    kratos_config conf,
    kratos_program p,
    kratos_trace * out
)

Perform verification of the given program.

Parameters:

• e The environment in which to operate.
• method The verification method to use.
• conf The configuration to use.
• p The program to verify.
• out If not-NULL, pointer to a trace to store the counterexample (if any). Note that counterexample generation must be enabled in the configuration.

Return: The verification result, or KRATOS_RESULT_ERROR on error.

function kratos_encode

char * kratos_encode(
    kratos_env e,
    kratos_config conf,
    kratos_program p
)

Encode the given program into a symbolic transition system.

Parameters:

• e The environment in which to operate.
• conf The configuration to use.
• p The program to encode.

Return: A string representation of the resulting transition system, which must be deallocated with kratos_free(), or NULL on error.

function kratos_get_stats

char * kratos_get_stats(
    kratos_env e
)

Get the search statistics of the latest verification run.

Parameters:

• e The environment in which to operate.

Return: The string of statistics, which must be deallocated with kratos_free(), or NULL on error.

function kratos_trace_is_path

bool kratos_trace_is_path(
    kratos_env e,
    kratos_trace t
)

Test whether the given trace is a path.

function kratos_trace_get_path_length

size_t kratos_trace_get_path_length(
    kratos_env e,
    kratos_trace t
)

Get the length of the given path trace.

function kratos_trace_get_path

kratos_trace * kratos_trace_get_path(
    kratos_env e,
    kratos_trace t
)

Get the path of the given path trace.

Return: A list of borrowed references, which must be deallocated with kratos_free(), or NULL on error.

function kratos_trace_get_step

kratos_expr kratos_trace_get_step(
    kratos_env e,
    kratos_trace t
)

Get the step expression of the given trace.

Return: A borrowed reference.

function kratos_trace_unref

bool kratos_trace_unref(
    kratos_env e,
    kratos_trace t
)

Decrease the refcount of the given trace.

Return: false on error.