Skip to content

Instantly share code, notes, and snippets.


Jeff Epler jepler

View GitHub Profile
View gist:baf8e7da47f24e50bc2e
// cbmc cmbc.c ref.c jepler.c -DBUFSIZE=1 -DCMBC
#include "nibble.h"
#include <assert.h>
#include <inttypes.h>
#include <string.h>
uint64_t nondet_u64();
void main() {
uint64_t ref[BUFSIZE], res[BUFSIZE];
View gist:333668bb8a3a4e92580b
ns ns / 8 bytes entry name errors
42447 41.45 alexander2 0
42604 41.61 vetter4 0
44426 43.38 vetter3 64
54061 52.79 jepler 0
58071 56.71 jerome 0
62759 61.29 parnell 0
62967 61.49 burton2 0
79841 77.97 rjk9 0
80519 78.63 nadav 0
jepler / gist:5193404
Created Mar 19, 2013
python code to get title, link, and my comment from a newsblur blurblog feed
View gist:5193404
import os
import re
import sys
import xml.etree.ElementTree
import BeautifulSoup
def exc_wrap(f):
def inner(*args, **kw):
return f(*args, **kw)
jepler / build and run it..
Last active Dec 15, 2015
surprising optimization difference (I'm not quite courageous enough to call it a compiler bug yet). Additionally compiling it with -ffast-math gives the same result via the incomprehensible sequence below gcc version info: Target: x86_64-linux-gnu gcc version 4.7.2 (Debian 4.7.2-5) The wrong result turns out to be dot / (sqrt(radius) * radius * …
View build and run it..
jepler@babs:~$ gcc -Os rsq.c -lm && ./a.out
jepler@babs:~$ gcc -Os -funsafe-math-optimizations rsq.c -lm && ./a.out
jepler / gist:5315865
Created Apr 5, 2013
running the linuxcnc tests (or linuxcnc itself!) under clang with -fsanitize= produces some resuts, but I haven't found any "useful" ones yet.
View gist:5315865
$ halrun test.hal
test.hal:1: Warning: HAL_LIB: HAL will pretend that the exact base period requested is possible.
This mode is not suitable for running real hardware.
hal/components/sampler.c:429:22: runtime error: unsigned integer overflow: 0 - 1 cannot be represented in type 'unsigned long'
==22536==WARNING: ASan doesn't fully support makecontext/swapcontext functions and may produce false positives in some cases!
hal/components/sampler_usr.c:255:22: runtime error: unsigned integer overflow: 18446744073709551615 + 1 cannot be represented in type 'unsigned long'
View gist:5396405
mem = 1042
^?^?Use, duplication or disclosure is subject to
^?^?restrictions stated in Contract with Western
^?^?Electric Company, Inc.
# echo 'main() { printf("hi\n"); } ' > hi.c
# cc hi.c
View rtapi-atomic-proposal-untested.h
#if defined(__clang__) && __clang__
#elif defined(__GNUC__) && (__GNUC__ > 4) && (__GNUC_MINOR__ >= 7)
typedef unsigned long rtapi_atomic_type;
#define RTAPI_DIV_ROUND_UP(n,d) (((n) + (d) - 1) / (d))
jepler / gist:6763003
Created Sep 30, 2013
Python program that simulates habitrpg drops; each output line is "number of drops until full stable", "greatest number of excess eggs of any type", "greatest number of excess potions of any type".
View gist:6763003
from __future__ import division
import bisect
import random
import sys
# 9 animal types - even probability
# 10 potion types - uneven probability
# 1/5: set of 10
# 1/5: set of 9
import sha
import sys
f = open("/dev/urandom", "rb")
while 1:
message0 =
cs0 =[:2]
flip_bit = 1 << (ord( % 8)
View cbmc-out.txt
$ /tmp/cbmc -D FAIL mycmp.c --trace
CBMC version 5.6 64-bit x86_64 linux
Parsing mycmp.c
Type-checking mycmp
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation