Fix 55-loop-unrolling/12-loop-no-overflows

Author: sim642

tests/regression/55-loop-unrolling/12-loop-no-overflows.c

@@ -1,6 +1,6 @@
 // PARAM: --enable ana.int.interval_set
 // extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i
-
+// CRAM
 typedef unsigned int size_t;
 struct ldv_list_head {
     struct ldv_list_head *next, *prev;
@@ -29,7 +29,7 @@ void ldv_msg_free(struct ldv_msg *msg) {
 void main(void) {
     struct ldv_msg *msg;
     struct ldv_msg *n;
-    for (msg = ({ const typeof( ((typeof(*msg) *)0)->list ) *__mptr = ((&ldv_global_msg_list)->next); (typeof(*msg) *)( (char *)__mptr - ((size_t) &((typeof(*msg) *)0)->list) ); }), n = ({ const typeof( ((typeof(*(msg)) *)0)->list ) *__mptr = ((msg)->list.next); (typeof(*(msg)) *)( (char *)__mptr - ((size_t) &((typeof(*(msg)) *)0)->list) ); }); &msg->list != (&ldv_global_msg_list); msg = n, n = ({ const typeof( ((typeof(*(n)) *)0)->list ) *__mptr = ((n)->list.next); (typeof(*(n)) *)( (char *)__mptr - ((size_t) &((typeof(*(n)) *)0)->list) ); })) // NOWARN
+    for (msg = ({ const typeof( ((typeof(*msg) *)0)->list ) *__mptr = ((&ldv_global_msg_list)->next); (typeof(*msg) *)( (char *)__mptr - ((size_t) &((typeof(*msg) *)0)->list) ); }), n = ({ const typeof( ((typeof(*(msg)) *)0)->list ) *__mptr = ((msg)->list.next); (typeof(*(msg)) *)( (char *)__mptr - ((size_t) &((typeof(*(msg)) *)0)->list) ); }); &msg->list != (&ldv_global_msg_list); msg = n, n = ({ const typeof( ((typeof(*(n)) *)0)->list ) *__mptr = ((n)->list.next); (typeof(*(n)) *)( (char *)__mptr - ((size_t) &((typeof(*(n)) *)0)->list) ); }))
     {
         ldv_list_del(&msg->list);
         ldv_msg_free(msg);

tests/regression/55-loop-unrolling/12-loop-no-overflows.t

@@ -0,0 +1,25 @@
+Should have no overflow warning (on line 32).
+Now has NULL dereference warning there still.
+
+  $ goblint --enable ana.int.interval_set 12-loop-no-overflows.c
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:32:9-32:550)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:34:9-34:33)
+  [Info][Unsound] Unknown address given as function argument (12-loop-no-overflows.c:34:9-34:33)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:20:5-20:45)
+  [Warning][Imprecise][Program] Trying to read an index, but was not given an array ({
+                                                         next -> {&ldv_global_msg_list}
+                                                         prev -> {&ldv_global_msg_list}
+                                                       }) (12-loop-no-overflows.c:20:5-20:45)
+  [Info][Unsound] Unknown address given as function argument (12-loop-no-overflows.c:20:5-20:45)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:15:5-15:22)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:16:5-16:22)
+  [Info][Unsound] Unknown address given as function argument (12-loop-no-overflows.c:35:9-35:26)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:24:5-24:20)
+  [Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer msg->data in function free is top. Potentially invalid memory deallocation may occur (12-loop-no-overflows.c:24:5-24:20)
+  [Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer msg in function free is top. Potentially invalid memory deallocation may occur (12-loop-no-overflows.c:25:5-25:14)
+  [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (12-loop-no-overflows.c:32:444-32:470)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 16
+    dead: 0
+    total lines: 16
+