[Termtools] Removing of examples in full C category which are in C integer programs now

Thomas Ströder stroeder at informatik.rwth-aachen.de
Tue Jul 7 17:00:39 CEST 2015


Dear all,

I just submitted 316 example programs for the C integer programs
category. Most of them are adaptions from numeric programs in the full C
category. For those programs where the adaptions were only tiny
syntactic changes, I would propose to remove the original programs from
the full C category such that we do not have duplicates across the
categories. This would concern the following examples:

C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-complex_true-termination.c
C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination.c
C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination.c
C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-exmini_true-termination.c
C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination.c
C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination.c
C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-speedFails4_true-termination.c
C/SV-Comp/Ben-Amram-LMCS2010-Ex2.3_true-termination.c
C/SV-Comp/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination.c
C/SV-Comp/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination.c
C/SV-Comp/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination.c
C/SV-Comp/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination.c
C/SV-Comp/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination.c
C/SV-Comp/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination.c
C/SV-Comp/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex1.01_true-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.09_true-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.18_true-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.19_true-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex2.21_true-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex3.07_true-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Ex3.10_true-termination.c
C/SV-Comp/ChenFlurMukhopadhyay-SAS2012-Fig1_true-termination.c
C/SV-Comp/ColonSipma-TACAS2001-Fig1_true-termination.c
C/SV-Comp/CookSeeZuleger-TACAS2013-Fig8a_true-termination.c
C/SV-Comp/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination.c
C/SV-Comp/CookSeeZuleger-TACAS2013-Fig8b_true-termination.c
C/SV-Comp/GulavaniGulwani-CAV2008-Fig1a_true-termination.c
C/SV-Comp/GulavaniGulwani-CAV2008-Fig1b_true-termination.c
C/SV-Comp/GulavaniGulwani-CAV2008-Fig1c_true-termination.c
C/SV-Comp/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination.c
C/SV-Comp/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination.c
C/SV-Comp/LeikeHeizmann-TACAS2014-Ex1_true-termination.c
C/SV-Comp/LeikeHeizmann-TACAS2014-Ex7_true-termination.c
C/SV-Comp/LeikeHeizmann-TACAS2014-Ex8_true-termination.c
C/SV-Comp/LeikeHeizmann-TACAS2014-Fig1_true-termination.c
C/SV-Comp/LeikeHeizmann-WST2014-Ex5_false-termination.c
C/SV-Comp/LeikeHeizmann-WST2014-Ex6_false-termination.c
C/SV-Comp/Masse-VMCAI2014-Ex6_true-termination.c
C/SV-Comp/Masse-VMCAI2014-Fig1a_true-termination.c
C/SV-Comp/NoriSharma-FSE2013-Fig7_true-termination.c
C/SV-Comp/NoriSharma-FSE2013-Fig8_true-termination.c
C/SV-Comp/PodelskiRybalchenko-LICS2004-Fig1_true-termination.c
C/SV-Comp/PodelskiRybalchenko-TACAS2011-Fig1_true-termination.c
C/SV-Comp/PodelskiRybalchenko-TACAS2011-Fig2_true-termination.c
C/SV-Comp/PodelskiRybalchenko-VMCAI2004-Ex2_true-termination.c
C/SV-Comp/Urban-WST2013-Fig1_false-termination.c
C/SV-Comp/Urban-WST2013-Fig2_true-termination.c
C/SV-Comp/Urban-WST2013-Fig2-modified1000_true-termination.c
C/SV-Comp/Velroyen_false-termination.c
C/Ultimate/2Nested_true-termination.c
C/Ultimate/4NestedWith3Variables_true-termination.c
C/Ultimate/Benghazi_true-termination.c
C/Ultimate/Copenhagen_true-termination.c
C/Ultimate/MenloPark_true-termination.c
C/Ultimate/NonTermination1_false-termination.c
C/Ultimate/NonTermination4_false-termination.c
C/Ultimate/Piecewise_true-termination.c
C/Ultimate/Pure2Phase_true-termination.c
C/Ultimate/Thun_true-termination.c
C/Ultimate/Waldkirch_true-termination.c

There are still many other examples operating only on integers in the
full C category, but these also contain instructions like "++" or "while
(1)" or features like recursion such that there is a bit more of a
difference and I think that we can keep these variants of programs in
two categories.

Best regards,

  Thomas


-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150707/717083eb/attachment.sig>


More information about the Termtools mailing list