Reflexive pointer literal equality not understood #1374
Description
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.xmlThese 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.