Module `Core.Frama_c_alarms`

module Location : sig ... end

module StringSet : sig ... end

module LocMap : sig ... end

type alarm_location = {

expression : Frama_c_kernel.Cil_types.exp option;
instruction : Location.t;
func : Frama_c_kernel.Kernel_function.t;

}

An alarm is located in a function, and possibly an instruction, and if possible an expression.

val alarm_location_of_loc_stack : 
  Codex_options.Location.location list ->
  alarm_location

We traverse the location stack to find the current expression (if it exists), instruction and function. Normally we should always have a function, then the instruction, and the a list of expression. On top of that we have the call stack.

val alarm_map : StringSet.t LocMap.t Stdlib.ref

module Log : Tracelog.S

val myalarm : 
  'a Operator.Alarm.t ->
  Codex_options.Location.location list ->
  unit

val count_alarms : unit -> int

val reset_alarms : unit -> unit

val dump_alarms : Stdlib.out_channel -> unit

Module Core.Frama_c_alarms

Module `Core.Frama_c_alarms`