analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Duplicate warnings for the same context

Open karoliineh opened this issue 2 years ago • 0 comments

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.

karoliineh avatar Feb 06 '24 11:02 karoliineh