Module Direct_analysis.Analyze

Setup the analysis for a given abstract domain.

Parameters

module Domain : Codex.Domains.Memory_domains.With_focusing.S_with_types

Signature

val run : Frama_c_kernel.Cil_types.kernel_function -> unit

run f Do a complete analysis starting from entry point f. The function can be called multiple times, in which case the results are accumulated. Thereafter, each call to run is called " an analysis".

val dump_alarms : Stdlib.out_channel -> unit

Dump the list of all collected alarms in all the analyses to out_channel.

val dump_assertions : Stdlib.out_channel -> unit

Dump the status of every assertion in all the analyses to out_channel.

val dump_exp_table : Stdlib.out_channel -> unit

Dump a mapping from each expression of the programm to its value to out_channel.

val dump_extra : Stdlib.out_channel -> unit

Dump additional statistics collected on all analyses to out_channel.

val dump_gc : Stdlib.out_channel -> unit

Dump GC statistics collected during all analyses on out_channel.

val print_html : string -> unit

print_html filename prints the results as an HTML file.

val print_webapp : string -> unit

print_webapp filename prints the results as an interactive HTML file.