gorefinement

Refinement type checking for golang.

func f() {
  // a: { v: int | v >= 0 }
  a := 3
  
  // b: { v: int | v <= -100 }
  b := 3
  
  a = 0   // ok
  a = -1  // reports "UNSAFE"
  b = 1   // reports "UNSAFE"
  
  a = b   // reports "UNSAFE"
  a = -b  // ok
  a = b*b // ok
  a = a*b // reports "UNSAFE", because assignments like (a, b) = (0, -100) can violate condition
}

requirement

Z3 SMT Solver is required.

Download pre-built binaries from Z3 repository releases page, then place header and library files to appropriate path.

If you are using macOS, install from HomeBrew is recommended.