-
Notifications
You must be signed in to change notification settings - Fork 62
/
testsuite.mysh
705 lines (705 loc) · 28.4 KB
/
testsuite.mysh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
begin_parallel
let verifast_both
ifz3 verifast
verifast -prover redux
in
cd bin
cd rt
verifast_both -c -runtime nort rt_verified.jarsrc
cd ..
cd ..
cd examples
verifast -c -uppercase_type_params_carry_typeid generic_pred_ctors.c
verifast -c -prover z3v4.5 -uppercase_type_params_carry_typeid generic_pred_ctors.c
verifast -c mutually_recursive_fns_simple.c
verifast -shared uniqueness.c
verifast -read_options_from_source_file unions.c
verifast unions2.c
verifast -fno-strict-aliasing -assume_no_subobject_provenance unions2_no_subobj_prov.c
cd futexes
verifast -c ghost_lists.c mutex.c mutex_classic.c simple_classic_client.c simple_cross_thread_client.c
cd ..
cd busywaiting
verifast -c lexprod_wf.c busywaiting_wf.c
verifast -c bounded_fifo.c
cd clhlock
verifast -c clhlock_as_ticketlock.c clhlock.c
cd ..
cd ioliveness
verifast -c echo.c
verifast -c echo_live.c
verifast -c echo_live_mt.c
cd ..
verifast -c await.c
cd flexiblespecs
cd spinlock
verifast -c -I ../.. spinlock.c spinlock_classic.c tricky_client.c
cd ..
cd ticketlock
verifast -c -I ../.. ticketlock_strong.c ticketlock.c ticketlock_classic.c simple_cross_thread_client.c
cd ..
cd ticketlock-stronger
verifast -c -I ../.. ghost_lists.c ticketlock_strong.c ticketlock.c ticketlock_classic.c simple_classic_client.c simple_cross_thread_client.c cohortlock.c
cd ..
cd ticketlock-java
verifast -c growing_lists.jarsrc ticketlockstrong.jarsrc ticketlock.jarsrc ticketlockclassic.jarsrc classicclient.jarsrc cohortlock.jarsrc
cd ..
cd ..
cd ..
cd jayanti
verifast threading.o popl20_prophecies.o atomics.c jayanti.c client.c
cd ..
cd abstract_io
mysh < io2.mysh
cd ..
verifast -target IP16 -c -allow_should_fail 16bittest.c
verifast -read_options_from_source_file -c 64bittest.c
cd clhlock
verifast -prover redux -c clhlock.c
cd ..
cd monitors
verifast -prover z3v4.5 -disable_overflow_check -shared ghost_counters.c
verifast -prover z3v4.5 -disable_overflow_check -shared ghost_counters.c monitors.o queues.o buffer.c
verifast -prover z3v4.5 -disable_overflow_check -shared ghost_counters.c monitors.o queues.o bounded_buffer.c
verifast -prover z3v4.5 -disable_overflow_check -shared monitors.o barrier.c
verifast -prover z3v4.5 -disable_overflow_check -shared ghost_counters.c monitors.o barbershop.c
verifast -prover z3v4.5 -disable_overflow_check -shared ghost_counters.c monitors.o readers_writers.c
cd ..
cd splitcounter
verifast atomics.o ghost_lists.c splitcounter.c client.c
cd ..
cd crypto_ccs
call crypto_ccs.mysh
cd ..
cd floating_point
cd sqrt_exact
verifast -prover redux -c sqrt_exact.c
cd ..
cd sqrt_with_rounding
verifast -prover redux -c sqrt_with_rounding.c
cd ..
cd interval_arithmetic
verifast -c interval.c
cd ..
cd ..
verifast_both -c -disable_overflow_check -allow_should_fail forall.c
verifast_both -c -disable_overflow_check -allow_should_fail address_of_local.c
verifast_both -c -disable_overflow_check alt_threading.c
verifast_both -c args.c
verifast_both array_of_struct.c
verifast_both -c arraylist.c
verifast_both -disable_overflow_check threading.o barrier.c
ifz3v4.5 verifast -prover z3v4.5 -c bitops_examples.c
verifast_both -c static_array.c
verifast -c -disable_overflow_check typedef_cast.c
verifast_both -c automation.c
verifast -read_options_from_source_file priorityqueue-forall_nth.c
verifast_both set.c
cd BeepDriver
mysh < BeepKernel.mysh
cd ..
cd relaxed
mysh < relaxed.mysh
cd ..
cd shared_boxes
verifast -c sblock.c
verifast_both -c sglock.c
verifast_both -c tblock.c
verifast_both -c strong_ghost_lists.c
verifast_both -c permutations.o ghost_lists.c
verifast_both -c ticketlock_cap.c
verifast -c ticket_lock.c
verifast_both -c gotsmanlock.c
verifast_both -c spinlock.c
verifast -c -target 32bit concurrentqueue.c
verifast -c -prover z3v4.5 -target 32bit -fno-strict-aliasing -assume_no_provenance concurrentstack.c
verifast -c concurrentstackclient.c
verifast -target 32bit -allow_assume threading.o atomics.o concurrentqueue.c concurrentqueue_client.c
verifast_both -c atomic_integer.c
verifast_both -c spinlock_with_atomic_integer.c
verifast_both -c ticketlock_with_atomic_integer.c
verifast -prover redux -c interval.c
verifast_both -c lcl_set.c
verifast_both -c cell_refcounted.c
verifast -c cowl.c
verifast_both -c shared_boxes.c
verifast_both -c incrbox.c
cd ..
cd termination
mysh < termination.mysh
cd concurrent
mysh < concurrent.mysh
cd ..
cd ..
cd tso
verifast_both -c -fno-strict-aliasing -assume_no_subobject_provenance cvm0.c
verifast_both -c lock.c
verifast_both -c -disable_overflow_check prodcons.c
cd ..
verifast stringBuffers.c sockets.o bot.c
verifast_both -disable_overflow_check cat.c
verifast_both char.c
mysh < chat.mysh
verifast -c close_struct_zero.c
verifast_both -c closetest.c
verifast_both Composite.c
verifast_both composite4.c
verifast_both -c -disable_overflow_check composite5.c
verifast_both -c contains.c
verifast_both -c contains_deep.c
verifast_both -c contrib.c
verifast_both -disable_overflow_check counter.c
verifast_both -disable_overflow_check counter_with_pred.c
verifast_both -disable_overflow_check counter_with_pred_auto.c
verifast_both -target 32bit -shared threading.o counting_threads.c
cd custom_bindir
mysh < custom_bindir.mysh
cd ..
verifast_both -disable_overflow_check cp.c
verifast -c decreases.c
verifast_both -c default_clause_test.c
cd nested_induction
mysh < nested_induction.mysh
cd ..
verifast_both -shared doubly_linked_list.c
verifast_both -allow_assume -disable_overflow_check dyncode.c
verifast_both enums.c
verifast_both -c equalsmap.c
verifast_both -disable_overflow_check -fno-strict-aliasing -assume_no_subobject_provenance expr.c
cd fm2012
mysh < fm2012.mysh
cd ..
verifast_both -disable_overflow_check -c fractions-counting.c
verifast_both -disable_overflow_check -c -fno-strict-aliasing -assume_no_subobject_provenance gcl0.c
verifast_both -disable_overflow_check -c -fno-strict-aliasing -assume_no_subobject_provenance gcl.c
verifast_both ghost_field.c
verifast_both -disable_overflow_check globals.c
verifast_both -disable_overflow_check global_points_to_syntax.c
verifast_both -shared goto.c
verifast_both -disable_overflow_check -c gui-app.c
cd heartbleed
verifast_both -c t1_lib.c
cd ..
verifast_both -c icap_mt_event_loop.c
verifast_both -c ifs.c
verifast_both threading.o incr.c
cd incr_box
verifast_both -c incr_box.c
cd ..
verifast_both -shared -disable_overflow_check inverse.c
verifast_both -shared insertion_sort.c
verifast_both iter.c
verifast_both iter_with_auto.c
cd old_io
verifast_both -c iospec.c
verifast -prover redux -c iospec_theory.c
verifast_both -disable_overflow_check -c full_func_io.c
verifast_both -disable_overflow_check -c full_func_io_mod.c
verifast_both -disable_overflow_check -c full_func_io_sim.c
cd ..
cd lcset
verifast_both threading.o atomics.o ghost_lists.c ghost_counters.c locks.c lcset.c lcset_client.c
cd ..
cd lemmafuncptr
verifast_both -c lemmafuncptr.c
verifast_both -c lemmafuncptr_fraction_valid.c
verifast_both -c -allow_should_fail lemmafuncptr_fraction_invalid.c
verifast_both -c lemmafuncptr_duplication_valid.c
verifast_both -c -allow_should_fail lemmafuncptr_duplication_invalid.c
verifast_both -c -allow_should_fail lemmafuncptr_produce_invalid.c
verifast_both -c linkedlist_with_lemmaptr.c
verifast_both -c odd_even_lemmas.c
verifast_both -c split_inductive_proof.c
cd ..
verifast_both -c limits.c
verifast_both map.c
cd mcas
call mcas.mysh
cd ..
verifast_both -c mergesort_and_binarysearch.c
cd MockKernel
mysh < MockKernel.mysh
cd ..
cd module_imports
mysh -cpus 1 < module_imports.mysh
cd ..
verifast_both -c multiset_abstract_type.c
cd linking
mysh < linking.mysh
cd ..
verifast_both threading.o philosophers.c
cd preprocessor
mysh < preprocessor.mysh
cd ..
verifast_both printf.c
verifast -prover redux sprintf.c
verifast_both -target 32bit -c pthreads.c
verifast_both -c public_invariant.c
verifast_both -c pure_map.c
cd queue
verifast_both threading.o atomics.o queue.c queue_client.c
cd ..
verifast_both -target 32bit -c -disable_overflow_check quicksort.c
verifast_both -c tokenizer_test.c
verifast_both -c truncating.c
verifast_both -disable_overflow_check stringBuffers.c tokenizer.c ghostlist.o -fno-strict-aliasing -assume_no_subobject_provenance rcl.c
verifast_both reallittest.c
verifast_both -disable_overflow_check ref_points_to_syntax.c
cd reduced_annotations
mysh < reduced_annotations.mysh
cd ..
verifast_both -c short.c
verifast_both sorted_bintree.c
verifast_both spouse.c
verifast_both -c spouse-user.c
verifast_both -disable_overflow_check -shared stack.c
verifast_both -disable_overflow_check -shared stack_typeparam.c
verifast_both -c struct_assignment.c
verifast_both struct_fields.c
verifast_both swap.c
verifast_both -c switch.c
verifast_both -c -disable_overflow_check tuerk.c
verifast_both -c -disable_overflow_check tuerk_explicit.c
verifast_both -c typedefs.c
verifast_both -c umemcpy.c
verifast_both -disable_overflow_check wc.c
verifast_both -c -allow_should_fail carrays.c
verifast -c wf_func_proof.c
verifast -c wf_func1_manual.c
verifast -c wf_func2_manual.c
verifast -c -disable_overflow_check wf_func1.c
verifast -c wf_func2.c
verifast -c wf_fact_manual.c
cd helloproc
# Helloproc.mysh is not parallelizable. mysh does not guarantee that 1 will be
# the default number of cpus forever, so we explicitly specify it to be 1.
mysh -cpus 1 < helloproc.mysh
cd ..
cd usbkbd
cd src
verifast_both -target 32bit -I . -c usbmouse.c
verifast -target 32bit -I . -c -prover redux usbkbd_verified.c
cd ..
cd ..
cd verifythis2016
mysh < verify.mysh
cd ..
cd generic_functypedef
mysh < runtests.mysh
cd ..
cd io
mysh < io.mysh
cd ..
cd java
cd channels
verifast -prover redux -disable_overflow_check -c channels.jarsrc client.jarsrc
cd ..
cd channels_raw
verifast -prover redux -disable_overflow_check -c channels.jarsrc client.jarsrc
cd ..
cd chat
verifast_both -c -allow_assume chat.jarsrc
cd ..
cd chat_raw
verifast_both -c -allow_assume chat.jarsrc
cd ..
cd chatbot
verifast_both -disable_overflow_check -c -provides "main_class chatbot.Bot" Bot.java
cd ..
cd frontend
cd big_example
verifast_both -disable_overflow_check -c Java7Program_desugared.java
cd ..
cd ..
cd Iterator
verifast_both -c it.jarsrc
verifast_both -c prog.jarsrc
cd ..
cd Java Card
verifast_both -c -provides "java_card_applet MyApplet 5,1,2,3,4,5,0,1,20" JavaCard.java
verifast_both -c -provides "java_card_applet echo.Echo" Echo.java
verifast_both -c -provides "java_card_applet Store.Store" Store.java
verifast -c -prover redux -provides "java_card_applet Addressbook.Addressbook" Addressbook.java
cd shareable-applets
verifast_both -c -provides "java_card_applet wallet.EPhone" wallet.jarsrc
cd ..
verifast -c -prover redux NewEPurse/IEPurseServices.jarsrc
verifast -c -prover redux -allow_assume -provides "java_card_applet newepurse.NewEPurseApplet" NewEPurse/NewEPurseApplet.jarsrc
verifast -c -prover redux -provides "java_card_applet newjticket.NewJTicketApplet" NewJTicket/NewJTicketApplet.jarsrc
verifast -c -prover redux NewEidCard/EidCardServices.jarsrc
verifast -c -prover redux -provides "java_card_applet be.fedict.neweidapplet.NewEidCard" NewEidCard/EidCard.jarsrc
verifast -c -prover redux -provides "java_card_applet be.fedict.eidapplet.EidCard" NewEidCard/EidCard-with-auto.java
verifast -c -allow_assume -prover redux -provides "java_card_applet newmypackage.NewMyApplet 5,1,2,3,4,5,0,3,2,10,10" NewMyApplet/NewMyApplet.jarsrc
verifast -c -allow_assume -prover redux -provides "java_card_applet mypackage.MyApplet 5,1,2,3,4,5,0,3,2,10,10" MyApplet-with-auto.java
cd ..
verifast -c -disable_overflow_check GenericClass.java
verifast_both -c -disable_overflow_check Account.java
verifast_both -c -disable_overflow_check AbstractClasses.java
verifast_both -c -disable_overflow_check ArrayList.java
verifast_both -c -disable_overflow_check ArraysAuto.java
verifast_both -c -disable_overflow_check ArraysManual.java
verifast_both -c -disable_overflow_check Automation.java
verifast -c Bag.java
verifast -c -disable_overflow_check Comprehensions.java
verifast_both -c Constants.java
verifast_both -c FieldInitializers.java
verifast_both -c -allow_should_fail CompoundAssignments.java
verifast_both -c -allow_should_fail Division.java
verifast_both -c -allow_should_fail DivisionOverflow.java
verifast_both -c ConstantExpressions.java
verifast_both -disable_overflow_check -c Contrib.jarsrc
verifast_both -c DefaultCtor.java
verifast_both -c DoWhile.java
verifast_both -c Downcast.java
verifast_both -c DowncastInfo.java
verifast_both -c -allow_assume FailboxedQueueExample.java
verifast_both -c FloatingPoint.java
cd ghost_imports
mysh < ghost_imports.mysh
cd ..
verifast_both -c hello.scala
verifast_both -c HelloWorld.java
verifast_both -c -disable_overflow_check InstanceOf.java
verifast_both -c InterfaceLemmas.java
verifast_both -c Iterator.java
verifast_both -allow_assume -disable_overflow_check -c map.java
verifast_both -c -disable_overflow_check NestedExprTest.java
cd prodcons
verifast -prover redux -disable_overflow_check -c client.jarsrc
cd ..
verifast_both -c -disable_overflow_check Recell.java
verifast_both -c -disable_overflow_check AmortizedQueue.java
verifast_both -c -disable_overflow_check SuperCalls.java
verifast_both -c Spouse.java
verifast_both -c Spouse2.java
verifast_both -c SpouseFinal.java
verifast_both -c Stack.java
verifast_both -c -disable_overflow_check -provides "main_class Program" StaticFields.java
cd termination
mysh < termination.mysh
cd ..
verifast_both -c ThreadRun.java
verifast_both -c Tree.java
verifast_both -c StringLiterals.java
verifast_both -c SuperConstructorCall.java
verifast -c -allow_should_fail Exceptions.java
cd out_of_order_jarsrc
cd in_order
verifast_both -c main.jarsrc
cd ..
cd out_of_order
verifast_both -c main.jarsrc
cd ..
cd inheritance_cycle
verifast_both -c -allow_should_fail main.jarsrc
cd ..
cd ..
cd override_methods
mysh < override_methods.mysh
cd ..
cd instanceof
verifast_both -c instanceof_1.java
verifast_both -c -allow_should_fail instanceof_2.java
verifast_both -c -allow_should_fail instanceof_3.java
verifast_both -c -allow_should_fail instanceof_4.java
cd ..
cd ..
cd vstte2010
verifast -c -disable_overflow_check problem1.c
verifast -c -disable_overflow_check problem2.c
verifast_both -c -disable_overflow_check problem3.java
verifast -c -disable_overflow_check problem4.java
verifast_both -c -disable_overflow_check problem5.java
cd ..
cd vstte2012
mysh < run.mysh
cd ..
cd vacid-0
ifz3 verifast -c -disable_overflow_check Problem3.c
cd ..
verifast_both -c noreturn.c
verifast_both -c void_ignore.c
cd sizeof
verifast_both -c -allow_should_fail struct.c
verifast_both -c -fno-strict-aliasing -assume_no_subobject_provenance packed.c
cd ..
cd ..
cd tutorial_solutions
verifast_both -c -disable_overflow_check account.c
verifast_both -c -disable_overflow_check deposit.c
verifast_both -c -disable_overflow_check limit.c
verifast_both -c -disable_overflow_check pred.c
verifast_both -c -disable_overflow_check stack.c
verifast_both -c -disable_overflow_check dispose.c
verifast_both -c -disable_overflow_check sum.c
verifast_both -c -disable_overflow_check popn.c
verifast_both -c -disable_overflow_check values.c
verifast_both -c -disable_overflow_check fixpoints.c
verifast_both -c -disable_overflow_check sum_full.c
verifast_both -c -disable_overflow_check lemma.c
verifast_both -c -disable_overflow_check push_all.c
verifast_both -c -disable_overflow_check reverse.c
verifast_both -c overflow.c
verifast_both -c -disable_overflow_check filter.c
verifast_both -c -disable_overflow_check byref.c
verifast_both -c -disable_overflow_check family0.c
verifast_both -c -disable_overflow_check family.c
verifast_both -c -disable_overflow_check map.c
verifast_both -c -disable_overflow_check generics.c
verifast_both -c -disable_overflow_check foreach.c
verifast_both -c -disable_overflow_check predctors.c
verifast_both -c -disable_overflow_check threads0.c
verifast_both -c -disable_overflow_check threads.c
verifast_both -c -disable_overflow_check fractions0.c
verifast_both -c -disable_overflow_check fractions.c
verifast_both -c -disable_overflow_check precise.c
verifast_both -c -disable_overflow_check precise_bad_merge.c
verifast_both -c -disable_overflow_check mutexes.c
verifast_both -c -disable_overflow_check leaks.c
verifast_both -c -disable_overflow_check characters.c
verifast_both -c -disable_overflow_check xor.c
verifast_both -c -disable_overflow_check characters_loop.c
verifast_both -c -disable_overflow_check tuerk.c
verifast_both -c -disable_overflow_check stack_tuerk.c
verifast_both -c memcpy.c
verifast_both -c memcmp.c
verifast_both -c -disable_overflow_check strlen.c
verifast_both -target 32bit students.c
cd ..
cd tests
verifast -c continue.c
verifast -c generic_points_to.c
verifast -c struct_points_to.c
verifast -c -allow_should_fail loop_cond_assigned_vars.java
verifast -c -prover z3v4.5 generic_points_to.c
verifast -c -uppercase_type_params_carry_typeid generic_structs.c
verifast -c -uppercase_type_params_carry_typeid -prover z3v4.5 generic_structs.c
verifast -c inductive_field_access.c
verifast -c -prover z3v4.5 inductive_field_access.c
verifast -c -target lp64 issue516.c
verifast -c issue513.c
verifast -c issue511.c
verifast -c issue507.c
verifast -c issue357.c
verifast -c comma_expr.c
verifast -c call_in_struct_init.c
verifast -c -allow_should_fail effective_types.c
verifast -c mul_distrib.c
verifast -c -allow_should_fail alloc_zero.c
verifast -c malloc_integers_.c
verifast -c void_cast.c
verifast -c typedef_pointers.c
verifast -c typeid.c
verifast -c -allow_should_fail no_fwrapv.c
verifast -c -fwrapv fwrapv.c
verifast -c -allow_should_fail subobject_provenance.c
verifast -c -allow_should_fail provenance.c
verifast -c -allow_should_fail pointer_limits.c
verifast -c -allow_should_fail provenance0.c
verifast -c -allow_should_fail uninit.c
verifast -c lit_ctor_pat.c
verifast -c twoDimArray.c
verifast -c issue311.c
verifast -c -disable_overflow_check issue112.c
verifast -c issue309.c
verifast -c -allow_should_fail uninit_local.c
verifast -c floating_point.c
verifast -c varargs.c
verifast -c -target lp64 sizeof_expr.c
verifast -c -allow_should_fail evaluation_order_checks.c
verifast -c -assume_left_to_right_evaluation no_evaluation_order_checks.c
verifast -c declarators.c
verifast -c check_expr_varargs.c
verifast -c issue247.c
verifast -c variadic_macros.c
verifast -c -D ABC cmdline_defined_macros_in_header.c
verifast -c issue238.c
verifast -c deref_integer_.c
verifast -c issue68.c
verifast -c issue110.c
verifast -c -allow_should_fail issue206.c
verifast -c -allow_should_fail two_should_fails.c
verifast -c -allow_should_fail div_mod_negative_dividend.c
verifast -c -allow_should_fail div.c
verifast -c -prover z3v4.5 prod_func_ptr_chunk_ftargs_convert_provertype.c
verifast -c -allow_should_fail russell_predctors.c
verifast -c -allow_should_fail any_russell.c
verifast -c -allow_should_fail any_russell2.c
verifast -c -allow_should_fail any_russell3.c
verifast -c typedef_enum_with_body.c
verifast -c -allow_should_fail noreturn.c
verifast_both -c redux_nonlinear_mult.c
verifast_both -c simplex_secondary_closes.c
verifast_both -c simplex_secondary_closes2.c
verifast_both -c match_ctor_pat.c
verifast_both -shared -target IP16 -allow_should_fail integer__pointee_pred.c
verifast_both -c llong_fields.c
verifast_both -c -allow_should_fail -allow_undeclared_struct_types undeclared_structs.c
verifast_both stresstest-one-plus-one.c
cd test-includepath
mysh < runthistest.mysh
cd ..
cd preprocessor_if
mysh < run.mysh
cd ..
cd preprocessor_pragma
mysh < run.mysh
cd ..
verifast -c nodecl_and_semicolon.c
verifast_both -c test-octal-number.c
verifast_both -c integral-ghost-types.c
verifast_both -c -allow_should_fail longlong.c
verifast_both -c test-precise-predicate-pointsto.c
cd copredicates
mysh < run.mysh
cd ..
verifast_both -c prodlemfuncptrchunk_local_lems.c
cd lemma_ptrs_with_nonghostcallersonly
mysh < run.mysh
cd ..
cd bugs
cd z3-proves-false
ifz3 verifast -c -runtime rt/rt.jarspec z3-proves-false.java
cd ..
cd ..
cd errors
verifast -c -allow_should_fail target.c
verifast -c -allow_should_fail ctor_pattern_upcast.c
verifast -c -allow_should_fail inductive_confusion.c
verifast -c -allow_should_fail array_slice_autosplit.java
verifast -c -allow_should_fail array_update.java
verifast -c -allow_should_fail shift_errors.c
verifast -c -allow_should_fail ghost_hiding_real.c
verifast -c -allow_should_fail div_mod_by_zero.c
verifast -c -allow_should_fail div_overflow.c
verifast_both -c -allow_should_fail macro_in_macro_arg.c
verifast -c -prover z3v4.5 int_lit_overflow.c
verifast_both -c -allow_should_fail basics.c
verifast_both -c -allow_should_fail typecheck1.c
verifast_both -c -allow_should_fail ghost_assignment.c
verifast_both -c -allow_should_fail ghost_field.c
verifast_both -c -allow_should_fail inhabited.c
verifast_both -c -allow_should_fail lemmafuncptr.c
verifast_both -c -allow_should_fail redux.c redux2.c redux3.c redux4.c redux5.c redux6.c redux7.c redux8.c redux9.c redux10.c
verifast_both -c -allow_should_fail switch.c
verifast_both -c -allow_should_fail override.java
verifast_both -c -allow_assume -allow_should_fail override2.java
verifast_both -c -allow_should_fail override3.java
verifast_both -c -allow_should_fail superctor.java
verifast_both -c -allow_should_fail inhabited_tparams.c
verifast_both -c -allow_should_fail inductive_welldefined.c
verifast -c -allow_should_fail chars_split_chars_join_loop.c
verifast -c -allow_should_fail chars_split_chars_join_loop2.c
verifast_both -c -allow_should_fail predtype_contra.c
verifast_both -c -allow_should_fail fixpoint_recursive_value.c
verifast_both -c -allow_should_fail -allow_dead_code if_while_component_pure.c
verifast -c -allow_should_fail erasure.c
verifast -c -allow_should_fail erasure2.c
verifast -c -allow_should_fail erasure3.c
verifast_both -c -allow_should_fail autoclose_bad_downcast.c
verifast_both -c -allow_should_fail unsigned_int_cast.c
verifast_both -allow_should_fail sizeof_signedness.c
verifast -c -allow_should_fail java_typing_array_assignment/Test1.java
verifast -c -allow_should_fail java_typing_array_assignment/Test2.java
verifast -c -allow_should_fail java_typing_array_assignment/Test2.java
verifast_both -c -allow_should_fail fraction-of-fraction.c
verifast_both -c -allow_should_fail test-precise-predicate-pointsto-errorcase.c
verifast_both -c -allow_should_fail test-ghost-break-from-real-loop.c
verifast -c -allow_should_fail expression_not_supported_in_fixpoint.c
cd context_free_pp
verifast -c -allow_should_fail lib.c prog.c
cd ..
cd ..
cd java
cd generics
verifast -c BasicGenericClass.java
verifast -c GenericInheritance.java
verifast -c GenericType.java
verifast -c QualifiedGenericMethodCall.java
verifast -c DiamondOperator.java
verifast -c MethodInference.java
verifast -c CorrectFieldTypes.java
cd errors
verifast -c -allow_should_fail Test3.java
cd ..
cd ..
cd ..
cd cxx
cd c_copy
verifast_both -disable_overflow_check globals.cpp
verifast -c typedef_enum_with_body.cpp
verifast -c nodecl_and_semicolon.cpp
verifast -c -allow_should_fail div_mod_negative_dividend.cpp
verifast -c -disable_overflow_check tuerk.cpp
verifast_both -c truncating.cpp
cd ..
cd java_like
verifast -disable_overflow_check -prover z3v4.5 Account.cpp account_client.cpp
verifast -disable_overflow_check Stack.cpp stack_client.cpp
cd ..
cd inheritance
verifast -c -disable_overflow_check single_inheritance.cpp
verifast -c -disable_overflow_check diamond.cpp
verifast -c multiple_inheritance.cpp
verifast -c method_call_in_dtor.cpp
cd ..
cd virtual_methods
verifast -c virtual_methods.cpp
verifast -c virtual_calls_in_xtor.cpp
verifast -c -allow_should_fail virtual_call_in_ctor_ub.cpp
verifast -c -allow_should_fail virtual_call_in_dtor_ub.cpp
verifast -c -allow_should_fail indirect_virtual_call_in_ctor_ub.cpp
verifast -c -allow_should_fail indirect_virtual_call_in_dtor_ub.cpp
verifast -c -allow_should_fail -allow_dead_code -disable_overflow_check check_vtype_ptr_before_call.cpp
verifast -c -disable_overflow_check override.cpp
verifast -c -disable_overflow_check spec_override_check.cpp
verifast -c -allow_should_fail invalid_spec_override_check.cpp
cd ..
cd instance_preds
verifast -c lvalue_ref.cpp
verifast -c -disable_overflow_check multiple_inheritance.cpp
verifast -c open_close_base_pred.cpp
verifast -disable_overflow_check Account.cpp account_client.cpp
verifast -disable_overflow_check Stack.cpp stack_client.cpp
verifast -c -disable_overflow_check Shape.cpp
verifast -c -disable_overflow_check multiple_inheritance.cpp
cd auto_open_close
verifast -c -disable_overflow_check access_base_field_in_derived_struct.cpp
verifast -c -disable_overflow_check delegate_to_precise_pred.cpp
verifast -c -disable_overflow_check derived_uses_base_pred.cpp
verifast -c -disable_overflow_check target_is_not_this.cpp
cd ..
cd ..
cd delete
verifast -c polymorphic.cpp
verifast -c -allow_should_fail -allow_dead_code non_polymorphic_base.cpp
verifast -c -allow_should_fail -allow_dead_code non_virtual_base_dtor.cpp
verifast -c no_pointee_pred_no_struct.cpp
cd ..
cd elision
verifast -c -disable_overflow_check -allow_should_fail copy_ctor_side_effect.cpp
verifast -c copy_ctor_no_side_effect.cpp
verifast -c -disable_overflow_check copy_global.cpp
verifast -c -disable_overflow_check copy_param.cpp
cd ..
verifast -c main_implicit_return.cpp
verifast -c new_class.cpp
verifast -c new_primitives.cpp
verifast -prover z3v4.5 Overloads.cpp
verifast -disable_overflow_check operators.cpp
verifast -c constructors.cpp
verifast -c destructors.cpp
verifast -c -disable_overflow_check lvalue_refs.cpp
verifast -c typeid.cpp
verifast -c ghost_field.cpp
verifast -c -disable_overflow_check non_compound_stmts.cpp
verifast -c -target Linux64 literals.cpp
verifast -c loops.cpp
verifast -c casts.cpp
verifast -c switch.cpp
verifast -c declarations.cpp
cd ..
cd rust
call testsuite.mysh
cd ..
end_parallel