package goblint-cil

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module OlfSource

Sourcetype lvalue
Sourcetype tau
Sourcetype absloc
Sourceexception UnknownLocation

Raised if a pointer flows to an undefined function. We assume that such a function can have any effect on the pointer's contents

Sourceval debug : bool ref
Sourceval debug_constraints : bool ref
Sourceval debug_aliases : bool ref
Sourceval smart_aliases : bool ref
Sourceval finished_constraints : unit -> unit
Sourceval print_constraints : bool ref
Sourceval no_flow : bool ref
Sourceval no_sub : bool ref
Sourceval analyze_mono : bool ref
Sourceval solve_constraints : unit -> unit
Sourceval rvalue : lvalue -> tau
Sourceval deref : tau -> lvalue
Sourceval join : tau -> tau -> tau
Sourceval join_inits : tau list -> tau
Sourceval address : lvalue -> tau
Sourceval instantiate : lvalue -> int -> lvalue
Sourceval assign : lvalue -> tau -> unit
Sourceval assign_ret : int -> lvalue -> tau -> unit
Sourceval apply : tau -> tau list -> tau * int
Sourceval apply_undefined : tau list -> tau * int
Sourceval assign_undefined : lvalue -> unit
Sourceval make_function : string -> lvalue list -> tau -> tau
Sourceval make_lvalue : bool -> string -> Cil.varinfo option -> lvalue
Sourceval bottom : unit -> tau
Sourceval return : tau -> tau -> unit
Sourceval make_fresh : string -> tau
Sourceval points_to_names : lvalue -> string list
Sourceval points_to : lvalue -> Cil.varinfo list
Sourceval epoints_to : tau -> Cil.varinfo list
Sourceval string_of_lvalue : lvalue -> string
Sourceval may_alias : tau -> tau -> bool
Sourceval absloc_points_to : lvalue -> absloc list
Sourceval absloc_epoints_to : tau -> absloc list
Sourceval absloc_of_lvalue : lvalue -> absloc
Sourceval absloc_eq : (absloc * absloc) -> bool
Sourceval d_absloc : unit -> absloc -> Pretty.doc
OCaml

Innovation. Community. Security.