Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit db044b7

Browse files
committed
Update task defs with properties coverage-branches and coverage-error-call
Over the course of the last year, a lot of tasks were fixed and a a lot of tasks were added. Most of the time, people did not consider the coverage-* properties for these tasks, so let's add them now. Properties are added according to the criteria stated in !842: * Compiles, if __VERIFIER_X method definitions are provided, * No termination property or expected verdict for termination is true, and * Some _VERIFIER_nondet* method exists that is not only declared, but used in at least one other location Compliance is checked and properties are added with the scripts found at https://gist.github.com/lembergerth/1a1bf782931fb16af0d9e4bc1085a737 . Ability to compile is checked with `bin/prtest --compile-only`, PRTest version https://gitlab.com/sosy-lab/software/prtest/-/tree/cc9cc249
1 parent 0fbf02b commit db044b7

File tree

14,472 files changed

+14950
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

14,472 files changed

+14950
-0
lines changed

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_01_bad.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: false
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_01_good.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: true
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_02_bad.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: false
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_02_good.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: true
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_03_bad.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: false
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_03_good.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: true
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_04_bad.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: false
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_04_good.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: true
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_05_bad.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: false
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

c/Juliet_Test/CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buffer_Overflow__CWE129_connect_socket_05_good.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ input_files: 'CWE121_Stack_Based_Buffer_Overflow---s01---CWE121_Stack_Based_Buff
55
properties:
66
- property_file: ../properties/valid-memsafety.prp
77
expected_verdict: true
8+
- property_file: ../properties/coverage-branches.prp
89

910
options:
1011
language: C

0 commit comments

Comments
 (0)