jon-whit

import argparse
import glob
import subprocess
import os

if __name__ == '__main__':

    parser = argparse.ArgumentParser(description="Reports svcomp benchmarks which have references to uninitialized memory.")
    parser.add_argument("--witness-dir", default=".", help="The directory containing the witeness files.")
    parser.add_argument("--bench-dir", default=".", help="The directory containing the benchmark files.")

jon-whit

import argparse
import glob
import os
import re

if __name__ == '__main__':

    parser = argparse.ArgumentParser(description="Reports svcomp benchmarks which have references to uninitialized memory.")
    parser.add_argument("--bench-dir", default=".", help="The directory containing the benchmark files that will be stripped.")
    parser.add_argument("--dest-dir", default="./stripped-files", help="The destination directory where stripped files will be placed.")

jon-whit

int main(void)
{ struct usb_serial *var_group1 = (struct usb_serial *) __VERIFIER_nondet_pointer();
  struct usb_device_id const *var_whiteheat_firmware_download_0_p1 = (struct usb_device_id const *) __VERIFIER_nondet_pointer();
  struct tty_struct *var_group2 = (struct tty_struct *) __VERIFIER_nondet_pointer();
  struct usb_serial_port *var_group3 = (struct usb_serial_port *) __VERIFIER_nondet_pointer();
  unsigned char const *var_whiteheat_write_6_p2 = (unsigned char const *) __VERIFIER_nondet_pointer();
  int var_whiteheat_write_6_p3 = __VERIFIER_nondet_int();
  unsigned int var_whiteheat_ioctl_10_p1 = __VERIFIER_nondet_uint();
  unsigned long var_whiteheat_ioctl_10_p2 = __VERIFIER_nondet_ulong();
  struct ktermios *var_whiteheat_set_termios_11_p2 = (struct ktermios *) __VERIFIER_nondet_pointer();

jon-whit

        // Get a pointer to the literal that needs assignment, if one exists
        if ((lp = is_unitclause(form->clauses[i], assigned, vals)) != NULL) {
            // COPY THE LITERAL POINTER
            lp1 = (literal*) malloc(sizeof(literal));
            memcpy(lp1, lp, sizeof(literal));

            assert_literal(lp1, vals, assigned);
            stack_item si = {lp1, i, 0};

            // COPY THE STACK ITEM

jon-whit

        // Get a pointer to the literal that needs assignment, if one exists
        if ((lp = is_unitclause(form->clauses[i], assigned, vals)) != NULL) 
        {

            assert_literal(lp, vals, assigned);
            stack_item si = {lp, i, 0};

            push_stack(&s, &si);
        }
        

jon-whit

int solve(formula* form)
{
    /* Create the structures to store the state of the
     * algorithm */
    bool *assigned = (bool *) calloc(form->nvars + 1, sizeof(bool));
    bool *vals = (bool *) calloc(form->nvars + 1, sizeof(bool));
    stack_item **sitems = (stack_item **) malloc(form->nvars * sizeof(stack_item*));

    stack s;
    s.items = sitems;

jon-whit

swagger: "2.0"
info:
  description: |
    A simple Pubsub messaging API that allows clients to:
      * Publish messages to a Topic
      * Create Subscriptions to a Topic
      * Pull messages from Subscriptions
      * Acknowledge receipt of the messages delivered to a Subscription.
      
      Example:

jon-whit

package lookup

import (
    "fmt"

    openfgapb "go.buf.build/openfga/go/openfga/api/openfga/v1"
    "golang.org/x/sync/errgroup"
)

func Lookup(req *openfgapb.LookupRequest, srv openfgapb.OpenFGAService_LookupServer) error {

jon-whit

package lookup

import (
    "context"
    "fmt"
    "sync/atomic"

    openfgapb "go.buf.build/openfga/go/openfga/api/openfga/v1"
    "golang.org/x/sync/errgroup"
)

jon-whit

	t.Run("dispatch_direct_userset_lookups", func(t *testing.T) {
		ds := memory.New()
		ctx := storage.ContextWithRelationshipTupleReader(context.Background(), ds)

		storeID := ulid.Make().String()

		model := parser.MustTransformDSLToProto(`model
	  schema 1.1
	
	type user