The C interface library provides a collection of basic types and operations
for direct manipulation of C values.
It is a support library for the Charon tool [FPR01].
6.1 Pervasive definitions
type LValue (t)
type VoidPtr
type CPtr(t) <: VoidPtr
type CFun(t)
type Arr(t)
type SizeOf(t)
type Signed
type Unsigned
type CChar(t)
type CShort(t)
type CInt(t)
type CLong(t)
type CLongLong(t)
type CFloat
type CDouble
type CLongDouble
type UChar = CChar(Unsigned)
type SChar = CChar(Signed)
type UShort = CShort(Unsigned)
type SShort = CShort(Signed)
type UInt = CInt(Unsigned)
type SInt = CInt(Signed)
type ULong = CLong(Unsigned)
type SLong = CLong(Signed)
type ULongLong = CLongLong(Unsigned)
type SLongLong = CLongLong(Signed)
6.2 Overloaded identifiers and operators
6.3 The CTypes module
val sizeOf : [t] SizeOf(t) -> Int
val null : [t] () -> CPtr(t)
val malloc : [t] (SizeOf(t)) -> CPtr(t)
val nmalloc : [t] (Int, SizeOf(t)) -> Arr(t)
val free : [t] CPtr(t) -> ()
val getSChar : LValue(SChar) -> Int
val setSChar : (LValue(SChar), Int) -> ()
val sizeOfSChar : () -> SizeOf(SChar)
val getUChar : LValue(UChar) -> Int
val setUChar : (LValue(UChar), Int) -> ()
val sizeOfUChar : () -> SizeOf(UChar)
val getSShort : LValue(SShort) -> Int
val setSShort : (LValue(SShort), Int) -> ()
val sizeOfSShort : () -> SizeOf(SShort)
val getUShort : LValue(UShort) -> Int
val setUShort : (LValue(UShort), Int) -> ()
val sizeOfUShort : () -> SizeOf(UShort)
val getSInt : LValue(SInt) -> Int
val setSInt : (LValue(SInt), Int) -> ()
val sizeOfSInt : () -> SizeOf(SInt)
val getUInt : LValue(UInt) -> Int
val setUInt : (LValue(UInt), Int) -> ()
val sizeOfUInt : () -> SizeOf(UInt)
val getSLong : LValue(SLong) -> Int
val setSLong : (LValue(SLong), Int) -> ()
val sizeOfSLong : () -> SizeOf(SLong)
val getULong : LValue(ULong) -> Int
val setULong : (LValue(ULong), Int) -> ()
val sizeOfULong : () -> SizeOf(ULong)
val getCFloat : LValue(CFloat) -> Float
val setCFloat : (LValue(CFloat), Float) -> ()
val sizeOfCFloat : () -> SizeOf(CFloat)
val getCDouble : LValue(CDouble) -> Double
val setCDouble : (LValue(CDouble), Double) -> ()
val sizeOfCDouble : () -> SizeOf(CDouble)
val addrOf : [t] LValue(t) -> CPtr(t)
val deref : [t] CPtr(t) -> LValue(t)
val addPtr : [t] (CPtr(t), SizeOf(t), Int) -> CPtr(t)
val getPtr : [t] (LValue(CPtr(t))) -> CPtr(t)
val setPtr : [t] (LValue(CPtr(t)), CPtr(t)) -> ()
val sizeOfPtr : [t] () -> SizeOf(CPtr(t))
val isNull : [t] CPtr(t) -> Bool
val sub : [t] (Arr(t), SizeOf(t), Int) -> LValue(t)
val toPtr : [t](Arr(t)) -> CPtr(t)
val toArr : [t](CPtr(t)) -> Arr(t)
val getArr : [t] (LValue(Arr(t))) -> Arr(t)
val setArr : [t] (LValue(Arr(t)), Arr(t)) -> ()
val getCFun : [t] (LValue(CFun(t))) -> CFun(t)
val setCFun : [t] (LValue(CFun(t)), CFun(t)) -> ()
val sizeOfCFun : [t] () -> SizeOf(CFun(t))
val isCFunNull : [t] CFun(t) -> Bool
val getCFun : [t] (LValue(CFun(t))) -> CFun(t)
val setCFun : [t] (LValue(CFun(t)), CFun(t)) -> ()
val sizeOfCFun : [t] () -> SizeOf(CFun(t))
val isCFunNull : [t] CFun(t) -> Bool
val copyString : [sign] CPtr(CChar(sign)) -> String
val copyBytes : (VoidPtr, Int) -> ByteArray
val viewAsBytes : (VoidPtr, Int) -> ByteArray