quebex

A software analysis framework built around the QBE intermediate language

git clone https://git.8pit.net/quebex.git

 1// SPDX-FileCopyrightText: 2017-2020 TheAlgorithms and contributors
 2// SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>
 3//
 4// SPDX-License-Identifier: GPL-3.0-only
 5
 6#include <stddef.h>
 7
 8// Taken from: https://github.com/TheAlgorithms/C/blob/10d006c3b10340b901860e4810d2122b10e35b76/sorting/insertion_sort.c
 9
10extern void quebex_make_symbolic(void *, size_t, size_t, const char *);
11
12_Noreturn void __assert_fail(void) {
13    __builtin_unreachable();
14}
15
16void insertionSort(int *arr, int size)
17{
18    for (int i = 1; i < size; i++)
19    {
20        int j = i - 1;
21        int key = arr[i];
22        /* Move all elements greater than key to one position */
23        while (j >= 0 && key < arr[j])
24        {
25            arr[j + 1] = arr[j];
26            j = j - 1;
27        }
28        /* Find a correct position for key */
29        arr[j + 1] = key;
30        if (key == 42) {
31            __assert_fail();
32        }
33    }
34}
35
36#define INPUT_SIZE 3
37
38int
39main(void)
40{
41    int array[INPUT_SIZE];
42
43    quebex_make_symbolic(array, INPUT_SIZE, sizeof(int), "array");
44    insertionSort(array, INPUT_SIZE);
45
46    return 0;
47}