Skip to main content

mk_bv

Function mk_bv 

Source
pub unsafe extern "C" fn mk_bv(
    tm: *mut TermManager,
    size: u32,
    s: *const c_char,
    base: u32,
) -> Term
Expand description

Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.

@note The given value must fit into a bit-vector of the given size.

@param tm The term manager instance. @param size The bit-width of the constant. @param s The string representation of the constant. @param base The base of the string representation (2 for binary, 10 for decimal, and 16 for hexadecimal). @return The bit-vector constant.