From a6cc486874656fa8a135e1e035c3ad1b77f27fbe Mon Sep 17 00:00:00 2001 From: Adharsh Kamath Date: Sat, 11 Nov 2023 13:06:59 +0530 Subject: [PATCH] refactored checking --- data/analysis/svcomp_dataset.ipynb | 55 ++++-- data/analysis/ultimate_success_benchmarks.txt | 170 ++++++++++++++++++ data/benchmarks/diffy_cav21_bench/brs1.c | 43 +++++ data/benchmarks/diffy_cav21_bench/brs2.c | 43 +++++ data/benchmarks/diffy_cav21_bench/brs3.c | 43 +++++ data/benchmarks/diffy_cav21_bench/brs4.c | 43 +++++ data/benchmarks/diffy_cav21_bench/brs5.c | 43 +++++ data/benchmarks/diffy_cav21_bench/cond1.c | 51 ++++++ data/benchmarks/diffy_cav21_bench/cond2.c | 46 +++++ data/benchmarks/diffy_cav21_bench/cond2s1.c | 46 +++++ data/benchmarks/diffy_cav21_bench/cond2s2.c | 46 +++++ data/benchmarks/diffy_cav21_bench/conda.c | 46 +++++ data/benchmarks/diffy_cav21_bench/condg.c | 49 +++++ data/benchmarks/diffy_cav21_bench/condi.c | 43 +++++ data/benchmarks/diffy_cav21_bench/condm.c | 42 +++++ data/benchmarks/diffy_cav21_bench/condn.c | 42 +++++ data/benchmarks/diffy_cav21_bench/condnl1.c | 45 +++++ data/benchmarks/diffy_cav21_bench/conds.c | 51 ++++++ data/benchmarks/diffy_cav21_bench/conds2.c | 45 +++++ data/benchmarks/diffy_cav21_bench/condsc.c | 51 ++++++ data/benchmarks/diffy_cav21_bench/condss.c | 56 ++++++ data/benchmarks/diffy_cav21_bench/condss1.c | 56 ++++++ data/benchmarks/diffy_cav21_bench/condss2.c | 56 ++++++ data/benchmarks/diffy_cav21_bench/condss3.c | 56 ++++++ data/benchmarks/diffy_cav21_bench/eqn1.c | 41 +++++ data/benchmarks/diffy_cav21_bench/eqn2.c | 42 +++++ data/benchmarks/diffy_cav21_bench/eqn3.c | 42 +++++ data/benchmarks/diffy_cav21_bench/eqn4.c | 41 +++++ data/benchmarks/diffy_cav21_bench/eqn5.c | 41 +++++ data/benchmarks/diffy_cav21_bench/ifcomp.c | 57 ++++++ data/benchmarks/diffy_cav21_bench/ifeqn1.c | 47 +++++ data/benchmarks/diffy_cav21_bench/ifeqn2.c | 47 +++++ data/benchmarks/diffy_cav21_bench/ifeqn3.c | 47 +++++ data/benchmarks/diffy_cav21_bench/ifeqn4.c | 47 +++++ data/benchmarks/diffy_cav21_bench/ifeqn5.c | 47 +++++ data/benchmarks/diffy_cav21_bench/ifncomp.c | 57 ++++++ data/benchmarks/diffy_cav21_bench/indp1.c | 44 +++++ data/benchmarks/diffy_cav21_bench/indp2.c | 44 +++++ data/benchmarks/diffy_cav21_bench/indp3.c | 49 +++++ data/benchmarks/diffy_cav21_bench/indp4.c | 44 +++++ data/benchmarks/diffy_cav21_bench/indp5.c | 52 ++++++ data/benchmarks/diffy_cav21_bench/modn.c | 40 +++++ data/benchmarks/diffy_cav21_bench/modp.c | 40 +++++ data/benchmarks/diffy_cav21_bench/mods.c | 50 ++++++ data/benchmarks/diffy_cav21_bench/ms1.c | 39 ++++ data/benchmarks/diffy_cav21_bench/ms2.c | 39 ++++ data/benchmarks/diffy_cav21_bench/ms3.c | 39 ++++ data/benchmarks/diffy_cav21_bench/ms4.c | 39 ++++ data/benchmarks/diffy_cav21_bench/ms5.c | 39 ++++ data/benchmarks/diffy_cav21_bench/ncomp.c | 48 +++++ .../benchmarks/diffy_cav21_bench/nested-as1.c | 56 ++++++ .../benchmarks/diffy_cav21_bench/nested-as2.c | 56 ++++++ .../benchmarks/diffy_cav21_bench/nested-as3.c | 56 ++++++ .../diffy_cav21_bench/nested-nli1.c | 43 +++++ .../diffy_cav21_bench/nested-nli2.c | 43 +++++ .../diffy_cav21_bench/nested-nli3.c | 44 +++++ .../diffy_cav21_bench/nested-nlj1.c | 41 +++++ .../diffy_cav21_bench/nested-nlj2.c | 43 +++++ .../diffy_cav21_bench/nested-nlj3.c | 44 +++++ .../diffy_cav21_bench/nested-nsna1.c | 52 ++++++ .../diffy_cav21_bench/nested-nsna2.c | 52 ++++++ .../diffy_cav21_bench/nested-nsna3.c | 52 ++++++ .../benchmarks/diffy_cav21_bench/nested-sa1.c | 50 ++++++ .../diffy_cav21_bench/nested-sna1.c | 51 ++++++ .../diffy_cav21_bench/nested-sna2.c | 51 ++++++ .../diffy_cav21_bench/nested-sna3.c | 51 ++++++ .../benchmarks/diffy_cav21_bench/nested-ss1.c | 61 +++++++ .../benchmarks/diffy_cav21_bench/nested-ss2.c | 61 +++++++ .../benchmarks/diffy_cav21_bench/nested-ss3.c | 61 +++++++ .../benchmarks/diffy_cav21_bench/nested-sum.c | 35 ++++ .../diffy_cav21_bench/nested-unb1.c | 43 +++++ .../diffy_cav21_bench/nested-unb2.c | 43 +++++ .../diffy_cav21_bench/nested-unb3.c | 43 +++++ data/benchmarks/diffy_cav21_bench/nsqm-if.c | 47 +++++ data/benchmarks/diffy_cav21_bench/nsqm.c | 42 +++++ data/benchmarks/diffy_cav21_bench/pcomp.c | 49 +++++ data/benchmarks/diffy_cav21_bench/res1.c | 48 +++++ data/benchmarks/diffy_cav21_bench/res1o.c | 48 +++++ data/benchmarks/diffy_cav21_bench/res2.c | 59 ++++++ data/benchmarks/diffy_cav21_bench/res2o.c | 59 ++++++ data/benchmarks/diffy_cav21_bench/s12if.c | 50 ++++++ data/benchmarks/diffy_cav21_bench/s1if.c | 41 +++++ data/benchmarks/diffy_cav21_bench/s1lif.c | 46 +++++ data/benchmarks/diffy_cav21_bench/s22if.c | 50 ++++++ data/benchmarks/diffy_cav21_bench/s2if.c | 41 +++++ data/benchmarks/diffy_cav21_bench/s2lif.c | 46 +++++ data/benchmarks/diffy_cav21_bench/s32if.c | 50 ++++++ data/benchmarks/diffy_cav21_bench/s3if.c | 41 +++++ data/benchmarks/diffy_cav21_bench/s3lif.c | 46 +++++ data/benchmarks/diffy_cav21_bench/s42if.c | 51 ++++++ data/benchmarks/diffy_cav21_bench/s4if.c | 41 +++++ data/benchmarks/diffy_cav21_bench/s4lif.c | 46 +++++ data/benchmarks/diffy_cav21_bench/s52if.c | 51 ++++++ data/benchmarks/diffy_cav21_bench/s5if.c | 41 +++++ data/benchmarks/diffy_cav21_bench/s5lif.c | 46 +++++ .../diffy_cav21_bench/sanfoundry_27_ground.c | 39 ++++ data/benchmarks/diffy_cav21_bench/sina1.c | 40 +++++ data/benchmarks/diffy_cav21_bench/sina2.c | 45 +++++ data/benchmarks/diffy_cav21_bench/sina3.c | 51 ++++++ data/benchmarks/diffy_cav21_bench/sina4.c | 51 ++++++ data/benchmarks/diffy_cav21_bench/sina5.c | 56 ++++++ data/benchmarks/diffy_cav21_bench/sqm-if.c | 47 +++++ data/benchmarks/diffy_cav21_bench/sqm.c | 42 +++++ data/benchmarks/diffy_cav21_bench/ss1.c | 46 +++++ data/benchmarks/diffy_cav21_bench/ss2.c | 60 +++++++ data/benchmarks/diffy_cav21_bench/ss3.c | 52 ++++++ data/benchmarks/diffy_cav21_bench/ss4.c | 48 +++++ data/benchmarks/diffy_cav21_bench/ssina.c | 56 ++++++ .../standard_compareModified_ground.c | 34 ++++ .../standard_compare_ground.c | 32 ++++ .../standard_copy1_ground-1.c | 28 +++ .../standard_copy2_ground-2.c | 32 ++++ .../standard_copy3_ground-1.c | 36 ++++ .../standard_copy4_ground-1.c | 40 +++++ .../standard_copy5_ground-1.c | 43 +++++ .../standard_copy6_ground-2.c | 48 +++++ .../standard_copy7_ground-2.c | 51 ++++++ .../standard_copy8_ground-1.c | 55 ++++++ .../standard_copy9_ground-2.c | 60 +++++++ .../standard_copyInitSum2_ground-2.c | 30 ++++ .../standard_copyInitSum3_ground.c | 34 ++++ .../standard_copyInitSum_ground.c | 33 ++++ .../standard_copyInit_ground.c | 27 +++ .../standard_init1_ground-2.c | 20 +++ .../standard_init2_ground-2.c | 25 +++ .../standard_init3_ground-2.c | 30 ++++ .../standard_init4_ground-2.c | 35 ++++ .../standard_init5_ground-1.c | 40 +++++ .../standard_init6_ground-2.c | 45 +++++ .../standard_init7_ground-2.c | 50 ++++++ .../standard_init8_ground-2.c | 55 ++++++ .../standard_init9_ground-2.c | 60 +++++++ .../standard_maxInArray_ground.c | 30 ++++ .../standard_minInArray_ground-2.c | 32 ++++ .../standard_password_ground.c | 34 ++++ .../diffy_cav21_bench/standard_running-2.c | 35 ++++ .../standard_seq_init_ground.c | 23 +++ .../standard_strcmp_ground.c | 31 ++++ .../standard_vector_difference_ground.c | 39 ++++ data/benchmarks/diffy_cav21_bench/zero_sum1.c | 36 ++++ data/benchmarks/diffy_cav21_bench/zero_sum2.c | 46 +++++ data/benchmarks/diffy_cav21_bench/zero_sum3.c | 56 ++++++ data/benchmarks/diffy_cav21_bench/zero_sum4.c | 66 +++++++ data/benchmarks/diffy_cav21_bench/zero_sum5.c | 76 ++++++++ .../diffy_cav21_bench/zero_sum_const1.c | 36 ++++ .../diffy_cav21_bench/zero_sum_const2.c | 46 +++++ .../diffy_cav21_bench/zero_sum_const3.c | 56 ++++++ .../diffy_cav21_bench/zero_sum_const4.c | 66 +++++++ .../diffy_cav21_bench/zero_sum_const5.c | 76 ++++++++ .../diffy_cav21_bench/zero_sum_const_m2.c | 46 +++++ .../diffy_cav21_bench/zero_sum_const_m3.c | 56 ++++++ .../diffy_cav21_bench/zero_sum_const_m4.c | 66 +++++++ .../diffy_cav21_bench/zero_sum_const_m5.c | 76 ++++++++ .../diffy_cav21_bench/zero_sum_const_m6.c | 86 +++++++++ .../diffy_cav21_bench/zero_sum_m2.c | 46 +++++ .../diffy_cav21_bench/zero_sum_m3.c | 56 ++++++ .../diffy_cav21_bench/zero_sum_m4.c | 66 +++++++ .../diffy_cav21_bench/zero_sum_m5.c | 76 ++++++++ .../diffy_cav21_bench/zero_sum_m6.c | 86 +++++++++ src/frama_c.py | 147 +++++++-------- 160 files changed, 7677 insertions(+), 90 deletions(-) create mode 100644 data/analysis/ultimate_success_benchmarks.txt create mode 100644 data/benchmarks/diffy_cav21_bench/brs1.c create mode 100644 data/benchmarks/diffy_cav21_bench/brs2.c create mode 100644 data/benchmarks/diffy_cav21_bench/brs3.c create mode 100644 data/benchmarks/diffy_cav21_bench/brs4.c create mode 100644 data/benchmarks/diffy_cav21_bench/brs5.c create mode 100644 data/benchmarks/diffy_cav21_bench/cond1.c create mode 100644 data/benchmarks/diffy_cav21_bench/cond2.c create mode 100644 data/benchmarks/diffy_cav21_bench/cond2s1.c create mode 100644 data/benchmarks/diffy_cav21_bench/cond2s2.c create mode 100644 data/benchmarks/diffy_cav21_bench/conda.c create mode 100644 data/benchmarks/diffy_cav21_bench/condg.c create mode 100644 data/benchmarks/diffy_cav21_bench/condi.c create mode 100644 data/benchmarks/diffy_cav21_bench/condm.c create mode 100644 data/benchmarks/diffy_cav21_bench/condn.c create mode 100644 data/benchmarks/diffy_cav21_bench/condnl1.c create mode 100644 data/benchmarks/diffy_cav21_bench/conds.c create mode 100644 data/benchmarks/diffy_cav21_bench/conds2.c create mode 100644 data/benchmarks/diffy_cav21_bench/condsc.c create mode 100644 data/benchmarks/diffy_cav21_bench/condss.c create mode 100644 data/benchmarks/diffy_cav21_bench/condss1.c create mode 100644 data/benchmarks/diffy_cav21_bench/condss2.c create mode 100644 data/benchmarks/diffy_cav21_bench/condss3.c create mode 100644 data/benchmarks/diffy_cav21_bench/eqn1.c create mode 100644 data/benchmarks/diffy_cav21_bench/eqn2.c create mode 100644 data/benchmarks/diffy_cav21_bench/eqn3.c create mode 100644 data/benchmarks/diffy_cav21_bench/eqn4.c create mode 100644 data/benchmarks/diffy_cav21_bench/eqn5.c create mode 100644 data/benchmarks/diffy_cav21_bench/ifcomp.c create mode 100644 data/benchmarks/diffy_cav21_bench/ifeqn1.c create mode 100644 data/benchmarks/diffy_cav21_bench/ifeqn2.c create mode 100644 data/benchmarks/diffy_cav21_bench/ifeqn3.c create mode 100644 data/benchmarks/diffy_cav21_bench/ifeqn4.c create mode 100644 data/benchmarks/diffy_cav21_bench/ifeqn5.c create mode 100644 data/benchmarks/diffy_cav21_bench/ifncomp.c create mode 100644 data/benchmarks/diffy_cav21_bench/indp1.c create mode 100644 data/benchmarks/diffy_cav21_bench/indp2.c create mode 100644 data/benchmarks/diffy_cav21_bench/indp3.c create mode 100644 data/benchmarks/diffy_cav21_bench/indp4.c create mode 100644 data/benchmarks/diffy_cav21_bench/indp5.c create mode 100644 data/benchmarks/diffy_cav21_bench/modn.c create mode 100644 data/benchmarks/diffy_cav21_bench/modp.c create mode 100644 data/benchmarks/diffy_cav21_bench/mods.c create mode 100644 data/benchmarks/diffy_cav21_bench/ms1.c create mode 100644 data/benchmarks/diffy_cav21_bench/ms2.c create mode 100644 data/benchmarks/diffy_cav21_bench/ms3.c create mode 100644 data/benchmarks/diffy_cav21_bench/ms4.c create mode 100644 data/benchmarks/diffy_cav21_bench/ms5.c create mode 100644 data/benchmarks/diffy_cav21_bench/ncomp.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-as1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-as2.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-as3.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nli1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nli2.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nli3.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nlj1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nlj2.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nlj3.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nsna1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nsna2.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-nsna3.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-sa1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-sna1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-sna2.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-sna3.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-ss1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-ss2.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-ss3.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-sum.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-unb1.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-unb2.c create mode 100644 data/benchmarks/diffy_cav21_bench/nested-unb3.c create mode 100644 data/benchmarks/diffy_cav21_bench/nsqm-if.c create mode 100644 data/benchmarks/diffy_cav21_bench/nsqm.c create mode 100644 data/benchmarks/diffy_cav21_bench/pcomp.c create mode 100644 data/benchmarks/diffy_cav21_bench/res1.c create mode 100644 data/benchmarks/diffy_cav21_bench/res1o.c create mode 100644 data/benchmarks/diffy_cav21_bench/res2.c create mode 100644 data/benchmarks/diffy_cav21_bench/res2o.c create mode 100644 data/benchmarks/diffy_cav21_bench/s12if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s1if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s1lif.c create mode 100644 data/benchmarks/diffy_cav21_bench/s22if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s2if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s2lif.c create mode 100644 data/benchmarks/diffy_cav21_bench/s32if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s3if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s3lif.c create mode 100644 data/benchmarks/diffy_cav21_bench/s42if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s4if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s4lif.c create mode 100644 data/benchmarks/diffy_cav21_bench/s52if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s5if.c create mode 100644 data/benchmarks/diffy_cav21_bench/s5lif.c create mode 100644 data/benchmarks/diffy_cav21_bench/sanfoundry_27_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/sina1.c create mode 100644 data/benchmarks/diffy_cav21_bench/sina2.c create mode 100644 data/benchmarks/diffy_cav21_bench/sina3.c create mode 100644 data/benchmarks/diffy_cav21_bench/sina4.c create mode 100644 data/benchmarks/diffy_cav21_bench/sina5.c create mode 100644 data/benchmarks/diffy_cav21_bench/sqm-if.c create mode 100644 data/benchmarks/diffy_cav21_bench/sqm.c create mode 100644 data/benchmarks/diffy_cav21_bench/ss1.c create mode 100644 data/benchmarks/diffy_cav21_bench/ss2.c create mode 100644 data/benchmarks/diffy_cav21_bench/ss3.c create mode 100644 data/benchmarks/diffy_cav21_bench/ss4.c create mode 100644 data/benchmarks/diffy_cav21_bench/ssina.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_compareModified_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_compare_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy1_ground-1.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy2_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy3_ground-1.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy4_ground-1.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy5_ground-1.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy6_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy7_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy8_ground-1.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copy9_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copyInitSum2_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copyInitSum3_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copyInitSum_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_copyInit_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init1_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init2_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init3_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init4_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init5_ground-1.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init6_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init7_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init8_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_init9_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_maxInArray_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_minInArray_ground-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_password_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_running-2.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_seq_init_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_strcmp_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/standard_vector_difference_ground.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum1.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum2.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum3.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum4.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum5.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const1.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const2.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const3.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const4.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const5.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const_m2.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const_m3.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const_m4.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const_m5.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_const_m6.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_m2.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_m3.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_m4.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_m5.c create mode 100644 data/benchmarks/diffy_cav21_bench/zero_sum_m6.c diff --git a/data/analysis/svcomp_dataset.ipynb b/data/analysis/svcomp_dataset.ipynb index 1694d4aff..e34c7ae06 100644 --- a/data/analysis/svcomp_dataset.ipynb +++ b/data/analysis/svcomp_dataset.ipynb @@ -2,7 +2,7 @@ "cells": [ { "cell_type": "code", - "execution_count": 69, + "execution_count": 1, "metadata": {}, "outputs": [], "source": [ @@ -14,7 +14,7 @@ }, { "cell_type": "code", - "execution_count": 70, + "execution_count": 2, "metadata": {}, "outputs": [], "source": [ @@ -30,7 +30,7 @@ }, { "cell_type": "code", - "execution_count": 72, + "execution_count": 3, "metadata": {}, "outputs": [], "source": [ @@ -46,7 +46,7 @@ }, { "cell_type": "code", - "execution_count": 74, + "execution_count": 4, "metadata": {}, "outputs": [ { @@ -55,7 +55,7 @@ "544" ] }, - "execution_count": 74, + "execution_count": 4, "metadata": {}, "output_type": "execute_result" } @@ -66,7 +66,7 @@ }, { "cell_type": "code", - "execution_count": 76, + "execution_count": 5, "metadata": {}, "outputs": [], "source": [ @@ -77,7 +77,7 @@ }, { "cell_type": "code", - "execution_count": 81, + "execution_count": 6, "metadata": {}, "outputs": [], "source": [ @@ -93,7 +93,7 @@ }, { "cell_type": "code", - "execution_count": 85, + "execution_count": 7, "metadata": {}, "outputs": [], "source": [ @@ -110,7 +110,7 @@ }, { "cell_type": "code", - "execution_count": 86, + "execution_count": 8, "metadata": {}, "outputs": [ { @@ -119,7 +119,7 @@ "403" ] }, - "execution_count": 86, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -128,6 +128,41 @@ "len(final_positive_set)" ] }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [], + "source": [ + "ultimate_failure_file = open(\"ultimate_failed_benchmarks.txt\", \"r\", encoding=\"utf-8\").read().splitlines()" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [], + "source": [ + "ultimate_success = []\n", + "ultimate_failure = []\n", + "\n", + "for f in final_positive_set:\n", + " if f in ultimate_failure_file:\n", + " ultimate_failure.append(f)\n", + " else:\n", + " ultimate_success.append(f)" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "metadata": {}, + "outputs": [], + "source": [ + "with open(\"ultimate_success_benchmarks.txt\", \"w\", encoding='utf-8') as f:\n", + " f.write(\"\\n\".join(ultimate_success))" + ] + }, { "cell_type": "code", "execution_count": 87, diff --git a/data/analysis/ultimate_success_benchmarks.txt b/data/analysis/ultimate_success_benchmarks.txt new file mode 100644 index 000000000..a3e4c49cb --- /dev/null +++ b/data/analysis/ultimate_success_benchmarks.txt @@ -0,0 +1,170 @@ +../../sv-benchmarks/c/bitvector/gcd_4.c +../../sv-benchmarks/c/bitvector/modulus-2.c +../../sv-benchmarks/c/bitvector/soft_float_2a.c.cil.c +../../sv-benchmarks/c/bitvector/soft_float_5a.c.cil.c +../../sv-benchmarks/c/floats-cbmc-regression/float-div1.c +../../sv-benchmarks/c/floats-cbmc-regression/float-no-simp2.c +../../sv-benchmarks/c/floats-cbmc-regression/float-no-simp4.c +../../sv-benchmarks/c/floats-cbmc-regression/float-no-simp6.c +../../sv-benchmarks/c/floats-cbmc-regression/float-rounding1.c +../../sv-benchmarks/c/floats-cbmc-regression/float-to-double1.c +../../sv-benchmarks/c/floats-cbmc-regression/float-zero-sum1.c +../../sv-benchmarks/c/floats-cbmc-regression/float14.c +../../sv-benchmarks/c/floats-cbmc-regression/float19.c +../../sv-benchmarks/c/floats-cbmc-regression/float20.c +../../sv-benchmarks/c/floats-cbmc-regression/float21.c +../../sv-benchmarks/c/floats-cbmc-regression/float3.c +../../sv-benchmarks/c/floats-cbmc-regression/float4.c +../../sv-benchmarks/c/floats-cbmc-regression/float8.c +../../sv-benchmarks/c/floats-cbmc-regression/float_lib2.c +../../sv-benchmarks/c/floats-esbmc-regression/trunc_nondet_2.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0250a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0250b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0260.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0281.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0470.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0480.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0490a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0490b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0730a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0730b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0740.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0910b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0920a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0920b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0931.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0960b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0970a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0970b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_0981.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1032c.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1032d.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1052a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1052b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1092c.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1092d.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1230.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1231b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1232a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1250.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1251b.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1252a.c +../../sv-benchmarks/c/float-newlib/double_req_bl_1300.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0250a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0250b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0260.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0281.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0460.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0470.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0480.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0490a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0490b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0710.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0730a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0730b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0730c.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0740.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0910a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0910b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0920a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0920b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0931.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0960a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0960b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0970a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0970b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_0981.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1072a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1072b.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1230.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1231.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1232a.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1250.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1251.c +../../sv-benchmarks/c/float-newlib/float_req_bl_1252a.c +../../sv-benchmarks/c/ldv-regression/test_cut_trace.i +../../sv-benchmarks/c/ldv-sets/test_add-2.c +../../sv-benchmarks/c/loops/trex01-2.c +../../sv-benchmarks/c/loops/trex04.c +../../sv-benchmarks/c/loops/trex04_abstracted.c +../../sv-benchmarks/c/loops/while_infinite_loop_3.c +../../sv-benchmarks/c/loop-acceleration/functions_1-1.c +../../sv-benchmarks/c/loop-acceleration/nested_1-1.c +../../sv-benchmarks/c/loop-invgen/SpamAssassin-loop.c +../../sv-benchmarks/c/loop-invgen/apache-get-tag.c +../../sv-benchmarks/c/loop-invgen/nest-if3.c +../../sv-benchmarks/c/loops-crafted-1/loopv2.c +../../sv-benchmarks/c/loops-crafted-1/nested5-1.c +../../sv-benchmarks/c/loops-crafted-1/sum_by_3_abstracted.c +../../sv-benchmarks/c/nla-digbench/cohendiv-ll.c +../../sv-benchmarks/c/nla-digbench/fermat1-ll.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound1.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound10.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound100.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound2.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound20.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound5.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound50.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound10.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound100.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound20.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound5.c +../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound50.c +../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_unwindbound1.c +../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_unwindbound2.c +../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin2_unwindbound1.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin2_unwindbound2.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin2_unwindbound5.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin2_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin2_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin_unwindbound1.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin_unwindbound2.c +../../sv-benchmarks/c/nla-digbench-scaling/divbin_unwindbound5.c +../../sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/egcd3-ll_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/egcd3-ll_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound10.c +../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound100.c +../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound20.c +../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound5.c +../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound50.c +../../sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound10.c +../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound100.c +../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound2.c +../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound20.c +../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound5.c +../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound50.c +../../sv-benchmarks/c/nla-digbench-scaling/knuth_valuebound1.c +../../sv-benchmarks/c/nla-digbench-scaling/knuth_valuebound2.c +../../sv-benchmarks/c/recursive/Ackermann01-2.c +../../sv-benchmarks/c/recursive/Ackermann03.c +../../sv-benchmarks/c/recursive/Ackermann04.c +../../sv-benchmarks/c/recursive/Addition01-2.c +../../sv-benchmarks/c/recursive/Fibonacci01-1.c +../../sv-benchmarks/c/recursive/Fibonacci02.c +../../sv-benchmarks/c/recursive/Fibonacci03.c +../../sv-benchmarks/c/recursive/McCarthy91-2.c +../../sv-benchmarks/c/recursive/Primes.c +../../sv-benchmarks/c/recursive/gcd01-1.c +../../sv-benchmarks/c/recursive/recHanoi02-2.c +../../sv-benchmarks/c/recursive/recHanoi03-2.c +../../sv-benchmarks/c/recursive-simple/fibo_2calls_10-1.c +../../sv-benchmarks/c/recursive-simple/id2_b2_o3.c +../../sv-benchmarks/c/recursive-simple/id2_b3_o5.c +../../sv-benchmarks/c/recursive-simple/id2_b5_o10.c +../../sv-benchmarks/c/recursive-simple/id_b2_o3.c +../../sv-benchmarks/c/recursive-simple/id_b3_o5-2.c +../../sv-benchmarks/c/recursive-simple/id_b5_o10-2.c +../../sv-benchmarks/c/recursive-simple/sum_non_eq-2.c +../../sv-benchmarks/c/systemc/pc_sfifo_1.cil-2.c +../../sv-benchmarks/c/systemc/pc_sfifo_2.cil-1.c \ No newline at end of file diff --git a/data/benchmarks/diffy_cav21_bench/brs1.c b/data/benchmarks/diffy_cav21_bench/brs1.c new file mode 100644 index 000000000..c803bdfb6 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/brs1.c @@ -0,0 +1,43 @@ +/* + * Benchmarks contributed by Divyesh Unadkat[1,2], Supratik Chakraborty[1], Ashutosh Gupta[1] + * [1] Indian Institute of Technology Bombay, Mumbai + * [2] TCS Innovation labs, Pune + * + */ + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int N; + +int main() +{ + N = __VERIFIER_nondet_int(); + if(N <= 0) return 1; + + int i; + int sum[1]; + int a[N]; + + for(i=0; i= 2); + } + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/conds2.c b/data/benchmarks/diffy_cav21_bench/conds2.c new file mode 100644 index 000000000..c3afcce49 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/conds2.c @@ -0,0 +1,45 @@ + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int N; + +int main() +{ + N = __VERIFIER_nondet_int(); + if(N <= 0) return 1; + + int i; + int sum[1]; + int a[N]; + int c[N]; + + sum[0] = 0; + for(i=0; i= sum[0]); + } + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/condss.c b/data/benchmarks/diffy_cav21_bench/condss.c new file mode 100644 index 000000000..4be2eca0d --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/condss.c @@ -0,0 +1,56 @@ + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int N; + +int main() +{ + N = __VERIFIER_nondet_int(); + if(N <= 0) return 1; + + int i; + int sum[1]; + int a[N]; + int b[N]; + int c[N]; + + sum[0] = 0; + for(i=0; i= sum[0]); + } + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/eqn1.c b/data/benchmarks/diffy_cav21_bench/eqn1.c new file mode 100644 index 000000000..93c09d7af --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/eqn1.c @@ -0,0 +1,41 @@ +/* + * Benchmarks contributed by Divyesh Unadkat[1,2], Supratik Chakraborty[1], Ashutosh Gupta[1] + * [1] Indian Institute of Technology Bombay, Mumbai + * [2] TCS Innovation labs, Pune + * + */ + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int N; + +int main() +{ + N = __VERIFIER_nondet_int(); + if(N <= 0) return 1; + + int i; + int a[N]; + int b[N]; + + a[0] = 2; + b[0] = 1; + for(i=1; i= array[ x ] ); + } + + return 0; +} diff --git a/data/benchmarks/diffy_cav21_bench/sina1.c b/data/benchmarks/diffy_cav21_bench/sina1.c new file mode 100644 index 000000000..5f86340c4 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/sina1.c @@ -0,0 +1,40 @@ +/* + * Benchmarks contributed by Divyesh Unadkat[1,2], Supratik Chakraborty[1], Ashutosh Gupta[1] + * [1] Indian Institute of Technology Bombay, Mumbai + * [2] TCS Innovation labs, Pune + * + */ + +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int N; + +int main() +{ + N = __VERIFIER_nondet_int(); + if(N <= 0) return 1; + + int i; + int sum[1]; + int a[N]; + + sum[0] = 0; + for(i=0; i max[0] ) { + max[0] = a[i]; + } + i = i + 1; + } + + int x; + for ( x = 0 ; x < N ; x++ ) { + __VERIFIER_assert( a[x] <= max[0] ); + } + return 0; +} diff --git a/data/benchmarks/diffy_cav21_bench/standard_minInArray_ground-2.c b/data/benchmarks/diffy_cav21_bench/standard_minInArray_ground-2.c new file mode 100644 index 000000000..c3784d663 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/standard_minInArray_ground-2.c @@ -0,0 +1,32 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int N; + +int main( ) { + N = __VERIFIER_nondet_int(); + int i; + int a[N]; + int min[1]; + + min[0]=0; + for(i = 0; i < N; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + i = 0; + while ( i < N ) { + if ( a[i] < min[0] ) { + min[0] = a[i]; + } + i = i + 1; + } + + int x; + for ( x = 0 ; x < N ; x++ ) { + __VERIFIER_assert( a[x] >= min[0] ); + } + return 0; +} diff --git a/data/benchmarks/diffy_cav21_bench/standard_password_ground.c b/data/benchmarks/diffy_cav21_bench/standard_password_ground.c new file mode 100644 index 000000000..b5a1e85a0 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/standard_password_ground.c @@ -0,0 +1,34 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(); + +int SIZE; +/* Invited talk at ETAPS 2014 */ + +int main( ) { + SIZE = __VERIFIER_nondet_int(); + int password[ SIZE ]; + int guess[ SIZE ]; + + int i; + int result[1]; + result[0] = 1; + + for (i = 0; i < SIZE; i++) + { + password[i] = __VERIFIER_nondet_int(); + guess[i] = __VERIFIER_nondet_int(); + } + + for ( i = 0 ; i < SIZE ; i++ ) { + if ( password[ i ] != guess[ i ] ) { + result[0] = 0; + } + } + + int x; + for ( x = 0 ; x < SIZE ; x++ ) { + __VERIFIER_assert( result[0] == 0 || password[ x ] == guess[ x ] ); + } + return 0; +} diff --git a/data/benchmarks/diffy_cav21_bench/standard_running-2.c b/data/benchmarks/diffy_cav21_bench/standard_running-2.c new file mode 100644 index 000000000..6094b2ed9 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/standard_running-2.c @@ -0,0 +1,35 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(); + +int N; +int main ( ) { + N = __VERIFIER_nondet_int(); + int a[N]; + int b[N]; + int i; + int f[1]; + + for(i = 0; i< N; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + i = 0; + while ( i < N ) { + if ( a[i] >= 0 ) b[i] = 1; + else b[i] = 0; + i = i + 1; + } + + f[0] = 1; + i = 0; + while ( i < N ) { + if ( a[i] >= 0 && !b[i] ) f[0] = 0; + if ( a[i] < 0 && b[i] ) f[0] = 0; + i = i + 1; + } + + __VERIFIER_assert ( f[0] == 1 ); + return 0; +} diff --git a/data/benchmarks/diffy_cav21_bench/standard_seq_init_ground.c b/data/benchmarks/diffy_cav21_bench/standard_seq_init_ground.c new file mode 100644 index 000000000..9edf6ba0a --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/standard_seq_init_ground.c @@ -0,0 +1,23 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(); + +int SIZE; +int main( ) { + SIZE = __VERIFIER_nondet_int(); + int a[SIZE]; + int i; + + a[0] = 7; + i = 1; + while( i < SIZE ) { + a[i] = a[i-1] + 1; + i = i + 1; + } + + int x; + for ( x = 1 ; x < SIZE ; x++ ) { + __VERIFIER_assert( a[x] >= a[x-1] ); + } + return 0; +} diff --git a/data/benchmarks/diffy_cav21_bench/standard_strcmp_ground.c b/data/benchmarks/diffy_cav21_bench/standard_strcmp_ground.c new file mode 100644 index 000000000..4e56239d4 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/standard_strcmp_ground.c @@ -0,0 +1,31 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(); + +int N; +int main( ) { + N = __VERIFIER_nondet_int(); + int i; + int a[N]; + int b[N]; + int c[1]; + + for(i = 0; i < N; i++) + { + a[i] = __VERIFIER_nondet_int(); + b[i] = __VERIFIER_nondet_int(); + } + + c[0] = 0; + i = 0; + while ( i < N ) { + if( a[i] != b[i] ) c[0] = 1; + i = i + 1; + } + + int x; + for ( x = 0 ; x < N ; x++ ) { + __VERIFIER_assert(c[0] == 1 || a[x] == b[x] ); + } + return 0; +} diff --git a/data/benchmarks/diffy_cav21_bench/standard_vector_difference_ground.c b/data/benchmarks/diffy_cav21_bench/standard_vector_difference_ground.c new file mode 100644 index 000000000..363290c09 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/standard_vector_difference_ground.c @@ -0,0 +1,39 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(); + +/* +From: "On Solving Universally Quantified Horn Clauses" +Bjorner, McMillan, and Rybalchenko +SAS 2013 +*/ + +int SIZE; + +int main( ) { + SIZE = __VERIFIER_nondet_int(); + int a[SIZE]; + int b[SIZE]; + int c[SIZE]; + int i = 0; + + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + b[i] = __VERIFIER_nondet_int(); + } + + i = 0; + while (i < SIZE) { + c[i] = a[i] - b[i]; + i = i + 1; + } + + int x; + for (x = 0; x < SIZE; x++) { + __VERIFIER_assert(c[x] == a[x] - b[x]); + } + + return 0; +} + diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum1.c b/data/benchmarks/diffy_cav21_bench/zero_sum1.c new file mode 100644 index 000000000..a66d62a86 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum1.c @@ -0,0 +1,36 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0] = 0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum2.c b/data/benchmarks/diffy_cav21_bench/zero_sum2.c new file mode 100644 index 000000000..a2ea14848 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum2.c @@ -0,0 +1,46 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum3.c b/data/benchmarks/diffy_cav21_bench/zero_sum3.c new file mode 100644 index 000000000..06efd661a --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum3.c @@ -0,0 +1,56 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum4.c b/data/benchmarks/diffy_cav21_bench/zero_sum4.c new file mode 100644 index 000000000..8f9880ee7 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum4.c @@ -0,0 +1,66 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum5.c b/data/benchmarks/diffy_cav21_bench/zero_sum5.c new file mode 100644 index 000000000..a9344d44a --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum5.c @@ -0,0 +1,76 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const1.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const1.c new file mode 100644 index 000000000..8eea1ddab --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const1.c @@ -0,0 +1,36 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const2.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const2.c new file mode 100644 index 000000000..53a887281 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const2.c @@ -0,0 +1,46 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const3.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const3.c new file mode 100644 index 000000000..aa33b1069 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const3.c @@ -0,0 +1,56 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const4.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const4.c new file mode 100644 index 000000000..44847c932 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const4.c @@ -0,0 +1,66 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const5.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const5.c new file mode 100644 index 000000000..68575c92e --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const5.c @@ -0,0 +1,76 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const_m2.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m2.c new file mode 100644 index 000000000..c8336f7ab --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m2.c @@ -0,0 +1,46 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const_m3.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m3.c new file mode 100644 index 000000000..38fbb2299 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m3.c @@ -0,0 +1,56 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const_m4.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m4.c new file mode 100644 index 000000000..189a7a3ec --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m4.c @@ -0,0 +1,66 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const_m5.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m5.c new file mode 100644 index 000000000..1128a0537 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m5.c @@ -0,0 +1,76 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_const_m6.c b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m6.c new file mode 100644 index 000000000..4293921f9 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_const_m6.c @@ -0,0 +1,86 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = 1; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_m2.c b/data/benchmarks/diffy_cav21_bench/zero_sum_m2.c new file mode 100644 index 000000000..19ff7bba6 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_m2.c @@ -0,0 +1,46 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_m3.c b/data/benchmarks/diffy_cav21_bench/zero_sum_m3.c new file mode 100644 index 000000000..744bacad8 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_m3.c @@ -0,0 +1,56 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_m4.c b/data/benchmarks/diffy_cav21_bench/zero_sum_m4.c new file mode 100644 index 000000000..54681a931 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_m4.c @@ -0,0 +1,66 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_m5.c b/data/benchmarks/diffy_cav21_bench/zero_sum_m5.c new file mode 100644 index 000000000..06ef9a175 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_m5.c @@ -0,0 +1,76 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/data/benchmarks/diffy_cav21_bench/zero_sum_m6.c b/data/benchmarks/diffy_cav21_bench/zero_sum_m6.c new file mode 100644 index 000000000..80c9435c1 --- /dev/null +++ b/data/benchmarks/diffy_cav21_bench/zero_sum_m6.c @@ -0,0 +1,86 @@ +extern void __VERIFIER_error() __attribute__ ((__noreturn__)); +extern void __VERIFIER_assume(int); +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } } +extern int __VERIFIER_nondet_int(void); + +int SIZE; + +int main() +{ + SIZE = __VERIFIER_nondet_int(); + if(SIZE <= 0) return 1; + + int i; + int a[SIZE]; + int sum[1]; + + sum[0]=0; + for(i = 0; i < SIZE; i++) + { + a[i] = __VERIFIER_nondet_int(); + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] + a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + for(i = 0; i < SIZE; i++) + { + sum[0] = sum[0] - a[i]; + } + + __VERIFIER_assert(sum[0] == 0); + + return 1; +} diff --git a/src/frama_c.py b/src/frama_c.py index 41d89cb23..7103c0803 100644 --- a/src/frama_c.py +++ b/src/frama_c.py @@ -71,9 +71,26 @@ def check( user_assertions = [] loop_variant = "" function_contracts = [] + csv_dump = [] csv_loop_invariants = {} success = False + if not os.path.exists(temp_output_dump_file): + return False, "No CSV output dump found from Frama-C" + + with open(temp_output_dump_file, "r", encoding="utf-8") as f: + csv_dump_full = [row for row in csv.DictReader(f, delimiter="\t")] + csv_dump = [ + row + for row in csv_dump_full + if not row["directory"] == "FRAMAC_SHARE/libc" + ] + csv_loop_invariants = { + int(row["line"]): row["status"] + for row in csv_dump + if row["property kind"] == "loop invariant" + } + """ Get the status of each loop invariant """ @@ -81,17 +98,6 @@ def check( if not os.path.exists(temp_wp_json_report_file): return False, "No JSON report found" - if not os.path.exists(temp_output_dump_file): - return False, "No CSV output dump found from Frama-C" - - with open(temp_output_dump_file, "r", encoding="utf-8") as f: - csv_dump = [row for row in csv.DictReader(f, delimiter="\t")] - csv_loop_invariants = { - int(row["line"]): row["status"] - for row in csv_dump - if row["property kind"] == "loop invariant" - } - with open(temp_wp_json_report_file, "r", encoding="utf-8") as f: json_output = f.read() json_output = re.sub(r"(\d+)\.,", r"\1.0,", json_output) @@ -176,74 +182,58 @@ def check( else: # Parse the output dump - if not os.path.exists(temp_output_dump_file): - return False, "No CSV output dump found from Frama-C" - - with open(temp_output_dump_file, "r", encoding="utf-8") as f: - csv_dump = [row for row in csv.DictReader(f, delimiter="\t")] + success = all( + row["status"] == "Valid" + for row in checker_output + if row["property kind"] == "loop invariant" + or row["property kind"] == "user assertion" + ) - success = all( - row["status"] == "Valid" - for row in checker_output + loop_invariants = "\n".join( + [ + f"Invariant {row['property']} on line {row['line']}: {row['status']}" + for row in csv_dump if row["property kind"] == "loop invariant" - or row["property kind"] == "user assertion" - ) - - loop_invariants = "\n".join( - [ - f"Invariant {row['property']} on line {row['line']}: {row['status']}" - for row in csv_dump - if row["property kind"] == "loop invariant" - ] - ) - - if not check_variant and not os.path.exists(temp_output_dump_file): - return False, "No CSV output dump found from Frama-C" + ] + ) """ Get the status of each user assertion and function contract """ - with open(temp_output_dump_file, "r", encoding="utf-8") as f: - csv_dump = [row for row in csv.DictReader(f, delimiter="\t")] - - if check_contracts: - success = success and all( - row["status"] == "Valid" - for row in csv_dump - if row["property kind"] == "precondition" - or row["property kind"] == "postcondition" - ) - - for row in csv_dump: - if row["property kind"] == "precondition": - function_contracts.append( - f"Pre-condition {row['property']} on line {row['line']}: {row['status']}" - ) - elif row["property kind"] == "postcondition": - function_contracts.append( - f"Post-condition {row['property']} on line {row['line']}: {row['status']}" - ) - - function_contracts = "\n".join(function_contracts) - + if check_contracts: success = success and all( row["status"] == "Valid" for row in csv_dump - if row["property kind"] == "user assertion" + if row["property kind"] == "precondition" + or row["property kind"] == "postcondition" ) - user_assertions = "\n".join( - [ - f"Assertion {row['property']}: " - + ( - f"Unproven" - if row["status"] == "Unknown" - else f"{row['status']}" + for row in csv_dump: + if row["property kind"] == "precondition": + function_contracts.append( + f"Pre-condition {row['property']} on line {row['line']}: {row['status']}" ) - for row in csv_dump - if row["property kind"] == "user assertion" - ] - ) + elif row["property kind"] == "postcondition": + function_contracts.append( + f"Post-condition {row['property']} on line {row['line']}: {row['status']}" + ) + + function_contracts = "\n".join(function_contracts) + + success = success and all( + row["status"] == "Valid" + for row in csv_dump + if row["property kind"] == "user assertion" + ) + + user_assertions = "\n".join( + [ + f"Assertion {row['property']}: " + + (f"Unproven" if row["status"] == "Unknown" else f"{row['status']}") + for row in csv_dump + if row["property kind"] == "user assertion" + ] + ) """ Check the status of the loop variant @@ -321,8 +311,10 @@ def houdini( unknown_clause_lines = self.get_line_nums_for_unknown_contract_clauses( checker_message ) - for line_no in unknown_clause_lines: - code_lines[line_no] = "" + if len(unknown_clause_lines) > 0: + for line_no in unknown_clause_lines: + code_lines[line_no] = "" + code_queue.append("\n".join(code_lines)) if "Annotation error " in checker_message: # TODO: Why not remove all annotation errors? @@ -1411,10 +1403,11 @@ def add_boiler_plate(self, code): main_definition_type = main_definition.child_by_field_name("type") code = ( - ( - "#define assume(e) if(!(e)) return;\n" - if main_definition_type.text.decode("utf-8") == "void" - else "#define assume(e) if(!(e)) return 0;\n" + ("#include \n#define assume(e) if(!(e)) exit(-1);\n") + + ( + "#define abort() exit(-2);\n" + if len(re.findall(r"abort\s*\(\s*\)", code)) > 0 + else "" ) + ("#define LARGE_INT 1000000\n" if "LARGE_INT" in code else "") + ("extern int unknown(void);\n" if "unknown()" in code else "") @@ -1580,12 +1573,6 @@ def remove_reach_error_calls(self, code): + "{; \n//@ assert(\\false);\n}" + code[function_call[0].end_byte :] ) - elif function_call[1] == "abort": - code = ( - code[: function_call[0].start_byte] - + "return -1;" - + code[function_call[0].end_byte :] - ) return code @@ -1624,7 +1611,7 @@ def all_functions_defined_in_program(self, input_code): for f in function_calls: f_call = f.split("(")[0].strip() - if f_call == "assume": + if f_call == "assume" or f_call == "abort": continue fname = re.match(r"unknown_(int|uint|bool|float|double|char|uchar)", f_call) if fname is not None: