### Function Call Example

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.error_trace.txt

Example of a function call, likely for initialization or setup.

```c
FunctionCall(__BLAST_initialize_/mnt/cluster/work/work/current--X--drivers/--X--ldv.317linux-3.0.1--X--08_1--X--68_1/linux-3.0.1/csd_deg_dscv/3373/dscv_tempdir/dscv/cmdfiles/rcv/08_1/preprocessed/drivers-isdn-mISDN-timerdev.o.usual.i())

```

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

### Example Build Command with Variables

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/Makefile-README.md

Example of how to set Makefile variables like CC and VERBOSE from the command line during a build.

```bash
make CC=clang VERBOSE=1
```

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

### Example Library Call Sequence (Server Benchmark)

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/openssl/README.txt

This sequence represents a specific series of library calls that should be impossible to execute in the context of the ssl3_accept function for server benchmarks.

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

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

### License Header Example

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/CONTRIBUTING.md

Example of a machine-readable header for copyright and license declaration, following the REUSE Specification.

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

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

### Build All Benchmarks in a Directory

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/Makefile-README.md

Navigate to the desired directory and run 'make' to build all benchmarks within that directory and its children.

```bash
cd <DIR>
make
```

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

### Build a Single Benchmark from .i File

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/Makefile-README.md

To build a specific benchmark from its .i file, navigate to its directory and use 'make <NAME>.oi'.

```bash
cd array-examples/
make standard_copy5_true-unreach-call_ground.oi
```

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

### Main Function Initialization

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/openssl/s3_srvr.blast.03_true-unreach-call.i.cil.c.error_trace.txt

Initializes SSL structures and calls ssl3_accept. Demonstrates memory allocation for SSL and its session state.

```c
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 ***
    ...
}
```

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

### Build a Single Benchmark from .c File

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/Makefile-README.md

To build a specific benchmark from its .c file, navigate to its directory and use 'make <NAME>.oc'.

```bash
cd array-examples/
make standard_copy5_true-unreach-call_ground.oc
```

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

### Return Statement Example

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko_false-unreach-call.error_trace.txt

A simple return statement indicating a successful operation or exit.

```c
Return(0);

```

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

### Interactive Program Notice

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/LICENSES/GPL-2.0-or-later.txt

Display this notice when a program starts in interactive mode. It provides basic information and directs users to commands for more details on warranty and redistribution.

```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.
```

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

### Build All Benchmarks

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/Makefile-README.md

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

```bash
make
```

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

### Property File Content Example

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/ldv-multiproperty/README.txt

A property file lists every error function corresponding to a property violation, typically used in conjunction with a CHECK statement for verification.

```c
CHECK( init(main()), LTL(G ! call(__VERIFIER_error_<property>())) )
```

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

### Create New Benchmark Directory

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/Makefile-README.md

Use 'mkdir <DIR>' to create a new directory for benchmarks.

```bash
mkdir <DIR>
```

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

### Get DMA Operations

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/ldv-linux-3.0/usb_urb-drivers-media-dvb-ttusb-dec-ttusb_dec.ko_false-unreach-call.error_trace.txt

Retrieves DMA (Direct Memory Access) operations for a given device. This snippet includes a check for a null device and uses __builtin_expect for optimization.

```c
Pred(dev@get_dma_ops  ==  0)
Block(__cil_tmp3@get_dma_ops = 1;)
FunctionCall(tmp@get_dma_ops = __builtin_expect(__cil_tmp3@get_dma_ops, 0))
Pred(tmp@get_dma_ops  !=  0)
Block(__retres4@get_dma_ops = dma_ops;)
Return(__retres4@get_dma_ops);
```

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

### Task Definition (Format 2.0)

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/README.md

Example of a task definition file using format version 2.0. It specifies 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

```

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

### Setting Benchmark Sets via Command Line

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/Makefile-README.md

Use the make command with the SET_FILES variable to build specific benchmark sets for quick testing.

```bash
$ make SET_FILES="BusyBox.set Floats.set"
```

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

### Interactive Mode Notice for GPL Programs

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/LICENSES/GPL-3.0-or-later.txt

A sample notice to display when a GPL-licensed program starts in interactive mode. This notice informs users about the program's warranty status and redistribution conditions.

```text
<program> Copyright (C) <year> <name of author>
This program 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 Goblint Regression Benchmark (28-race_reach)

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/goblint-regression/README.txt

This C code demonstrates a typical benchmark structure for the '28-race_reach' category. It utilizes custom macros for memory access and thread management, and includes a potential synchronization error for testing.

```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;
}
```

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

### Applying GPL-3.0+ to a New Program

Source: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/LICENSES/GPL-3.0-or-later.txt

Instructions for incorporating the GPL into a new software project. It's recommended to include copyright notices and a pointer to the full license text in each source file.

```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 3 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, see <https://www.gnu.org/licenses/>.
```