testsuite.mysh

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 unions.c
  cd busywaiting
    verifast -c bounded_fifo.c
    cd clhlock
      verifast -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 ..
  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 -prover z3v4.5 -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.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 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 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 expr.c
  cd fm2012
    mysh < fm2012.mysh
  cd ..
  verifast_both -disable_overflow_check -c fractions-counting.c
  verifast_both -disable_overflow_check -c gcl0.c
  verifast_both -disable_overflow_check -c 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 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
  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 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 ..
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 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 -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_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
    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 ..
end_parallel