gorefinement

package module
v0.0.0-...-60d02c1 Latest Latest
Warning

This package is not in the latest version of its module.

Go to latest
Published: Sep 4, 2020 License: MIT Imports: 13 Imported by: 0

README

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.

Documentation

Index

Constants

This section is empty.

Variables

View Source
var Analyzer = &analysis.Analyzer{
	Name: "gorefinement",
	Doc:  doc,
	Run:  run,
	Requires: []*analysis.Analyzer{
		inspect.Analyzer,
		buildssa.Analyzer,
		commentmap.Analyzer,
	},
}

Analyzer is ...

Functions

This section is empty.

Types

This section is empty.

Directories

Path Synopsis
cmd

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL