.. |
unit
|
[pulse] quantifier elimination using var_eqs
|
5 years ago |
Pulse.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
Pulse.mli
|
make pulse take an `InterproceduralAnalysis.t`
|
5 years ago |
PulseAbductiveDomain.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseAbductiveDomain.mli
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseAbstractValue.ml
|
[pulse] emit formula of path conditions in json output
|
5 years ago |
PulseAbstractValue.mli
|
[pulse] emit formula of path conditions in json output
|
5 years ago |
PulseArithmetic.ml
|
[pulse] make sure we checked satisfiability on summaries
|
5 years ago |
PulseArithmetic.mli
|
[pulse] make sure we checked satisfiability on summaries
|
5 years ago |
PulseAttribute.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseAttribute.mli
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseBaseAddressAttributes.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseBaseAddressAttributes.mli
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseBaseDomain.ml
|
[pulse] also visit values involved in array accesses
|
5 years ago |
PulseBaseDomain.mli
|
[pulse] Uninitialized value check in pulse
|
5 years ago |
PulseBaseMemory.ml
|
[pulse] not-completely-broken interprocedural arrays
|
5 years ago |
PulseBaseMemory.mli
|
[pulse] not-completely-broken interprocedural arrays
|
5 years ago |
PulseBaseStack.ml
|
[pulse] canonicalize wrt equality relation
|
5 years ago |
PulseBaseStack.mli
|
[pulse] canonicalize wrt equality relation
|
5 years ago |
PulseBasicInterface.ml
|
[pulse][refactor] extract and reuse a `SatUnsat` module
|
5 years ago |
PulseCItv.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseCItv.mli
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseCallEvent.ml
|
[pulse] report errors only when the PRUNE nodes along the path are true
|
5 years ago |
PulseCallEvent.mli
|
[pulse] report errors only when the PRUNE nodes along the path are true
|
5 years ago |
PulseDiagnostic.ml
|
[pulse] Revise trace of uninitialized value check
|
5 years ago |
PulseDiagnostic.mli
|
[pulse] Revise trace of uninitialized value check
|
5 years ago |
PulseDomainInterface.ml
|
[pulse] report errors only when the PRUNE nodes along the path are true
|
5 years ago |
PulseExecutionDomain.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseExecutionDomain.mli
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseFormula.ml
|
[pulse] quantifier elimination using var_eqs
|
5 years ago |
PulseFormula.mli
|
[pulse] canonicalize wrt equality relation
|
5 years ago |
PulseInterproc.ml
|
[pulse] Revise trace of uninitialized value check
|
5 years ago |
PulseInterproc.mli
|
[pulse][refactor] extract and reuse a `SatUnsat` module
|
5 years ago |
PulseInvalidation.ml
|
[pulse] Revise trace of uninitialized value check
|
5 years ago |
PulseInvalidation.mli
|
[pulse] Revise trace of uninitialized value check
|
5 years ago |
PulseLatentIssue.ml
|
[pulse] Revise trace of uninitialized value check
|
5 years ago |
PulseLatentIssue.mli
|
[pulse] Revise trace of uninitialized value check
|
5 years ago |
PulseModels.ml
|
[pulse] Model std::__optional_storage_base::has_value
|
5 years ago |
PulseModels.mli
|
make pulse take an `InterproceduralAnalysis.t`
|
5 years ago |
PulseOperations.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseOperations.mli
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulsePathCondition.ml
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulsePathCondition.mli
|
[Pulse] explicit Ok/Error summaries: bi-abduction for memory read
|
5 years ago |
PulseReport.ml
|
[pulse] make sure we checked satisfiability on summaries
|
5 years ago |
PulseReport.mli
|
[pulse][refactor] extract and reuse a `SatUnsat` module
|
5 years ago |
PulseSatUnsat.ml
|
[pulse][refactor] extract and reuse a `SatUnsat` module
|
5 years ago |
PulseSatUnsat.mli
|
[pulse][refactor] extract and reuse a `SatUnsat` module
|
5 years ago |
PulseSkippedCalls.ml
|
[pulse] define PulseSummary.yojson_of_t
|
5 years ago |
PulseSkippedCalls.mli
|
[pulse] define PulseSummary.yojson_of_t
|
5 years ago |
PulseSummary.ml
|
[pulse] define PulseSummary.yojson_of_t
|
5 years ago |
PulseSummary.mli
|
[pulse] define PulseSummary.yojson_of_t
|
5 years ago |
PulseTopl.ml
|
[topl] Refactor: Put constraint code in PulseTopl.Constraint.
|
5 years ago |
PulseTopl.mli
|
[topl] Be more precise in extracting summaries.
|
5 years ago |
PulseToplShallow.ml
|
[topl] Small step hook inside Pulse
|
5 years ago |
PulseToplShallow.mli
|
[topl] Small step hook inside Pulse
|
5 years ago |
PulseTrace.ml
|
[pulse] report errors only when the PRUNE nodes along the path are true
|
5 years ago |
PulseTrace.mli
|
[pulse] report errors only when the PRUNE nodes along the path are true
|
5 years ago |
PulseValueHistory.ml
|
[pulse] Remove duplicate `by` from a trace
|
5 years ago |
PulseValueHistory.mli
|
[pulse] define PulseSummary.yojson_of_t
|
5 years ago |
dune
|
[topl] Small step hook inside Pulse
|
5 years ago |