dwightguth

int value(int * restrict i) {
  return *i * 3;
}

dwightguth

#define restrict
#include<stdio.h>

int _foo = 100;

inline int value(int * restrict i) {
  return *i * 4;
}

main() {

dwightguth

type foo = Foo of int | Baz of baz
and baz = {foo: foo; bar: string}

dwightguth

[]

module BASIC-K
  sort K{} []
  sort KItem{} []
endmodule []

module KSEQ
  import BASIC-K []

dwightguth

[]

module BASIC-K
  sort SortK{} []
  sort SortKItem{} []
endmodule []

module KSEQ
  import BASIC-K []

dwightguth

specializations:
- - Nil{}
  - action: 1
    variables:
    - - 0
      - 0
- - Cons{}
  - specializations: []
    default:
      swap:

dwightguth

This code may be licensed under either the BSD 3-Clause License, or the Boost Open Source License 1.0.

BSD 3-Clause License

Copyright (c) 2019, Runtime Verification, Inc.
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

dwightguth

from z3 import *
npcs = []
biomes = []

class npc(object):
  def __init__(self, name):
    self.name = name
    self.sells = True
    self._loves = []
    self._likes = []

dwightguth

#fetchCoverageData ( 8277554891507775505279220911850293719734826420268574462026436790795686283050 ) <firefly>
  <kevm-coverage>
    <programID>
      .
    </programID>
    <previousPC>
      0
    </previousPC>
    <coverage>
      <coveragePC>

dwightguth

#fetchCoverageData ( 8277554891507775505279220911850293719734826420268574462026436790795686283050 ) <firefly>
  <kevm-coverage>
    <programID>
      .
    </programID>
    <previousPC>
      0
    </previousPC>
    <coverage>
      <coveragePC>