~/bend-docscommunity

src/rules/laws/unsafe.bend checks

raw source on the hub · import 0x013e0f9a479bbebad5ed196725eede95/src/rules/laws/unsafe.bend as Unsafe

rule unsafe (project-wide): an @unsafe def that a LAWS.bend or PROOF.bend reaches by relative imports, over the files bolt read. The checker skips its termination check, prints "All terms check, but N defs rely on unsafe or foreign code:" (2.0.16: "with N unsafe annotation(s).") and exits 0, so a gate that only reads the exit status goes green on a proof that is not sound (a def that never returns proves anything). Recurse on a shrinking argument, or on a fuel, and drop the @unsafe; or keep the def out of what the laws import. An @unsafe def no law file reaches is not this rule's business. The rule reads each file's digest (src/rules/digest.bend), and takes every closure over one import graph.

4 imports
import Base
import ../../finding.bend as F
import ../digest.bend as Digest
import ../imports.bend as Imports

Types

type Reach source · line 17 · raw

Data

a law file and what it reaches

Definitions

def reaches source · line 21 · raw

@ds:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/rules/digest.Digest> -> @+es:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/rules/imports.Edge> -> @+read:List<&2, String> -> @+fuel:Nat -> List<&2, Reach>

every LAWS.bend and PROOF.bend with its closure over the graph

def reacher source · line 35 · raw

@rs:List<&2, Reach> -> @+pp:String -> Maybe<&2, String>

the first law file that reaches the path

def report source · line 44 · raw

@us:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/rules/digest.Unsafe> -> @+origin:String -> @+path:String -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

each unsafe def as a finding, reached from the law file

def found source · line 53 · raw

@mm:Maybe<&2, String> -> @us:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/rules/digest.Unsafe> -> @path:String -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

the unsafe defs of a file, when a law file reaches it

def check.go source · line 60 · raw

@ds:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/rules/digest.Digest> -> @+rs:List<&2, Reach> -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

def check source · line 68 · raw

@+ds:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/rules/digest.Digest> -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

the rule, over every file the linter read