(** This module implements a check for CWE-476 (NULL Pointer Dereference).
    It checks if the result of a function that may return a NULL value is checked
    for NULL before any memory gets accessed using the return values. The symbols
    are configurable in config.json. See https://cwe.mitre.org/data/definitions/476.html
    for detailed description.

    Parameters:
    - strict_call_policy={true, false}: Determines behaviour on call and return instructions.
      If false, we assume that the callee, resp. the caller on a return instruction,
      checks all unchecked values still contained in the registers. If true, every
      unchecked value on a call or return instruction gets reported.
    - max_steps=<num>: Max number of steps for the dataflow fixpoint algorithm.

    Notes: The check relies on Bap-generated stubs to identify return registers of the
    checked functions. Therefore it only works for functions for which Bap generates
    these stubs. *)

val name : string
val version : string

val check_cwe : Bap.Std.program Bap.Std.term -> Bap.Std.project -> Bap.Std.word Bap.Std.Tid.Map.t -> string list list -> string list -> unit