Merge pull request #1153 from tautschnig/add-undef-assert

dbeyer · web-flow · commit 11a5602758fd · 2020-10-07T08:55:37.000+02:00
Resolving conflicting definitions of assert macro
diff --git a/c/aws-c-common/prelude.h b/c/aws-c-common/prelude.h
@@ -24,6 +24,7 @@ void __VERIFIER_assert(_Bool cond) {
 
 #define __CPROVER_size_t unsigned long
 
+#undef assert
 #define assert(cond) \
     __VERIFIER_assert(cond)
 
diff --git a/c/pthread-atomic/dekker.c b/c/pthread-atomic/dekker.c
@@ -11,6 +11,7 @@ void reach_error() { assert(0); }
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int flag1 = 0, flag2 = 0; // boolean flags
diff --git a/c/pthread-atomic/lamport.c b/c/pthread-atomic/lamport.c
@@ -7,6 +7,7 @@ void reach_error() { assert(0); }
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int x, y;
diff --git a/c/pthread-atomic/peterson.c b/c/pthread-atomic/peterson.c
@@ -7,6 +7,7 @@ void reach_error() { assert(0); }
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int flag1 = 0, flag2 = 0; // boolean flags
diff --git a/c/pthread-atomic/qrcu-1.c b/c/pthread-atomic/qrcu-1.c
@@ -16,6 +16,7 @@ extern int __VERIFIER_nondet_int();
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int idx=0; // boolean to control which of the two elements will be used by readers
diff --git a/c/pthread-atomic/qrcu-2.c b/c/pthread-atomic/qrcu-2.c
@@ -16,6 +16,7 @@ extern int __VERIFIER_nondet_int();
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int idx=0; // boolean to control which of the two elements will be used by readers
diff --git a/c/pthread-atomic/read_write_lock-1.c b/c/pthread-atomic/read_write_lock-1.c
@@ -15,6 +15,7 @@ void reach_error() { assert(0); }
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int w=0, r=0, x, y;
diff --git a/c/pthread-atomic/read_write_lock-2.c b/c/pthread-atomic/read_write_lock-2.c
@@ -15,6 +15,7 @@ void reach_error() { assert(0); }
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int w=0, r=0, x, y;
diff --git a/c/pthread-atomic/scull.c b/c/pthread-atomic/scull.c
@@ -83,6 +83,7 @@ extern int __VERIFIER_nondet_int();
 
 
 
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 inode i;
diff --git a/c/pthread-atomic/szymanski.c b/c/pthread-atomic/szymanski.c
@@ -7,6 +7,7 @@ void reach_error() { assert(0); }
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int flag1 = 0, flag2 = 0; // integer flags 
diff --git a/c/pthread-atomic/time_var_mutex.c b/c/pthread-atomic/time_var_mutex.c
@@ -15,6 +15,7 @@ void reach_error() { assert(0); }
 */
 
 #include <pthread.h>
+#undef assert
 #define assert(e) if (!(e)) ERROR: reach_error()
 
 int block;
diff --git a/c/pthread-complex/safestack_relacy.c b/c/pthread-complex/safestack_relacy.c
@@ -7,6 +7,7 @@ extern void abort(void);
 void reach_error() { assert(0); }
 extern void __VERIFIER_atomic_begin(void);
 extern void __VERIFIER_atomic_end(void);
+#undef assert
 #define assert(X) if(!(X)) reach_error()
 
 #include <stdio.h>
diff --git a/c/pthread-complex/workstealqueue_mutex-1.c b/c/pthread-complex/workstealqueue_mutex-1.c
@@ -9,6 +9,7 @@ extern void abort(void);
 void reach_error() { assert(0); }
 extern void __VERIFIER_atomic_begin(void);
 extern void __VERIFIER_atomic_end(void);
+#undef assert
 #define assert(X) if(!(X)) reach_error()
 
 #include <stdio.h>
diff --git a/c/pthread-complex/workstealqueue_mutex-2.c b/c/pthread-complex/workstealqueue_mutex-2.c
@@ -9,6 +9,7 @@ extern void abort(void);
 void reach_error() { assert(0); }
 extern void __VERIFIER_atomic_begin(void);
 extern void __VERIFIER_atomic_end(void);
+#undef assert
 #define assert(X) if(!(X)) reach_error()
 
 #include <stdio.h>
diff --git a/c/pthread-ext/01_inc.c b/c/pthread-ext/01_inc.c
@@ -12,6 +12,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 volatile unsigned value, m = 0;
diff --git a/c/pthread-ext/02_inc_cas.c b/c/pthread-ext/02_inc_cas.c
@@ -7,6 +7,7 @@ void reach_error() { assert(0); }
 
 #include <pthread.h>
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void __VERIFIER_atomic_CAS(
diff --git a/c/pthread-ext/03_incdec.c b/c/pthread-ext/03_incdec.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 #define atomic_assert(e) {__VERIFIER_atomic_acquire();assert(e);__VERIFIER_atomic_release();}
diff --git a/c/pthread-ext/04_incdec_cas.c b/c/pthread-ext/04_incdec_cas.c
@@ -8,6 +8,7 @@ void reach_error() { assert(0); }
 
 #include <pthread.h>
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void __VERIFIER_atomic_CAS(
diff --git a/c/pthread-ext/05_tas.c b/c/pthread-ext/05_tas.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #define locked 1
 volatile int lock = unlocked;
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void __VERIFIER_atomic_TAS(
diff --git a/c/pthread-ext/06_ticket.c b/c/pthread-ext/06_ticket.c
@@ -16,6 +16,7 @@ extern void __VERIFIER_atomic_end();
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 volatile unsigned next_ticket = 0;
diff --git a/c/pthread-ext/07_rand.c b/c/pthread-ext/07_rand.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int m = 0;
diff --git a/c/pthread-ext/08_rand_cas.c b/c/pthread-ext/08_rand_cas.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 inline int calculateNext(int s2){ 
diff --git a/c/pthread-ext/09_fmaxsym.c b/c/pthread-ext/09_fmaxsym.c
@@ -10,6 +10,7 @@ extern int __VERIFIER_nondet_int();
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 #define WORKPERTHREAD 2
diff --git a/c/pthread-ext/10_fmaxsym_cas.c b/c/pthread-ext/10_fmaxsym_cas.c
@@ -10,6 +10,7 @@ extern int __VERIFIER_nondet_int();
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 #define WORKPERTHREAD 2
diff --git a/c/pthread-ext/11_fmaxsymopt.c b/c/pthread-ext/11_fmaxsymopt.c
@@ -11,6 +11,7 @@ extern int __VERIFIER_nondet_int();
 
 #define assume(e) assume_abort_if_not(e)
 #define assert_nl(e) { if(!(e)) { goto ERROR; } }
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 #define WORKPERTHREAD 2
diff --git a/c/pthread-ext/12_fmaxsymopt_cas.c b/c/pthread-ext/12_fmaxsymopt_cas.c
@@ -11,6 +11,7 @@ extern int __VERIFIER_nondet_int();
 
 #define assume(e) assume_abort_if_not(e)
 #define assert_nl(e) { if(!(e)) { goto ERROR; } }
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void __VERIFIER_atomic_CAS(
diff --git a/c/pthread-ext/13_unverif.c b/c/pthread-ext/13_unverif.c
@@ -11,6 +11,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 unsigned int r = 0;
diff --git a/c/pthread-ext/14_spin2003.c b/c/pthread-ext/14_spin2003.c
@@ -9,6 +9,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int x=1, m=0;
diff --git a/c/pthread-ext/15_dekker.c b/c/pthread-ext/15_dekker.c
@@ -4,6 +4,7 @@ void reach_error() { assert(0); }
 
 #include <pthread.h>
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int flag1 = 0, flag2 = 0; // N boolean flags 
diff --git a/c/pthread-ext/16_peterson.c b/c/pthread-ext/16_peterson.c
@@ -4,6 +4,7 @@ void reach_error() { assert(0); }
 
 #include <pthread.h>
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int turn; // integer variable to hold the ID of the thread whose turn is it
diff --git a/c/pthread-ext/17_szymanski.c b/c/pthread-ext/17_szymanski.c
@@ -4,6 +4,7 @@ void reach_error() { assert(0); }
 
 #include <pthread.h>
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int flag1 = 0, flag2 = 0; // N integer flags 
diff --git a/c/pthread-ext/18_read_write_lock.c b/c/pthread-ext/18_read_write_lock.c
@@ -9,6 +9,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int w=0, r=0, x, y;
diff --git a/c/pthread-ext/19_time_var_mutex.c b/c/pthread-ext/19_time_var_mutex.c
@@ -9,6 +9,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/20_lamport.c b/c/pthread-ext/20_lamport.c
@@ -4,6 +4,7 @@ void reach_error() { assert(0); }
 
 #include <pthread.h>
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int x;
diff --git a/c/pthread-ext/23_lu-fig2.fixed.c b/c/pthread-ext/23_lu-fig2.fixed.c
@@ -9,6 +9,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int mThread=0;
diff --git a/c/pthread-ext/25_stack.c b/c/pthread-ext/25_stack.c
@@ -14,6 +14,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/25_stack_longer-1.c b/c/pthread-ext/25_stack_longer-1.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/25_stack_longer-2.c b/c/pthread-ext/25_stack_longer-2.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/25_stack_longest-1.c b/c/pthread-ext/25_stack_longest-1.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/25_stack_longest-2.c b/c/pthread-ext/25_stack_longest-2.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/26_stack_cas.c b/c/pthread-ext/26_stack_cas.c
@@ -14,6 +14,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/26_stack_cas_longer-1.c b/c/pthread-ext/26_stack_cas_longer-1.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/26_stack_cas_longer-2.c b/c/pthread-ext/26_stack_cas_longer-2.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/26_stack_cas_longest-1.c b/c/pthread-ext/26_stack_cas_longest-1.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/26_stack_cas_longest-2.c b/c/pthread-ext/26_stack_cas_longest-2.c
@@ -13,6 +13,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();} (void)0; } }
 
 void __VERIFIER_atomic_acquire(int * m)
diff --git a/c/pthread-ext/27_Boop_simple_vf.c b/c/pthread-ext/27_Boop_simple_vf.c
@@ -5,6 +5,7 @@ void reach_error() { assert(0); }
 
 #include <pthread.h>
 
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int usecount;
diff --git a/c/pthread-ext/28_buggy_simple_loop1_vf.c b/c/pthread-ext/28_buggy_simple_loop1_vf.c
@@ -6,6 +6,7 @@ extern unsigned int __VERIFIER_nondet_uint();
 #include <pthread.h>
 
 #define assert_nl(e) { if(!(e)) { goto ERROR; } }
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 void* thr1(void* arg){
diff --git a/c/pthread-ext/29_conditionals_vs.c b/c/pthread-ext/29_conditionals_vs.c
@@ -11,6 +11,7 @@ void reach_error() { assert(0); }
 
 #define assume(e) assume_abort_if_not(e)
 #define assert_nl(e) { if(!(e)) { goto ERROR; } }
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int m = 0;
diff --git a/c/pthread-ext/30_Function_Pointer3_vs.c b/c/pthread-ext/30_Function_Pointer3_vs.c
@@ -10,6 +10,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int mutex;
diff --git a/c/pthread-ext/31_simple_loop5_vs.c b/c/pthread-ext/31_simple_loop5_vs.c
@@ -9,6 +9,7 @@ void reach_error() { assert(0); }
 #include <pthread.h>
 
 #define assume(e) assume_abort_if_not(e)
+#undef assert
 #define assert(e) { if(!(e)) { ERROR: {reach_error();abort();}(void)0; } }
 
 int a = 1;
diff --git a/c/pthread-ext/32_pthread5_vs.c b/c/pthread-ext/32_pthread5_vs.c
diff --git a/c/pthread-ext/33_double_lock_p1_vs.c b/c/pthread-ext/33_double_lock_p1_vs.c
diff --git a/c/pthread-ext/34_double_lock_p2_vs.c b/c/pthread-ext/34_double_lock_p2_vs.c
diff --git a/c/pthread-ext/35_double_lock_p3_vs.c b/c/pthread-ext/35_double_lock_p3_vs.c
diff --git a/c/pthread-ext/36_stack_cas_p0_vs_concur.c b/c/pthread-ext/36_stack_cas_p0_vs_concur.c
diff --git a/c/pthread-ext/37_stack_lock_p0_vs_concur.c b/c/pthread-ext/37_stack_lock_p0_vs_concur.c
diff --git a/c/pthread-ext/38_rand_cas_vs_concur.c b/c/pthread-ext/38_rand_cas_vs_concur.c
diff --git a/c/pthread-ext/39_rand_lock_p0_vs.c b/c/pthread-ext/39_rand_lock_p0_vs.c
diff --git a/c/pthread-ext/40_barrier_vf.c b/c/pthread-ext/40_barrier_vf.c
diff --git a/c/pthread-ext/41_FreeBSD_abd_kbd_sliced.c b/c/pthread-ext/41_FreeBSD_abd_kbd_sliced.c
diff --git a/c/pthread-ext/42_FreeBSD_rdma_addr_sliced.c b/c/pthread-ext/42_FreeBSD_rdma_addr_sliced.c
diff --git a/c/pthread-ext/43_NetBSD_sysmon_power_sliced.c b/c/pthread-ext/43_NetBSD_sysmon_power_sliced.c
diff --git a/c/pthread-ext/44_Solaris_space_map_sliced.c b/c/pthread-ext/44_Solaris_space_map_sliced.c
diff --git a/c/pthread-ext/45_monabsex1_vs.c b/c/pthread-ext/45_monabsex1_vs.c
diff --git a/c/pthread-ext/46_monabsex2_vs.c b/c/pthread-ext/46_monabsex2_vs.c
diff --git a/c/pthread-ext/47_ticket_lock_hc_backoff_vs.c b/c/pthread-ext/47_ticket_lock_hc_backoff_vs.c
diff --git a/c/pthread-ext/48_ticket_lock_low_contention_vs.c b/c/pthread-ext/48_ticket_lock_low_contention_vs.c

Original file line number	Diff line number	Diff line change
`@@ -83,6 +83,7 @@ extern int __VERIFIER_nondet_int();`
`83`	`83`
`84`	`84`
`85`	`85`
	`86`	`+#undef assert`
`86`	`87`	`#define assert(e) if (!(e)) ERROR: reach_error()`
`87`	`88`
`88`	`89`	`inode i;`