CCHLibTypes (codehawk.CCHLibTypes)

Machine sizes

Adapted from the automatically generated machdep in CIL

type machine_sizes_t = {

sizeof_short : XprTypes.xpr_t;
sizeof_int : XprTypes.xpr_t;
sizeof_bool : XprTypes.xpr_t;
sizeof_long : XprTypes.xpr_t;
sizeof_longlong : XprTypes.xpr_t;
sizeof_int128 : XprTypes.xpr_t;
sizeof_ptr : XprTypes.xpr_t;
sizeof_enum : XprTypes.xpr_t;
sizeof_float : XprTypes.xpr_t;
sizeof_double : XprTypes.xpr_t;
sizeof_longdouble : XprTypes.xpr_t;
sizeof_complex_float : XprTypes.xpr_t;
sizeof_complex_double : XprTypes.xpr_t;
sizeof_complex_longdouble : XprTypes.xpr_t;
sizeof_void : XprTypes.xpr_t;
sizeof_fun : XprTypes.xpr_t;
alignof_short : XprTypes.xpr_t;
alignof_int : XprTypes.xpr_t;
alignof_bool : XprTypes.xpr_t;
alignof_long : XprTypes.xpr_t;
alignof_longlong : XprTypes.xpr_t;
alignof_int128 : XprTypes.xpr_t;
alignof_ptr : XprTypes.xpr_t;
alignof_enum : XprTypes.xpr_t;
alignof_float : XprTypes.xpr_t;
alignof_double : XprTypes.xpr_t;
alignof_longdouble : XprTypes.xpr_t;
alignof_complex_float : XprTypes.xpr_t;
alignof_complex_double : XprTypes.xpr_t;
alignof_complex_longdouble : XprTypes.xpr_t;
alignof_str : XprTypes.xpr_t;
alignof_fun : XprTypes.xpr_t;
alignof_aligned : XprTypes.xpr_t;

}

type max_sizes_t = {

sizeof_int : int;
sizeof_float : int;
sizeof_void : int;
sizeof_ptr : int;
sizeof_fun : int;
sizeof_enum : int;

}

class type type_range_int = object ... end

class type 'a sumtype_string_converter_int = object ... end

Dictionary

type constantstring = string * bool * int

class type cdictionary_int = object ... end

Declarations

type enumitem =
  string
  * CCHBasicTypes.attributes
  * CCHBasicTypes.exp
  * CCHBasicTypes.location

class type cdeclarations_int = object ... end

Context

class type cfg_context_int = object ... end

class type exp_context_int = object ... end

class type program_context_int = object ... end

class type ccontexts_int = object ... end

Environments

class type file_environment_int = object ... end

Transformers

class type exp_transformer_int = object ... end

class type exp_walker_int = object ... end

Function summary

type api_parameter_t =

| ParFormal of int
| ParGlobal of string

type s_offset_t =

| ArgNoOffset
| ArgFieldOffset of string * s_offset_t
| ArgIndexOffset of CHNumerical.numerical_t * s_offset_t

type s_term_t =

| ArgValue of api_parameter_t * s_offset_t
| LocalVariable of string
| ExternalState of string
| ReturnValue
| NamedConstant of string
| NumConstant of CHNumerical.numerical_t
| IndexSize of s_term_t
| ByteSize of s_term_t
| ArgAddressedValue of s_term_t * s_offset_t
| ArgNullTerminatorPos of s_term_t
| ArgSizeOfType of s_term_t
| ArithmeticExpr of CCHBasicTypes.binop * s_term_t * s_term_t
| FormattedOutputSize of s_term_t
| Region of s_term_t
| RuntimeValue
| ChoiceValue of s_term_t option * s_term_t option

type xpredicate_t =

