kdrag.printers.c

Functions

c_of_expr(ctx, sig, e)

compile_and_link(name, args, body)

compile_and_link_defn(f)

compile_c(c_code[, opts])

#>>> x,y = smt.BitVecs("x y", 32) #>>> compile_c(cstring("foo", [x,y], smt.If(smt.UGT(x + x*y + 1, x), x , y)))

cstring(name, args, body)

ctype_of_sort(s)

is_valid_c_identifier(identifier)

is_valid_c_identifier_strict(identifier)

link(name, args, body, filename)

of_defn(f)

kdrag.printers.c.c_of_expr(ctx: list[ExprRef], sig: list[FuncDeclRef], e: ExprRef) → str
Parameters:

  • ctx (list[ExprRef])

  • sig (list[FuncDeclRef])

  • e (ExprRef)

Return type:

str

Parameters:

f (FuncDeclRef)

kdrag.printers.c.compile_c(c_code, opts=[])

#>>> x,y = smt.BitVecs(“x y”, 32) #>>> compile_c(cstring(“foo”, [x,y], smt.If(smt.UGT(x + x*y + 1, x), x , y)))

kdrag.printers.c.cstring(name, args, body)
kdrag.printers.c.ctype_of_sort(s: SortRef)
Parameters:

s (SortRef)

kdrag.printers.c.is_valid_c_identifier(identifier: str) → bool
Parameters:

identifier (str)

Return type:

bool

kdrag.printers.c.is_valid_c_identifier_strict(identifier: str) → bool
Parameters:

identifier (str)

Return type:

bool

kdrag.printers.c.of_defn(f: FuncDeclRef)
Parameters:

f (FuncDeclRef)