package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

sha256=ca24f72fa9a87d288affe97c411753f14b7802bab4ca3649b337276b89bf5674

sha512=394b3521ccda0da91540cebb2f433f7525763060be4bbe179edd3b952a3580a8e173c4e410fc6895dc67fe6d17e6699aeddfed600f4692858bec093dd912bf1e

Events.

type t =

| Lock of LockDomain.Lockset.Lock.t
| Unlock of ValueDomain.Addr.t
| Escape of EscapeDomain.EscapedVars.t
| EnterMultiThreaded
| SplitBranch of GoblintCil.exp * bool
(*
Used to simulate old branch-based split.
*)
| AssignSpawnedThread of GoblintCil.lval * ThreadIdDomain.FlagConfiguredTID.t
(*
Assign spawned thread's ID to lval.
*)
| Access of {
1. exp : CilType.Exp.t;
2. lvals : ValueDomainQueries.LS.t;
3. kind : AccessKind.t;
4. reach : bool;
}
| Assign of {
1. lval : CilType.Lval.t;
2. exp : CilType.Exp.t;
}
(*
Used to simulate old ctx.assign.
*)
| UpdateExpSplit of GoblintCil.exp
(*
Used by expsplit analysis to evaluate exp on post-state.
*)
| Assert of GoblintCil.exp
| Unassume of {
1. exp : CilType.Exp.t;
2. uuids : string list;
}
| Longjmped of {
1. lval : CilType.Lval.t option;
}

val emit_on_deadcode : t -> bool

Should event be emitted after transfer function raises Deadcode?

val pretty : unit -> t -> GoblintCil.Pretty.doc