Skip to content

Instantly share code, notes, and snippets.

View Mr-Slippery's full-sized avatar

Cornel Izbașa Mr-Slippery

4 followers · 1 following
View GitHub Profile
@Mr-Slippery
Mr-Slippery / turing.c
Created February 11, 2021 23:03
Find the Turing machine that will produce a desired string.
#ifdef KLEE
#include <klee/klee.h>
#include <assert.h>
#endif
#ifndef KLEE
#include <string.h>
#include <stdio.h>
#endif
@Mr-Slippery
Mr-Slippery / taxi.c
Created November 19, 2020 22:06
Finding Ramanujan's taxicab number 1729 with KLEE
#include <klee/klee.h>
#include <assert.h>
#define N (15)
#define SYM(x) { \
klee_make_symbolic(&x, sizeof x, #x); \
}
int main() {
@Mr-Slippery
Mr-Slippery / einstein.c
Last active November 19, 2020 17:35
Solving Einstein's enigma with KLEE
#include <klee/klee.h>
#include <assert.h>
typedef enum {
NAT = 0,
COL = 1,
PET = 2,
DRI = 3,
SMO = 4
} cols_type;
@Mr-Slippery
Mr-Slippery / queens.c
Created November 19, 2020 17:15
Solving 8-queens with KLEE
#include <klee/klee.h>
#include <assert.h>
#define N 8
unsigned char queens[N];
int abs(int x)
{
return x >= 0 ? x: -x;
}
@Mr-Slippery
Mr-Slippery / hamilton.c
Last active November 19, 2020 15:09
Hamiltonian cycle finder with KLEE
#include <klee/klee.h>
#include <assert.h>
typedef unsigned char byte;
#define N 5
byte a[N * N]=
{
/* A B C D E*/
@Mr-Slippery
Mr-Slippery / klee_c.sh
Created November 18, 2020 20:49
Example invocation of KLEE on a sample source or user-supplied file
#!/usr/bin/env bash
set -euo pipefail
FILE=${1-main.cc}
if [ ! -f "${FILE}" ]
then
cat << EOF > "${FILE}"
#include <klee/klee.h>
#include <assert.h>
@Mr-Slippery
Mr-Slippery / mandel.rs
Last active April 5, 2020 16:27
ASCII rendering of Mandelbrot in Rust
extern crate num;
use num::complex::Complex;
struct IFS
{
max_iter: u64
}
trait DDS<State> {
@Mr-Slippery
Mr-Slippery / data_member_detection.cpp
Created March 5, 2020 17:41
Basic data member detection in C++17
#include <type_traits>
#define HAS_MEMBER(member) \
template <typename T, typename = void> \
struct has_##member : std::false_type {}; \
template <typename T> \
struct has_##member<T, std::void_t<decltype(std::declval<T>().member)>> : std::true_type {};
struct WithBla {
int bla;
@Mr-Slippery
Mr-Slippery / col3.py
Created November 6, 2019 21:01
Find counter examples to the conjecture: The orbit of all strictly positive natural numbers through col3 ends up in one of the two finite cycles.
#!/usr/bin/env python3
"""
Find counter examples to the conjecture:
The orbit of all strictly positive natural numbers
through col3 ends up in either C[0] and C[1].
"""
# Ignores PEP8 and pylint for brevity and math-friendly notation.
import sys
@Mr-Slippery
Mr-Slippery / klee_template.c
Created October 20, 2019 12:46
Template C file for verifying an array operation using KLEE
#ifdef KLEE
#include <klee/klee.h>
#include <assert.h>
#endif
#include <stdbool.h>
#ifndef KLEE
#include <stdio.h>
#endif