Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Reflexive pointer literal equality not understood #1374

Closed
sim642 opened this issue Feb 28, 2024 · 0 comments · Fixed by #1396
Closed

Reflexive pointer literal equality not understood #1374

sim642 opened this issue Feb 28, 2024 · 0 comments · Fixed by #1396

Comments

@sim642
Copy link
Member

sim642 commented Feb 28, 2024

Running our simplest regression test now produces some odd

expression "& mutex1 == & mutex1" not understood

output:

$ ./regtest.sh 04 01
./goblint --enable warn.debug --enable dbg.regression --html   tests/regression/04-mutex/01-simple_rc.c
[Debug][Analyzer] Invariant failed: expression "& mutex1 == & mutex1" not understood. (tests/regression/04-mutex/01-simple_rc.c:9:3-9:30)
[Debug][Analyzer] Invariant failed: expression "& mutex2 == & mutex2" not understood. (tests/regression/04-mutex/01-simple_rc.c:18:3-18:30)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 12
  dead: 0
  total lines: 12
[Warning][Race] Memory location myglobal (race with conf. 110): (tests/regression/04-mutex/01-simple_rc.c:4:5-4:13)
  write with [lock:{mutex1}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (tests/regression/04-mutex/01-simple_rc.c:10:3-10:22)
  write with [mhp:{created={[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (tests/regression/04-mutex/01-simple_rc.c:19:3-19:22)
  read with [lock:{mutex1}, thread:[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (tests/regression/04-mutex/01-simple_rc.c:10:3-10:22)
  read with [mhp:{created={[main, t_fun@tests/regression/04-mutex/01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (tests/regression/04-mutex/01-simple_rc.c:19:3-19:22)
[Info][Race] Memory locations race summary:
  safe: 0
  vulnerable: 0
  unsafe: 1
  total memory locations: 1
[Info] Writing xml to temp. file: /tmp/ocaml4ffc79tmp
Time needed: 296 ms
See result/index.xml

These are probably the result of #1343 which emits such refinements. The fact that they are emitted is not the problem, rather that base analysis claims to not understand trivial refinements which cannot refine anything anyway.

@sim642 sim642 self-assigned this Mar 21, 2024
sim642 added a commit that referenced this issue Mar 21, 2024
@sim642 sim642 added this to the v2.4.0 milestone Mar 21, 2024
sim642 added a commit to sim642/opam-repository that referenced this issue Aug 2, 2024
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
avsm pushed a commit to avsm/opam-repository that referenced this issue Sep 5, 2024
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant