jepler

$ /tmp/cbmc -D FAIL mycmp.c  --trace 
CBMC version 5.6 64-bit x86_64 linux
Parsing mycmp.c
Converting
Type-checking mycmp
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation

jepler

#include <stdio.h>
#include <stdint.h>
#include <math.h>

#ifdef AVR
#include <avr/pgmspace.h>
#define printf_PP(s, ...) printf_P(PSTR(s), ## __VA_ARGS__)
#else
#define printf_PP(s, ...) printf(s, ## __VA_ARGS__)
#endif

jepler

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

int main() {
    double from = (1LL << 52), to = from + 2;
    long long bucket[3] = { 0 };
    int i;

    for (i = 0; i < 1000000; i++) {
        double r = from + (to - from) * (i / 1000000.);

jepler

#!/usr/bin/python
import sys
import tarfile

script = '''\
#!/bin/sh
exec sh -c 'dd bs=512 skip=1 if="$0" | tar xvf -' "$0"
'''

t = tarfile.TarInfo(name=script)

jepler

#include <stdlib.h>
#include <string.h>
#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>

int main() {
    for(int i=0; i<1000000; i++) {
        char s[16]; 
        snprintf(s, sizeof(s), "1.%06d", i);

jepler

Keybase proof

I hereby claim: * I am jepler on github. * I am jepler (https://keybase.io/jepler) on keybase. * I have a public key ASA0_fH8gDZNptnuiUi3UY-JRGWCOA9U4pVfk8XRJNDs2wo To claim this, I am signing this object:

{   "body": {     "key": {       "eldest_kid": "012034fdf1fc80364da6d9ee8948b7518f89446582380f54e2955f93c5d124d0ecdb0a",       "host": "keybase.io",       "kid": "012034fdf1fc80364da6d9ee8948b7518f89446582380f54e2955f93c5d124d0ecdb0a",       "uid": "e454d4676bab140824da8ee85556d019",       "username": "jepler"     },     "merkle_root": {       "ctime": 1570922042,       "hash": "80129943fb51953be7a5c21c32b68dfdd00194566cade08750ba34b52cf5080cbb3a285dfa5662543b6ea4c8b4313485267e9d2e16b8412b786eb286b3d6e5bc",       "hash_meta": "c4e5417bb113cc6e710253939b0c409ab74bf8a4b3ce7c1188867931c55049e4",       "seqno": 8069126     },     "service": {       "entropy": "CmcuzkA7vtioA9x/FBhMvLpr",       "name": "github",       "username": "jepler"     },     "type": "web_service_bind

jepler

WARNING: ThreadSanitizer: data race (pid=7514)
  Read of size 1 at 0x7fcf91400017 by thread T2:
    #0 gc_mark ../../py/gc.c:352 (micropython+0x19666)
    #1 gc_mark ../../py/gc.c:349 (micropython+0x19666)
    #2 gc_collect_root ../../py/gc.c:393 (micropython+0x19666)
    #3 gc_collect_regs_and_stack /home/jepler/src/circuitpython/ports/unix/gccollect.c:159 (micropython+0x73072)
    #4 mp_thread_gc /home/jepler/src/circuitpython/ports/unix/mpthreadport.c:65 (micropython+0x7351e)
    #5 <null> <null> (libtsan.so.0+0x28c0f)
    #6 array_append ../../py/objarray.c:356 (micropython+0x43fce)
    #7 array_construct ../../py/objarray.c:149 (micropython+0x44e70)

jepler

import analogio
import board

class AnalogJoystick:
    def __init__(self, pin_x=None, pin_y=None, x_invert=False, y_invert=False, deadzone=8000):
        self._x = analogio.AnalogIn(pin_x or board.JOYSTICK_X)
        self._y = analogio.AnalogIn(pin_y or board.JOYSTICK_Y)
        self.x_invert = x_invert
        self.y_invert = y_invert
        self.deadzone = deadzone

jepler

# CircuitPython demo - NeoPixel

import time
import board
import neopixel
import random

# Customize your neopixel configuration here...
pixel_pin = board.A1
num_pixels = const(96)

jepler

(gdb) p *$34
$83 = {CTRL = {bit = {SWRST = 0, DMAENABLE = 1, LVLEN0 = 1, LVLEN1 = 0, LVLEN2 = 0, LVLEN3 = 0}, vec = {LVLEN = 1}, reg = 258}, 
  CRCCTRL = {bit = {CRCBEATSIZE = 0, CRCPOLY = 0, CRCSRC = 0, CRCMODE = 0}, reg = 0}, CRCDATAIN = {bit = {CRCDATAIN = 0}, 
    reg = 0}, CRCCHKSUM = {bit = {CRCCHKSUM = 0}, reg = 0}, CRCSTATUS = {bit = {CRCBUSY = 0 '\000', CRCZERO = 0 '\000', 
      CRCERR = 0 '\000'}, reg = 0 '\000'}, DBGCTRL = {bit = {DBGRUN = 0 '\000'}, reg = 0 '\000'}, Reserved1 = "\000", 
  SWTRIGCTRL = {bit = {SWTRIG0 = 0, SWTRIG1 = 0, SWTRIG2 = 0, SWTRIG3 = 0, SWTRIG4 = 0, SWTRIG5 = 0, SWTRIG6 = 0, SWTRIG7 = 0, 
      SWTRIG8 = 0, SWTRIG9 = 0, SWTRIG10 = 0, SWTRIG11 = 0, SWTRIG12 = 0, SWTRIG13 = 0, SWTRIG14 = 0, SWTRIG15 = 0, SWTRIG16 = 0, 
      SWTRIG17 = 0, SWTRIG18 = 0, SWTRIG19 = 0, SWTRIG20 = 0, SWTRIG21 = 0, SWTRIG22 = 0, SWTRIG23 = 0, SWTRIG24 = 0, 
      SWTRIG25 = 0, SWTRIG26 = 0, SWTRIG27 = 0, SWTRIG28 = 0, SWTRIG29 = 0, SWTRIG30 = 0, SWTRIG31 = 0}, vec = {SWTRIG = 0}, 
    reg = 0}, P