analyzer
analyzer copied to clipboard
Duplicate warnings for the same context
Looking into the warnings of context-sensitive analyses of the Concrat benchmarks revealed that for the Signed integer overflow and underflow, there are, in some cases, duplicate warnings for the same context (e.g. context with the hash 2764024368751658272 in the following segment):
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:10-1960:33)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1962:5-1962:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1965:7-1965:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:10-1960:33)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1962:5-1962:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1965:7-1965:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1960:10-1960:33)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1962:5-1962:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1965:7-1965:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 2764024368751658272 (/mnt/goblint-svcomp/goblint-bench/bench/concrat/EasyLogger/main.c:1968:7-1968:29)
The same happened when the context hashes (that might not be unique according to @sim642, and thus were not used in the abstract debugger itself) were replaced by tags (that are unique):
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 16937 (main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 16937 (main.c:1960:10-1960:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in context 16937 (main.c:1962:5-1962:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 16937 (main.c:1965:7-1965:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 16937 (main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 16937 (main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 16937 (main.c:1960:10-1960:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in context 16937 (main.c:1962:5-1962:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 16937 (main.c:1965:7-1965:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 16937 (main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 16937 (main.c:1968:7-1968:29)
[Info][Unsound] Write to unknown address: privatization is unsound. in context 16937 (main.c:1960:10-1960:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow in context 16937 (main.c:1962:5-1962:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow in context 16937 (main.c:1965:7-1965:13)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow in context 16937 (main.c:1968:7-1968:29)
We could not identify in which aspect these warnings differ from each other or why they are printed several times if they do not actually differ.