| XAllocationBase of s_term_t
(*
term points to start of allocated region that can be freed
*)
| XControlledResource of string * s_term_t
(*
term is not/must not be tainted
*)
| XBlockWrite of s_term_t * s_term_t
(*
unstructured write of bytes to pointed adress with given length (used as a side effect)
*)
| XBuffer of s_term_t * s_term_t
(*
XBuffer (t1, t2): t1 points to a memory region with at least t2 bytes after pointer
*)
| XConfined of s_term_t
(*
pointer expression is out of scope without leaking references
*)
| XConstTerm of s_term_t
(*
pointed to term is not modified
*)
| XFormattedInput of s_term_t
(*
term corresponds to argument that provides the format string
*)
| XFalse
(*
always false, used as post condition
*)
| XFreed of s_term_t
(*
term pointed to is freed
*)
| XFunctional
(*
function has no observable side effects
*)
| XInitialized of s_term_t
(*
lval denoted is initialized
*)
| XInitializedRange of s_term_t * s_term_t
(*
term pointed to is initialized for t2 length
*)
| XInitializesExternalState of s_term_t * s_term_t
(*
term t2 initializes the external state denoted by t1
*)
| XExternalStateValue of s_term_t * s_term_t
(*
term t1 has the same value as the external state denoted by t2
*)
| XInputFormatString of s_term_t
(*
term points to scanf format string
*)
| XInvalidated of s_term_t
(*
term pointed to may not be valid any more
*)
| XNewMemory of s_term_t
(*
term points to newly allocated memory (since the start of the function), stack or heap
*)
| XStackAddress of s_term_t
(*
term points to stack memory
*)
| XHeapAddress of s_term_t
(*
term points to heap memory
*)
| XGlobalAddress of s_term_t
(*
term points to global memory
*)
| XNoOverlap of s_term_t * s_term_t
(*
the two pointed-to memory regions do not overlap
*)
| XNotNull of s_term_t
(*
term is not null
*)
| XNull of s_term_t
(*
term is null
*)
| XNotZero of s_term_t
(*
term is not zero
*)
| XNonNegative of s_term_t
(*
term is not negative
*)
| XNullTerminated of s_term_t
(*
term pointed to is null-terminated
*)
| XOutputFormatString of s_term_t
(*
term points to printf format string
*)
| XPreservesAllMemory
(*
function does not free any external memory
*)
| XPreservesAllMemoryX of s_term_t list
(*
function does not free any external memory except given terms
*)
| XPreservesMemory of s_term_t
(*
function does not free pointed to memory
*)
| XPreservesValue of s_term_t
(*
function does not modify the value of s_term
*)
| XPreservesNullTermination
(*
function does not strip null-terminating bytes
*)
| XPreservesValidity of s_term_t
(*
validity of pointed to resource is maintained
*)
| XRelationalExpr of CCHBasicTypes.binop * s_term_t * s_term_t
| XRepositioned of s_term_t
(*
term pointed to may be freed and reassigned
*)
| XRevBuffer of s_term_t * s_term_t
(*
term points to memory region with at least t2 bytes before pointer
*)
| XTainted of s_term_t * s_term_t option * s_term_t option
(*
value of term is externally controlled with optional lower and upper bound
*)
| XUniquePointer of s_term_t
(*
pointer reference is the only one
*)
| XValidMem of s_term_t
(*
pointed-to memory has not been freed (at time of delivery)
*)
| XPolicyPre of s_term_t * string * string list
(*
the term has to be in one of the given states
*)
| XPolicyValue of s_term_t * string * string option
(*
the term is a newly created policy value and optionally makes a first transition
*)
| XPolicyTransition of s_term_t * string * string
(*
the term transitions according to a named transition in the policy
*)

predicate used in representation of external conditions

type postrequest_t = int * xpredicate_t

type postassume_t = int * xpredicate_t

type summary_annotation_t =

| ExternalCondition of string
| EnvironmentCondition of string
| UnmodeledArgumentDependency of string
| NoAnnotation

type annotated_xpredicate_t = xpredicate_t * summary_annotation_t

type ds_condition_t = {

dsc_name : string;
dsc_ckey : int;
dsc_fields : xpredicate_t list;

}

type function_summary_t = {

fs_fname : string;
fs_domainref : (string * string) option;
fs_params : (string * int) list;
fs_preconditions : annotated_xpredicate_t list;
fs_postconditions : annotated_xpredicate_t list;
fs_error_postconditions : annotated_xpredicate_t list;
fs_sideeffects : annotated_xpredicate_t list;

}

class type function_summary_library_int = object ... end

Interface dictionary

class type interface_dictionary_int = object ... end

Contracts

type contract_instr_t =

| SetVar of int * s_term_t * s_term_t

type contract_note_t = {

cn_tag : string;
cn_prq : string;
cn_txt : string;

}

class type function_contract_int = object ... end

class type globalvar_contract_int = object ... end

class type file_contract_int = object ... end

class type global_contract_int = object ... end

System settings

type analysis_level_t =

| UndefinedBehavior
(*
only indicate undefined behavior (Red)
*)
| ImplementationDefinedBehavior
(*
indicate undefined behavior and implementation defined behavior (Red,Purple) (default)
*)
| ValueWrapAround
(*
indicate undefined behavior, implementation-defined behavior, and value wrap around of unsigned integers (Red, Purple, Blue)
*)

class type system_settings_int = object ... end

Paths and analysis options