pschanely

from crosshair.core_and_libs import proxy_for_type, standalone_statespace
from pathlib import PurePath
from crosshair.core import NoTracing
from crosshair.libimpl.builtinslib import (LazyIntSymbolicStr, SymbolicBoundedIntTuple)
                                           
with standalone_statespace:
    with NoTracing():
        # Any of these definitions will exhibit the issue,
        # because we don't really do anything with the string:
        

pschanely

from crosshair.core_and_libs import proxy_for_type, standalone_statespace
from pathlib import PurePath
from crosshair.core import NoTracing
from crosshair.libimpl.builtinslib import (LazyIntSymbolicStr, SymbolicBoundedIntTuple)
                                           
with standalone_statespace:
    with NoTracing():
        symbolic = LazyIntSymbolicStr(
            SymbolicBoundedIntTuple((1, 2, 3), "tempname")
        )

pschanely

import re

def f():
  '''
  post: True
  '''
  dict(foo=1)

pschanely

def make_bigger(n: int) -> int:
  '''
  post: __return__ != 0
  '''
  return 2 * n + 10

pschanely

import re
from typing import Optional

def parse_year(yearstring: str) -> Optional[int]:
    '''
    Something is wrong with this year parser! Can you guess what it is?
    
    post: __return__ is None or 1000 <= __return__ <= 9999
    '''
    return int(yearstring) if re.match('[1-9][0-9][0-9][0-9]', yearstring) else None

pschanely

from fractions import Fraction

def test(n1: int, n2: int) -> None:
    '''
    post: True
    '''
    assert n2 > 0
    print(Fraction(n1, n2))

pschanely

import typing

class Foo:
    def __init__(self, values: list) -> None:
        self._values = values


def fn(_: bool):
    """ post: True """
    return typing.get_type_hints(Foo)

pschanely

def make_bigger(n: int) -> int:
  '''
  post: __return__ != 0
  '''
  return 2 * n + 10

pschanely

import hashlib

def dohash(buf: bytes):
    """ post: True """
    return hashlib.sha256(buf)

pschanely

import dataclasses
from typing import List

@dataclasses.dataclass
class AverageableQueue:
    '''
    A queue of numbers with a O(1) average() operation.
    inv: self._total == sum(self._values)
    '''
    _values = []