Module Symex.StatKeys

Keys for statistics used in Soteria's symex engine. These are exposed so clients can query statistics if needed; the type with which they are logged is also documented.

It is recommended for clients to not use these keys for custom statistics tracking. To avoid clashes, all of these are prefixed with soteria.

val exec_time : string

Total execution time. Logged as a Stats.stat_entry.Float.

val sat_time : string

SAT solving time. Logged as a Stats.stat_entry.Float.

val sat_checks : string

Number of calls to the solver's sat function. Logged as a Stats.stat_entry.Int.

val sat_unknowns : string

Number of calls to the solver's sat function that returned Unknown. Logged as a Stats.stat_entry.Int.

val unexplored_branches : string

Number of unexplored branches due to fuel exhaustion. Logged as a Stats.stat_entry.Int.

val branches : string

Number of branches explored. Logged as a Stats.stat_entry.Int.

val steps : string

Total number of steps taken across all branches. Logged as a Stats.stat_entry.Int.

val give_up_reasons : string

Number of give-ups due to incompleteness. Logged as a Stats.stat_entry.StrSeq.

val miss_without_fix : string

Number of misses without any fix. Logged as a Stats.stat_entry.StrSeq.

val branch_on_calls : string

Number of times branch_on was called

val branch_on_branched : string

Number of times branch_on actually branched