Add NOCHECK and another annotations

tests/regression/00-sanity/37-long-double.c

@@ -1,3 +1,4 @@
+// CRAM
 int main() {
   long double l = 0.0L;
   return (int)l;

tests/regression/00-sanity/52-thread-unsafe-libfuns-single-thread.c

@@ -1,4 +1,5 @@
 // PARAM: --enable allglobs --set ana.activated[+] threadJoins
+// CRAM
 #include <stdlib.h>
 #include <pthread.h>
 

tests/regression/01-cpa/51-marshal.c

@@ -1,4 +1,5 @@
 // PARAM: --enable ana.int.interval
+// NOCHECK
 void callee(int j) {
   j++;
 }

tests/regression/02-base/57-meet-def-exc.c

@@ -1,3 +1,4 @@
+// NOCHECK
 void main(void) {
     int x;
     int i = 41;

tests/regression/03-practical/03-pthread_ptrs.c

@@ -1,5 +1,5 @@
 #include <pthread.h>
-
+// NOCHECK
 static pthread_t sid1 ;
 static pthread_t sid2 ;
 static pthread_t sid3 ;
@@ -15,22 +15,22 @@ void *fn2(void) {
 extern void *fn3(void * a);
 
 
-int main() { 
+int main() {
 	/* normal call to fn1 */
 	pthread_create(&sid1, NULL, fn1, NULL);
-	
-	/* ignore parameter (cast parameter to void) call */ 
+
+	/* ignore parameter (cast parameter to void) call */
 	pthread_create(&sid2, NULL, (void *(*)(void * )) (& fn2), NULL);
-	
+
 	/* we create a unknown thread -- that can't be good */
 	pthread_create(&sid3, NULL, &fn3, NULL);
 
 	pthread_join(sid3, NULL);
-	
+
 	pthread_join(sid2, NULL);
-	
+
 	pthread_join(sid1, NULL);
-	
+
 	return 0;
 }
 

tests/regression/03-practical/22-nested-infinite-loops.c

@@ -1,4 +1,5 @@
 // https://github.com/goblint/analyzer/issues/231#issuecomment-868369123
+// NOCHECK: should check CFG?
 int main(void) {
   int x = 0;
   while(1) {

tests/regression/03-practical/35-base-mutex-macos.c

@@ -1,5 +1,5 @@
 // Intentionally no #include <pthread.h>, because we want to imitate/debug MacOS construction on anything.
-
+// CRAM
 #define __PTHREAD_MUTEX_SIZE__		56
 
 struct _opaque_pthread_mutex_t {

tests/regression/10-synch/07-thread_self_create.c

@@ -1,5 +1,5 @@
 // PARAM: --set ana.activated[+] thread
-// Checks termination of thread analysis with a thread who is its own single parent.
+// NOTIMEOUT: Checks termination of thread analysis with a thread who is its own single parent.
 #include <pthread.h>
 
 void *t_fun(void *arg) {

tests/regression/10-synch/27-tid-array-malloc-2.c

@@ -1,4 +1,5 @@
-// PARAM: --set ana.activated[+] thread 
+// PARAM: --set ana.activated[+] thread
+// NOCRASH
 #include <stdlib.h>
 #include <pthread.h>
 
@@ -19,7 +20,7 @@ int main()
 	pthread_create(&t[tid], 0, thread, 0);
 	tid++;
 	pthread_create(&t[tid], 0, thread, 0);
-	
+
 	tid=0;
 	pthread_join(t[tid], 0);
 	tid++;

tests/regression/13-privatized/62-global-threadid.c

@@ -1,5 +1,5 @@
 #include <pthread.h>
-
+// NOCHECK
 pthread_t id;
 
 extern void magic();

tests/regression/13-privatized/65-threadreturn-cpa-remove.c

@@ -1,5 +1,5 @@
 #include <pthread.h>
-
+// NOCHECK
 int d;
 pthread_t g;
 enum { b } c() {}

tests/regression/20-slr_term/01-no-int-context.c

@@ -1,5 +1,5 @@
 // PARAM: --enable ana.int.interval --set solver slr3t --disable ana.base.context.int
-
+// NOCHECK
 int f (int i) { // -2
 	return i+1; } // -3
 void g(int j) { // -4

tests/regression/20-slr_term/02-global-inc.c

@@ -1,4 +1,4 @@
-
+// NOCHECK
 int g = 0;
 int f = 0;
 

tests/regression/20-slr_term/03-3ctxs.c

@@ -1,4 +1,4 @@
-
+// NOCHECK
 int f(int j){
 	return j+1;
 }

tests/regression/20-slr_term/05-selfloop.c

@@ -1,3 +1,4 @@
+// NOCHECK
 void f() { }
 void g() { }
 void h() { }

tests/regression/22-partitioned_arrays/08-unsupported.c

@@ -1,6 +1,7 @@
 // PARAM: --enable ana.int.interval --disable exp.fast_global_inits --set ana.base.arrays.domain partitioned
 
 // This is just to test that the analysis does not cause problems for features that are not explicitly dealt with
+// NOCHECK: what problems?
 int main(void) {
   callok();
 }

tests/regression/22-partitioned_arrays/12-was_problematic_2.c

@@ -1,4 +1,5 @@
 // PARAM: --enable ana.int.interval  --set ana.base.arrays.domain partitioned
+// NOCHECK
 int main(void)
 {
   int arr[260];

tests/regression/22-partitioned_arrays/13-was_problematic_3.c

@@ -1,4 +1,5 @@
 // PARAM: --enable ana.int.interval  --set ana.base.arrays.domain partitioned
+// NOCHECK
 struct some_struct
 {
     int dir[7];

tests/regression/22-partitioned_arrays/16-refine-meet.c

@@ -1,4 +1,5 @@
 // PARAM: --set ana.base.arrays.domain partitioned
+// NOCHECK
 int garr[7];
 
 int main(int argc, char **argv)

tests/regression/22-partitioned_arrays/19-fixpoint.c

@@ -1,4 +1,5 @@
 // PARAM: --set ana.base.arrays.domain partitioned
+// FIXPOINT
 #include <pthread.h>
 
 int stored_elements[20];

tests/regression/22-partitioned_arrays/20-more-fixpoint.c

@@ -1,4 +1,5 @@
 // PARAM: --set ana.base.arrays.domain partitioned
+// FIXPOINT
 #include <stdio.h>
 #include <stdlib.h>
 #include <pthread.h>

tests/regression/23-partitioned_arrays_last/08-unsupported.c

@@ -1,6 +1,7 @@
 // PARAM: --enable ana.int.interval --disable exp.fast_global_inits --set ana.base.arrays.domain partitioned  --set ana.base.partition-arrays.keep-expr "last"
 
 // This is just to test that the analysis does not cause problems for features that are not explicitly dealt with
+// NOCHECK: what problems?
 int main(void) {
   vla();
   callok();

tests/regression/23-partitioned_arrays_last/12-was_problematic_2.c

@@ -1,4 +1,5 @@
 // PARAM: --enable ana.int.interval  --set ana.base.arrays.domain partitioned --set ana.base.partition-arrays.keep-expr "last"
+// NOCHECK
 int main(void)
 {
   int arr[260];

tests/regression/24-octagon/03-previously_problematic_a.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 int main(int argc, char const *argv[])
 {

tests/regression/24-octagon/04-previously_problematic_b.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 typedef int wchar_t;
 typedef unsigned long size_t;

tests/regression/24-octagon/05-previously_problematic_c.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval  --set ana.base.arrays.domain partitioned --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 int main(int argc, char const *argv[])
 {

tests/regression/24-octagon/06-previously_problematic_d.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 int main(int argc, char const *argv[])
 {

tests/regression/24-octagon/07-previously_problematic_e.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 int main(int argc, char const *argv[])
 {

tests/regression/24-octagon/08-previously_problematic_f.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 int main(int argc, char const *argv[])
 {

tests/regression/24-octagon/09-previously_problematic_g.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 int main(int argc, char const *argv[])
 {

tests/regression/24-octagon/10-previously_problematic_h.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 int main(int argc, char const *argv[])
 {

tests/regression/24-octagon/11-previously_problematic_i.c

@@ -1,5 +1,5 @@
 // SKIP PARAM: --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.activated[+] apron
-// These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
+// FIXPOINT: These examples were cases were we saw issues of not reaching a fixpoint during development of the octagon domain. Since those issues might
 // resurface, these tests without asserts are included
 char buf2[67];
 

tests/regression/24-octagon/12-previously_problematic_j.c

@@ -1,4 +1,5 @@
 // SKIP PARAM: --set ana.activated[+] apron
+// NOCHECK
 void main(void) {
   int i = 0;
   int j = i;

tests/regression/25-vla/03-calls.c

@@ -1,5 +1,6 @@
 // PARAM: --enable ana.int.interval --disable ana.int.def_exc --set ana.base.arrays.domain partitioned
 // Variable-sized arrays
+// NOCHECK
 void foo(int n, int a[n]);
 void foo2(int n, int a[30][n]);
 void foo3(int n, int a[n][30]);

tests/regression/27-inv_invariants/02-bot-during-condition.c

@@ -1,3 +1,4 @@
+// NOCHECK
 int main ()
 {
   int tmp;

tests/regression/27-inv_invariants/07-more-bot.c

@@ -1,5 +1,6 @@
 // PARAM: --enable ana.int.interval
 // Adapted from sv-comp array-programs/partial_mod_count_1.c
+// NOCHECK
 int N = 1000;
 int main(){
   int i;

tests/regression/28-race_reach/95-deref-fun.c

@@ -1,6 +1,6 @@
 // PARAM: --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"
 #include<pthread.h>
-
+// NOCRASH
 void foo(int (*callback)()) {
 }
 

tests/regression/28-race_reach/96-deref-fun2.c

@@ -1,6 +1,6 @@
 // PARAM: --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"
 #include<pthread.h>
-
+// NOCRASH
 #define SVCOMP 1
 
 #include <pthread.h>

tests/regression/29-svcomp/25-writing-into-char-array.c

@@ -1,3 +1,4 @@
+// NOCHECK
 #include<stdio.h>
 struct __anonstruct_mbox_t_232 {
    int one;

tests/regression/29-svcomp/26-ikinds_if.c

@@ -1,4 +1,5 @@
 //PARAM: --enable ana.int.interval
+// NOCHECK
 #include<stdlib.h>
 
 static long sound_ioctl(unsigned int cmd , unsigned long arg )

tests/regression/29-svcomp/29-witness.c

@@ -1,4 +1,5 @@
 // PARAM: --enable ana.sv-comp.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"
+// NOCRASH
 #include <pthread.h>
 #include <goblint.h>
 

tests/regression/29-svcomp/32-no-ov.c

@@ -1,5 +1,5 @@
 // PARAM: --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )"
-
+// CRAM
 int main(){
 	// This is not an overflow, just implementation defined behavior on a cast
 	int data = ((int)(rand() & 1 ? (((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) : -(((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) - 1));

tests/regression/33-constants/01-const.c

@@ -1,5 +1,6 @@
 //PARAM: --set ana.activated '["constants"]'
 // intentional explicit ana.activated to do tutorial in isolation
+// NOCHECK
 int f(int a, int b){
     int d = 3;
     int z = a + d;

tests/regression/33-constants/02-simple.c

@@ -1,6 +1,6 @@
 //PARAM: --set ana.activated '["constants"]'
 // intentional explicit ana.activated to do tutorial in isolation
-
+// NOCHECK
 int main(){
     int x = 3;
     int y = 4;

tests/regression/33-constants/03-empty-not-dead-branch.c

@@ -1,6 +1,6 @@
 //PARAM: --set ana.activated '["constants"]'
 // intentional explicit ana.activated to do tutorial in isolation
-
+// NOCHECK
 int g;
 
 int main() {

tests/regression/33-constants/04-empty-not-dead.c

@@ -1,6 +1,6 @@
 //PARAM: --set ana.activated '["constants"]'
 // intentional explicit ana.activated to do tutorial in isolation
-
+// NOCHECK
 int g;
 
 int main() {

tests/regression/33-constants/05-fun_ptranal.c

@@ -1,5 +1,6 @@
 //PARAM: --set ana.activated '["constants", "ptranal"]'
 // intentional explicit ana.activated to do tutorial in isolation
+// NOCHECK
 int f(int a, int b){
     int d = 3;
     int z = a + d;

tests/regression/34-localwn_restart/05-nested.w.counter.c

@@ -1,4 +1,5 @@
 // Variant of nested.c with a counter.
+// NOCHECK
 void main()
 {
   int z = 0;

tests/regression/36-apron/65-multi-lock-producer-consumer.c

@@ -1,5 +1,6 @@
 // SKIP PARAM: --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.relation.privatization mutex-meet --set ana.apron.domain polyhedra
 // TODO: why doesn't mutex-meet-tid succeed? a widening loses some upper bound and we forget a possible overflow, succeeds with assume_none
+// NOCHECK
 #include <pthread.h>
 #include <goblint.h>
 

tests/regression/38-int-refinements/05-invalid-widen.c

@@ -1,4 +1,5 @@
 //PARAM: --set ana.int.refinement once --enable ana.int.enums
+// NOCRASH
 #include <goblint.h>
 
 int main() {

tests/regression/41-stdlib/03-noqsort.c

@@ -1,4 +1,5 @@
 // PARAM: --set pre.cppflags[+] -DGOBLINT_NO_QSORT
+// CRAM
 #include<stddef.h>
 
 // There should be no CIL warning about multiple definitions here

tests/regression/41-stdlib/03-noqsort.t

@@ -1,7 +1,7 @@
 There should be no CIL warning about multiple definitions:
 
   $ goblint --set pre.cppflags[+] -DGOBLINT_NO_QSORT 03-noqsort.c
-  [Warning][Deadcode] Function 'qsort' is uncalled: 1 LLoC (03-noqsort.c:5:1-6:1)
+  [Warning][Deadcode] Function 'qsort' is uncalled: 1 LLoC (03-noqsort.c:6:1-7:1)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 1 (1 in uncalled functions)

tests/regression/43-struct-domain/12-aget.c

@@ -1,5 +1,5 @@
 // PARAM: --set ana.base.structs.domain "sets"
-
+// NOCHECK
 // This is shortened from aget.c in the bench repository
 // There was an issue when testing arrays, as they init to bottom and this code triggers narrowing.
 /* Generated by CIL v. 1.3.6 */

tests/regression/43-struct-domain/25-aget-keyed.c

@@ -1,5 +1,5 @@
 // PARAM: --set ana.base.structs.domain "keyed"
-
+// NOCHECK
 // This is shortened from aget.c in the bench repository
 // There was an issue when testing arrays, as they init to bottom and this code triggers narrowing.
 /* Generated by CIL v. 1.3.6 */