Skip to content

Commit 09723f4

Browse files
committed
Clang-format code after updates to labels
Whitespace changes only.
1 parent 5ca420b commit 09723f4

File tree

6 files changed

+28
-17
lines changed
  • regression/cbmc-concurrency

6 files changed

+28
-17
lines changed

regression/cbmc-concurrency/atomic_section_sc3/main.c

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,10 @@ unsigned dec() {
8585

8686
int main(){
8787
__CPROVER_ASYNC_1: inc();
88-
__CPROVER_ASYNC_2: dec();
89-
__CPROVER_ASYNC_3: dec();
88+
__CPROVER_ASYNC_2:
89+
dec();
90+
__CPROVER_ASYNC_3:
91+
dec();
9092

9193
return 0;
9294
}

regression/cbmc-concurrency/conditional_spawn2/main.c

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,10 @@ int main()
1616
__CPROVER_ASYNC_1: thread();
1717
}
1818

19-
__CPROVER_ASYNC_2: thread();
20-
__CPROVER_ASYNC_3: thread();
19+
__CPROVER_ASYNC_2:
20+
thread();
21+
__CPROVER_ASYNC_3:
22+
thread();
2123

2224
__CPROVER_assert(n<4, "3 threads spawned");
2325

regression/cbmc-concurrency/generic_hw_sw_benchmark1/main.c

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@
88

99
#ifdef _ENABLE_CBMC_
1010

11-
#define ASYNC(n, c) __CPROVER_ASYNC_ ## n: (c)
12-
#define ATOMIC_BEGIN __CPROVER_atomic_begin()
13-
#define ATOMIC_END __CPROVER_atomic_end()
11+
# define ASYNC(n, c) __CPROVER_ASYNC_##n : (c)
12+
# define ATOMIC_BEGIN __CPROVER_atomic_begin()
13+
# define ATOMIC_END __CPROVER_atomic_end()
1414

1515
char symbolic_char(char);
1616

@@ -233,7 +233,7 @@ void* write_data_register(struct Hardware *hw, RegisterId reg_id, Register value
233233
pthread_create(&interrupt_thread, NULL, hw->interrupt_handler, (void *) hw->fw);
234234
}
235235
#else
236-
ASYNC(1, hw->interrupt_handler((void *) hw->fw));
236+
ASYNC(1, hw->interrupt_handler((void *)hw->fw));
237237
#endif
238238

239239
SKIP:
@@ -346,7 +346,7 @@ int main(void)
346346
pthread_t firmware_thread;
347347
pthread_create(&firmware_thread, NULL, poll, (void *) fw);
348348
#else
349-
ASYNC(1, poll((void *) fw));
349+
ASYNC(1, poll((void *)fw));
350350
#endif
351351

352352
#ifdef _EXPOSE_BUG_
@@ -358,7 +358,7 @@ int main(void)
358358
pthread_t stimulus_thread;
359359
pthread_create(&stimulus_thread, NULL, stimulus, (void *) hw);
360360
#else
361-
ASYNC(2, stimulus((void *) hw));
361+
ASYNC(2, stimulus((void *)hw));
362362
#endif
363363

364364
#ifdef _EXPOSE_BUG_

regression/cbmc-concurrency/svcomp13_qrcu_safe/main.c

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,9 @@ void* qrcu_updater() {
118118

119119
int main() {
120120
__CPROVER_ASYNC_1: qrcu_reader1();
121-
__CPROVER_ASYNC_2: qrcu_reader2();
122-
__CPROVER_ASYNC_3: qrcu_updater();
121+
__CPROVER_ASYNC_2:
122+
qrcu_reader2();
123+
__CPROVER_ASYNC_3:
124+
qrcu_updater();
123125
return 0;
124126
}

regression/cbmc-concurrency/svcomp13_qrcu_unsafe/main.c

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,9 @@ void* qrcu_updater() {
118118

119119
int main() {
120120
__CPROVER_ASYNC_1: qrcu_reader1();
121-
__CPROVER_ASYNC_2: qrcu_reader2();
122-
__CPROVER_ASYNC_3: qrcu_updater();
121+
__CPROVER_ASYNC_2:
122+
qrcu_reader2();
123+
__CPROVER_ASYNC_3:
124+
qrcu_updater();
123125
return 0;
124126
}

regression/cbmc-concurrency/svcomp13_read_write_lock_safe/main.c

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,11 @@ void *reader() { //reader
3939

4040
int main() {
4141
__CPROVER_ASYNC_1: writer();
42-
__CPROVER_ASYNC_2: reader();
43-
__CPROVER_ASYNC_3: writer();
44-
__CPROVER_ASYNC_4: reader();
42+
__CPROVER_ASYNC_2:
43+
reader();
44+
__CPROVER_ASYNC_3:
45+
writer();
46+
__CPROVER_ASYNC_4:
47+
reader();
4548
return 0;
4649
}

0 commit comments

Comments
 (0)