izlatkin / HornLauncher

scripts and reports for executions seahorn and test generation
0 stars 0 forks source link

[loops] Benchmarks with low coverage #37

Open izlatkin opened 2 years ago

izlatkin commented 2 years ago

apache-get-tag.i.p+nlh-reducer.c - huge benchmark with a lot of conditions apache-get-tag.i.p+sep-reducer.c - huge benchmark with a lot of conditions benchmark09_conjunctive.c image diamond_2-2.c image n.c11.c image n.c24.c image string-1.c Error: key \d+ not found image string-2.c Error: key \d+ not found image terminator_02-2.c Error: key \d+ not found image veris.c_OpenSER_cases1_stripFullBoth_arr.c Error: key \d+ not found image vogal-1.c image MADWiFi-encode_ie_ok.c image apache-escape-absolute.i.v+cfa-reducer.c Big benchmark

benchmark28_linear.c image benchmark37_conjunctive.c image benchmark43_conjunctive.c image benchmark46_disjunctive.c image gauss_sum.i.p+lhb-reducer.c image gsv2008.c.i.v+lhb-reducer.c image jm2006.c image jm2006.c.i.v+cfa-reducer.c image mod3.c.v+cfa-reducer.c image multivar_1-1.c image n.c40.c image nested9.c image simple_array_index_value_4.i.v+nlh-reducer.c image

I am not sure that there is one feature of benchmarks, but I noticed a few moments witch could affected the results

  1. Case when coverage is significantly low: A) TG could not find a condition for a branch that guards several other conditions, so they stay uncovered B) “Key not found” - compiler merge conditions
  2. Case when coverage is less than 20% lower than VeriFuzz: A) One of the double conditions is not coverage (for example: x < 100 && y < 100) B) Arrays C) goto D) border cases, like x > LARGE_INT
izlatkin commented 2 years ago

recheck: vogal-1.c

grigoryfedyukovich commented 2 years ago

For vogal-1.c, we have Error: key 22437 not found