diff --git a/.github/actions/benchexec-test/theta-short.xml b/.github/actions/benchexec-test/theta-short.xml new file mode 100644 index 0000000000..65491106ac --- /dev/null +++ b/.github/actions/benchexec-test/theta-short.xml @@ -0,0 +1,202 @@ +<?xml version="1.0"?> +<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-2.3.dtd"> +<benchmark tool="theta" timelimit="40 s" hardtimelimit="60 s"> + + <resultfiles>**/witness.*</resultfiles> + + <option name="--svcomp"/> + <option name="--portfolio">STABLE</option> + <option name="--loglevel">RESULT</option> + + + <rundefinition name="SV-COMP25_unreach-call"> + <tasks name="ReachSafety-Arrays"> + <includesfile>../sv-benchmarks/c/Arrays.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-BitVectors"> + <includesfile>../sv-benchmarks/c/BitVectors.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-ControlFlow"> + <includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-ECA"> + <includesfile>../sv-benchmarks/c/ECA.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Floats"> + <includesfile>../sv-benchmarks/c/Floats.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Heap"> + <includesfile>../sv-benchmarks/c/Heap.set</includesfile> + <includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Loops"> + <includesfile>../sv-benchmarks/c/Loops.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-ProductLines"> + <includesfile>../sv-benchmarks/c/ProductLines.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Recursive"> + <includesfile>../sv-benchmarks/c/Recursive.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Sequentialized"> + <includesfile>../sv-benchmarks/c/Sequentialized.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-XCSP"> + <includesfile>../sv-benchmarks/c/XCSP.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Combinations"> + <includesfile>../sv-benchmarks/c/Combinations.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Hardware"> + <includesfile>../sv-benchmarks/c/Hardware.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Hardness"> + <includesfile>../sv-benchmarks/c/Hardness.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + <tasks name="ReachSafety-Fuzzle"> + <includesfile>../sv-benchmarks/c/Fuzzle.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + + <tasks name="ConcurrencySafety-Main"> + <includesfile>../sv-benchmarks/c/Concurrency.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile> + </tasks> + </rundefinition> + + <rundefinition name="SV-COMP25_no-data-race"> + <tasks name="NoDataRace-Main"> + <includesfile>../sv-benchmarks/c/Concurrency.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/no-data-race.prp</propertyfile> + </tasks> + </rundefinition> + + <rundefinition name="SV-COMP25_valid-memcleanup"> + <tasks name="MemSafety-MemCleanup"> + <includesfile>../sv-benchmarks/c/Heap.set</includesfile> + <includesfile>../sv-benchmarks/c/Juliet.set</includesfile> + <includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/valid-memcleanup.prp</propertyfile> + </tasks> + </rundefinition> + + <rundefinition name="SV-COMP25_valid-memsafety"> + <tasks name="MemSafety-Arrays"> + <includesfile>../sv-benchmarks/c/Arrays.set</includesfile> + <includesfile>../sv-benchmarks/c/Heap-Termination.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile> + </tasks> + <tasks name="MemSafety-Heap"> + <includesfile>../sv-benchmarks/c/Heap.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile> + </tasks> + <tasks name="MemSafety-LinkedLists"> + <includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile> + </tasks> + <tasks name="MemSafety-Other"> + <includesfile>../sv-benchmarks/c/Loops.set</includesfile> + <includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile> + <includesfile>../sv-benchmarks/c/ControlFlow-Termination.set</includesfile> + <includesfile>../sv-benchmarks/c/Recursive.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile> + </tasks> + <tasks name="MemSafety-Juliet"> + <includesfile>../sv-benchmarks/c/Juliet.set</includesfile> + <!-- Exclude Juliet_test unsafe memsafety tasks without subproperty from competition. Originally excluded in commit 024bdad652 by @versokova --> + <exclude>../sv-benchmarks/c/Juliet_Test/*_bad.yml</exclude> + <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile> + </tasks> + + <tasks name="ConcurrencySafety-MemSafety"> + <includesfile>../sv-benchmarks/c/Concurrency.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile> + </tasks> + </rundefinition> + + <rundefinition name="SV-COMP25_no-overflow"> + <tasks name="NoOverflows-Main"> + <includesfile>../sv-benchmarks/c/Arrays.set</includesfile> + <includesfile>../sv-benchmarks/c/BitVectors.set</includesfile> + <includesfile>../sv-benchmarks/c/BitVectors-Termination.set</includesfile> + <includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile> + <includesfile>../sv-benchmarks/c/ControlFlow-Termination.set</includesfile> + <includesfile>../sv-benchmarks/c/ECA.set</includesfile> + <includesfile>../sv-benchmarks/c/Floats.set</includesfile> + <includesfile>../sv-benchmarks/c/Heap.set</includesfile> + <includesfile>../sv-benchmarks/c/Heap-Termination.set</includesfile> + <includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile> + <includesfile>../sv-benchmarks/c/Loops.set</includesfile> + <includesfile>../sv-benchmarks/c/Recursive.set</includesfile> + <includesfile>../sv-benchmarks/c/Sequentialized.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile> + <includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile> + <includesfile>../sv-benchmarks/c/XCSP.set</includesfile> + <includesfile>../sv-benchmarks/c/SoftwareSystems-AWS-C-Common.set</includesfile> + <includesfile>../sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/no-overflow.prp</propertyfile> + </tasks> + <tasks name="NoOverflows-Juliet"> + <includesfile>../sv-benchmarks/c/Juliet.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/no-overflow.prp</propertyfile> + </tasks> + + <tasks name="ConcurrencySafety-NoOverflows"> + <includesfile>../sv-benchmarks/c/Concurrency.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/no-overflow.prp</propertyfile> + </tasks> + </rundefinition> + + <rundefinition name="SV-COMP25_termination"> + <tasks name="Termination-BitVectors"> + <includesfile>../sv-benchmarks/c/BitVectors-Termination.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile> + </tasks> + <tasks name="Termination-MainControlFlow"> + <includesfile>../sv-benchmarks/c/ControlFlow-Termination.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile> + </tasks> + <tasks name="Termination-MainHeap"> + <includesfile>../sv-benchmarks/c/Heap-Termination.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile> + </tasks> + <tasks name="Termination-Other"> + <includesfile>../sv-benchmarks/c/Arrays.set</includesfile> + <includesfile>../sv-benchmarks/c/BitVectors.set</includesfile> + <includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile> + <includesfile>../sv-benchmarks/c/ECA.set</includesfile> + <includesfile>../sv-benchmarks/c/Floats.set</includesfile> + <includesfile>../sv-benchmarks/c/Heap.set</includesfile> + <includesfile>../sv-benchmarks/c/Loops.set</includesfile> + <includesfile>../sv-benchmarks/c/ProductLines.set</includesfile> + <includesfile>../sv-benchmarks/c/Recursive.set</includesfile> + <includesfile>../sv-benchmarks/c/Sequentialized.set</includesfile> + <includesfile>../sv-benchmarks/c/SoftwareSystems-uthash.set</includesfile> + <propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile> + </tasks> + + </rundefinition> + + + +</benchmark>