aprell

CC := gcc
CFLAGS += -Wall -Wextra -std=c99
LDLIBS += -lpthread

all: test_preload preload.so

# Make sure that `num_threads` is added to the dynamic symbol table
test_preload: LDFLAGS += -Wl,--export-dynamic
test_preload: test_preload.c

aprell

--- /usr/local/Cellar/ikos/2.1/lib/python3.7/site-packages/ikos/analyzer_orig.py	2019-02-14 11:21:52.000000000 +0100
+++ /usr/local/Cellar/ikos/2.1/lib/python3.7/site-packages/ikos/analyzer.py	2019-02-14 10:09:09.000000000 +0100
@@ -525,6 +525,8 @@
     return [
         # enable clang warnings
         '-Wall',
+        # silence nullability warnings
+        '-Wno-nullability-completeness',
         # disable source code fortification
         '-U_FORTIFY_SOURCE',

aprell

CPPFLAGS +=
CFLAGS += -Wall -Wextra -fsanitize=address,undefined
LDFLAGS += -fsanitize=address,undefined

ifeq ($(CC),clang)
  # ...
else
  # Assume gcc
  CC := gcc
  # ...

aprell

#!/usr/bin/env bash
# Code inspired by https://poormansprofiler.org

set -eu

if [ "$#" -ne 1 ]; then
    echo "Usage: $0 <program>"
    exit 0
fi

aprell

#include <stdio.h>
#include <string.h>

void print1(const char *str, int len)
{
    // Precision must be given as an int
    printf("%.*s\n", len, str);
}

void print2(const char *str, int len)

aprell

#include <assert.h>
#include <signal.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <sys/mman.h>

static void *guard_page;
static unsigned int interruptions;

aprell

#!/bin/bash
# A poor man's profiler
# Code adapted from https://poormansprofiler.org

set -eu

if [ "$#" -ne 2 ]; then
    echo "Usage: $0 <program> <nsamples>"
    exit 0
fi

aprell

// Exercise 0
method Max(a: int, b: int) returns (c: int)
    // ensures (a > b && c == a) || (a <= b && c == b)
    ensures a > b ==> c == a
    ensures a <= b ==> c == b
{
    if a > b { return a; }
    else { return b; }
}

aprell

#include <assert.h>
#include <stdbool.h>
#include <stdio.h>
#include <stdlib.h>
#include <omp.h>

// Default is 16 for each dimension
static int N;

#define A(i,j) A[(i)*N+(j)] // A: N x N

aprell

#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include <omp.h>

// Default is 10 for each dimension
static int N, M, K;

#define A(i,j) A[(i)*M+(j)] // A: N x M
#define B(i,j) B[(i)*K+(j)] // B: M x K