goblint / analyzer

66%

master: 67%

LAST BUILD ON BRANCH invalidate-array-no-oob

branch: invalidate-array-no-oob

CHANGE BRANCH

x

Reset

• invalidate-array-no-oob
• 1943-affeq-analysis-crashes-on-672-sv-comp-juliet-overflow-tasks
• 2163-affine-equality-inclusion-bug
• 2197-affine-equality-bug-in-join
• HEAD
• abs-speculating
• addressdomain-of_int
• affeq-constant-sign
• affineeq-refine
• afterconfig-later
• alternative_1673
• aplas26-autotuning
• apron-empty-integer-bounds
• apron-invariant-constFold
• apron-invariant-diff-box-direct
• apron-invariant-simplify
• apron-octagon-invariant-simplify
• apron-unassume-extra-trivial
• apron-unassume-no-strengthening
• arg-complete-0.2.0
• arg-complete-array
• arg-complete-bool
• arg-stack-dedup
• arg-uncil-ambiguous
• arg-uncil-fixes
• arg-widening-termination
• arithIntBot-gone
• arithbot-tests
• array-blob-len
• arraydomain-indexdomain
• arraydomain-nullbyte-cleanup
• arraydomain-strcmp
• asm-goto
• assert-ptr
• assumption-array-bounds
• assumption-blob-init
• atomic-exchange
• auto-disable-race-analyses
• autotune-octagon-fun
• barrier-race-warning
• barriers_non_const
• base-add_offset_varinfo
• base-evalbinop-typ
• base-invariant-meet-down
• base-invariant-meet-down2
• base-protection-w
• base-reachable-refactor
• base-set-lval-type
• base-set-refactor
• base_path_sens
• biset-reduce
• bitfield-band-bor-refine
• bitfield-cast-bool
• bitfield-z-overflow
• blob-zeroinit-join
• bot_env_handling_fix
• bot_in_blob_leq_bot
• branchSet-optimize
• branch_set
• bump_goblint_cil_184
• c2po-combine
• c2po-fix-lazy
• c2po-invariant
• calloc-speculating
• camlidl-1.13
• cast-kind
• channel-with
• checks-constFold-overflow
• checks-integer-overflow
• cil-59ed1d8
• cil-dynlink
• cil-issue-183-pr-211
• cil-pretty-state
• cil-sizeOf
• codex/construct-ghost-instrumenter-for-yaml-witness
• conf-fd-leak
• congruence-hardness-unsound-branches
• copilot/add-missing-library-functions
• copilot/add-pldi25-readme-to-artifacts
• copilot/apply-transfer-function-on-sync-split
• copilot/audit-performance-bottlenecks
• copilot/detect-multiple-number-assignment
• copilot/fix-invalid-widen-issue
• copilot/fix-missing-attribute-printing
• copilot/fix-signs-ml-eval-negative-numbers
• copilot/fix-symbolic-locksets-invalidations
• copilot/fix-typos-in-ocaml-comments
• copilot/fix-typos-in-variable-names
• copilot/implement-ghost-update-instrumenter
• copilot/make-use-of-ocaml-4-14-features
• copilot/port-tutorial-analyses
• copilot/skip-ci-jobs-for-docs-changes
• copilot/warn-bitwise-shift-misuse
• copilot/warn-on-hashconsing-issues
• coverage
• cpa-extern_var-test
• cpa-hashing
• cram_coverage
• create2-check_ov
• creation-lockset-access-print
• dbg-regression
• deadcode-doc
• def_exc-doc-range
• def_exc-general-range
• def_exc-minimal-maximal
• def_exc-nonnegative-range
• deferred-hashes-for-unrolling
• delay-widening-cleanup
• delete-unsupported-analyses
• descendantLockset-output
• dev-setup
• dev-setup-opam-2.1
• dimchange-tidyup
• direct_recursive_trash
• disjointdomain-invariant
• div-by-zero-invariant
• div-by-zero-invariant-2
• div-by-zero-sem
• dune-3.20
• dune-3.22-regression
• enable-locked-creation-analyses-in-svcomp-runs
• enum-to-seq
• evalint-contradiction-deadcode
• exprelation_simplify
• fix-2297
• fix-apron-overflows
• fix-base-invariant-arithbot
• fix-forget-assigned-variables
• fix-termination-upjumping-goto
• fix/may-signed-overflow-divisor-zero-check
• fix_fork_barrier
• float-predicates
• float16
• fm26-tutorial
• fundec-missingproto-warn
• fwd_constrsys
• fwd_constrsys_digests
• fwd_constrsys_new_postsolver
• g2html-ocaml
• gStoreWidening-intervals
• generic-spec-lifters
• ghost_examples
• ghost_generalize_phase
• ghosts
• github-actions-docker-cache
• github-actions-macos-13-deprecated
• goblint-par-svcomp27-dev
• gobref
• gobview-ocaml5
• graph-easy-deterministic
• halbwachs-phd-tests
• hashcons-batteries
• indexdomain-ikind
• indexdomain-lift
• inet-fortify
• int-c-ops
• int-predicates
• int-to-float-cast-invariant
• intKindForValue-fix
• intdomain-equal_to
• intdomain-is_excl_list
• intdomain-lifter-full-output
• intdomain-no-top
• intdomain-no_ov
• intdomain-refine-refactor
• intdomain-split
• intdomain-top_typ
• intdomain-torg
• intdomain_intf
• interval32
• invariant-check-oveflows
• invariant-mli
• invariants-with-typedef-vars
• issue-1421
• issue-1449
• issue-1538
• issue-1566
• issue-1577
• issue-1591
• issue-1722
• issue-1736
• issue-1762
• issue-1767
• issue-1779
• issue-1782
• issue-1798
• issue-1801
• issue-1803
• issue-1902
• issue-1964
• issue-1967
• issue-2025
• issue-2069
• issue-2092
• issue-2093
• issue-2276
• issue-2319
• issue_1418
• issue_1438
• issue_1467
• issue_1535
• issue_1536
• issue_1558_master
• issue_1647
• issue_1651
• issue_1658
• issue_1662
• issue_1664
• issue_1673
• issue_1683
• issue_1686
• issue_1691
• issue_1697b
• issue_1719
• issue_1719_followup
• issue_1732
• issue_1774
• issue_1861
• issue_1934-str-not-an-address
• issue_2082
• issue_2091
• issue_2104
• issue_2110
• issue_2136
• issue_2227
• issue_2229
• issue_2231
• issue_2233
• issue_2235
• issue_2237
• issue_2239
• issue_2241
• issue_2243
• issue_2245
• issue_2247
• issue_2249
• issue_2251
• issue_2253
• issue_2256
• issue_2256-memalloc
• issue_2256-memcpy
• issue_2256-stdio
• issue_2261
• issue_2265
• issue_2268
• issue_2304
• issue_2307
• issue_46_94
• jobs-0
• k-branch-sens
• l4_l5_no_fast_global_init
• lattice-lift-po
• let-at
• lib-alloc-match
• list-concat_map-map
• lmust_cluster
• loc-synthetic-switch
• local-mutex
• longjmp-counting-local-dedup
• loop-unrolling-dead-branch
• lower-bounds-ci-builtin
• master
• memOutOfBounds-addr-kind-simplify
• memOutOfBounds-base-offset-relation
• memOutOfBounds-binop
• memOutOfBounds-blobsize
• memOutOfBounds-blobsize-var
• memOutOfBounds-error
• memOutOfBounds-one-past-end
• memOutOfBounds-sizedomain-count
• memleak-assert
• memsafety-bugs
• memsafety-neg-offset
• memsafety-ptr-deref
• memtrace
• min_range_sign_agnostic-64
• mine-W-noinit-threadenter
• mm_phaseGhost
• mm_rel_phaseGhost
• mod-bounds-unsoundness
• msg-assumption
• multishot-svcomp25
• multishot-tuning
• mutex-ghost
• mutex-meet-invariant
• mutex-refactor-readwrite
• nan-ne-both-branches-dead
• narrowing-gas
• no-show
• no-threadflag
• ocaml-5.5
• oob-event
• opam-locked-archived
• optimize-for_all-exists
• optimize_sparse_affeq_lindisjunc
• option_cleanup
• overflow-cast-kind
• overflow-kind
• overflow-kind-minus
• overflow-mod
• partitioned-array-make-normalize
• path_sens-error
• patricia-cached-paths
• patricia-tree
• patricia-tree-0.15.0
• patricia-tree-jsoo
• patricia-tree2
• pentagons
• phase-digest
• phase-ghost-cyclic
• phase_detection
• php_bug
• poly-set
• pools_v2
• ppx-easy-deriving-opt
• pr_1659_repair
• printable-expand2
• printable-expand3
• priv_prec_compare_stats
• protection-read-only
• ptr-minus-speculating
• qcheck-0.90
• qsolver-deadcode-escape
• query-tag
• race-coloring
• race-mcpaccess-pretty
• race-mcpaccess-rev
• race_digest_staging
• racedigest_readme
• rand-nondet-int
• reach-oob-checks
• real-sparse
• refine-pointer-by-pointee-option
• refine_loop
• region-escape
• region-unlift
• rel-ana-combine-dead
• relation-is-multiple
• remove_current_node_usages
• rm-dbg.dump
• rm-graphml-witness
• rm-post_all
• sarif-assumptions
• scc-hash
• semgrep-batenum
• semgrep-cil-var
• semgrep-let-unit-in
• signal
• simmo-phd-inc-dec
• sizedomain
• sizedomain-blob
• smart-vdq
• sparse_octagons
• spec-vg
• stats_on_texpr
• strengthening-equal-env
• struct-sets-union-uncomparable
• subpoly
• suppress_ovwarn
• sv-benchmarks-init-fixes
• svcomp-conf-explicit-malloc-fail
• svcomp-runner-continue-on-error
• svcomp26-dev
• svcomp26portfolio-nov18
• svcomp27-dev
• svcomp27-portfolios
• termination-unflat
• tests-fun-ptr-void
• threadid-history-may_create
• tm-inv-transfer
• topdown_term
• traces-vojdani
• traces-vojdani-invariant
• tutorial-testing
• uaf-event
• unassume-mutex
• unassume-postsolving
• unassume-precheck-disj
• union-read-other-member-top
• union-top-field-known-value
• unrolltype
• unrolltype-review
• update_suite-parallel
• v2.7.0-metadata
• valuedomain-do-offset
• valuedomain-do-offset-2
• valuedomain-eval-offset-f
• var
• var_eq-const
• var_eq-invariant2
• var_eq-unassume
• verbose-version
• verifier-nondet-memory
• violation_witnesses
• vmcai25-docs
• vojdani-protected-vars
• weak-branch
• weak-deps
• widen-no-leq
• widen-threshold-refactor
• widen-threshold-reset
• witness-ghost-alloc-lock-flaky-2
• witness-invariant-anon-comp-field
• witness-invariant-anon-comp-field-2
• witness-invariant-bitfield
• witness-lazy-join
• witness-validate-bottom-unconfirmed
• witness_val_fail_cherrypick
• xslt-context
• yaml-witness-2.1
• yaml-witness-2.1-transition
• yaml-witness-2.1-transition-octagon
• yaml-witness-2.1-transition-validate
• yaml-witness-2.1-version
• yaml-witness-2.2
• yaml-witness-certificates
• yaml-witness-convert
• yaml-witness-convert-2
• yaml-witness-default
• yaml-witness-ghost-unused
• yaml-witness-ghost-validate-empty
• yaml-witness-invariant-set-flow-insensitive
• yaml-witness-rm-precondition
• yaml-witness-validate-cabs2cil
• yaml-witness-validate-sha256
• yaml-witness-version-lattice
• yojson-3

Build # 5064

Build Type

Pull #2181

github

Committed by web-flow

Commit Message

Merge e6ec377dc into fabf66229

Pull Request Pull Request #2181: Do not check array bounds when invalidating or collecting reachable addresses

Coverage Stats

3 of 3 new or added lines in 2 files covered. (100.0%)

23138 of 35210 relevant lines covered (65.71%)

395732.76 hits per line