### Interactive Program Notice Example

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-validator-v0.6/LICENSE.GPLv2.txt

A short notice to display when an interactive program starts, informing users about its status and how to get more details on warranty and conditions.

```text
Gnomovision version 69, Copyright (C) year name of author
Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
This is free software, and you are welcome to redistribute it
under certain conditions; type `show c' for details.
```

--------------------------------

### Example Library Call Sequence (Server Benchmark)

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/openssl/README.txt

This sequence illustrates a specific series of library calls that a server benchmark aims to prove is impossible. It is checked within the ssl3_accept function.

```text
ssl3_get_client_hello -> ssl3_send_server_hello ->
ssl3_send_change_cipher_spec -> ssl3_get_finished ->
ssl3_send_finished -> ssl3_send_finished
```

--------------------------------

### Goblint Regression Test Example

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/goblint-regression/README.txt

A C code example demonstrating a Goblint regression test scenario before preprocessing. It uses macros for thread creation, access, and assertion, highlighting a potential issue with mutex usage.

```c
int global = 0;
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;

void *t_fun(void *arg) {
  pthread_mutex_lock(&mutex1);
  access(global);               // global++; global--
  pthread_mutex_unlock(&mutex1);
  return NULL;
}

int main(void) {
  create_threads(t);
  pthread_mutex_lock(&mutex2);  // <-- wrong mutex; the following will fail
  assert_racefree(global);      // verifier_assert(global == 0)
  pthread_mutex_unlock(&mutex2);
  join_threads(t);
  return 0;
}
```

--------------------------------

### Example Task Definition for C Program

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/README.md

This snippet shows an example extract from a task definition file for a C program. It specifies the format version, input files, properties with expected verdicts, and verification options.

```yaml
format_version: '2.0'

input_files: 'list-1.i'

properties:
  - property_file: ../properties/unreach-call.prp
    expected_verdict: true
  - property_file: ../properties/valid-memsafety.prp
    expected_verdict: false
    subproperty: valid-memtrack

options:
  language: C
  data_model: ILP32

```

--------------------------------

### License Header Template for SV-Benchmarks

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/CONTRIBUTING.md

This is an example of the required machine-readable header for all files, including copyright and license information. It follows the REUSE Specification.

```c
// This file is part of the SV-Benchmarks collection of verification tasks:
// https://github.com/sosy-lab/sv-benchmarks
//
// SPDX-FileCopyrightText: 2020 ...
//
// SPDX-License-Identifier: Apache-2.0
```

--------------------------------

### Build All Benchmarks

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/Makefile-README.md

Command to build all benchmarks from the top-level directory. Use -j<N> for parallel builds.

```makefile
make
```

--------------------------------

### Build Single Benchmark from .i file

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/Makefile-README.md

Build a specific benchmark using its .i source file. Assumes you are in the benchmark's directory.

```makefile
make standard_copy5_true-unreach-call_ground.oi
```

--------------------------------

### Set Compiler and Verbosity

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/Makefile-README.md

Example of setting the C compiler to clang and enabling verbose output during the build process.

```makefile
make CC=clang VERBOSE=1
```

--------------------------------

### Build Single Benchmark from .c file

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/Makefile-README.md

Build a specific benchmark using its .c source file. Assumes you are in the benchmark's directory.

```makefile
make standard_copy5_true-unreach-call_ground.oc
```

--------------------------------

### Adding License Header with REUSE Tool

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/CONTRIBUTING.md

Demonstrates how to use the 'reuse' tool to add a license header to a file. This command specifies a template, copyright holder, and license.

```bash
reuse addheader --template header.jinja2 --copyright "..." --license Apache-2.0 yourfile.c
```

--------------------------------

### SSL Structure Initialization

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/openssl/s3_srvr.blast.04_true-unreach-call.i.cil.c.error_trace.txt

Initializes the SSL structure and its components by allocating memory. This snippet shows the setup before the main function call.

```c
int main()
{
    SSL *s;
    ...
    s = malloc(sizeof(SSL));                        // s = 0x7fffff08
    s->s3 = malloc(sizeof(struct ssl3_state_st));   // s->s3 = 0x7ffff780 (stored @ 0x7fffff5c)
    s->session = malloc(sizeof(SSL_SESSION));
    s->state = 8464;
    tmp = ssl3_accept(s);                           // *** 1 ***
    ...
}
```

--------------------------------

### Copyright Disclaimer Example for a Company

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-validator-v0.6/LICENSE.GPLv2.txt

A sample copyright disclaimer for a company to sign, relinquishing copyright interest in a specific program written by an individual.

```text
Yoyodyne, Inc., hereby disclaims all copyright interest in the program
`Gnomovision' (which makes passes at compilers) written by James Hacker.

<signature of Ty Coon>, 1 April 1989
Ty Coon, President of Vice
```

--------------------------------

### Standard Copyright Notice for Free Software

Source: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-validator-v0.6/LICENSE.GPLv2.txt

Include this notice at the start of each source file to convey the exclusion of warranty and specify distribution terms under the GNU GPLv2.

```text
<one line to give the program's name and a brief idea of what it does.>
Copyright (C) <year>  <name of author>

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License along
with this program; if not, write to the Free Software Foundation, Inc.,
51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
```