Error Reference¶

Errors are organized by the pipeline stage that produces them.

Extraction Errors¶

These occur when scanning the source file for annotated functions.

Error	Cause and Fix
`annotation block at line N must be followed immediately by sub`	There is a blank line or non-comment line between the annotation comments and the `sub` keyword. Remove the blank line.
`invalid sub declaration at line N`	The `sub` line does not match the expected format `sub name {`. Check for typos or missing braces.
`function NAME has unmatched braces`	The closing `}` for the function body is missing or mismatched.

These occur when parsing the # sig:, # pre:, # post: lines.

Error	Cause and Fix
`missing # sig: annotation`	Every annotated function must have a `# sig:` line declaring its type signature.
`missing # post: annotation`	Every annotated function must have a `# post:` (or `# pos:`) line declaring its postcondition.
`duplicate directive: sig`	The annotation block has more than one `# sig:` line. Only one is allowed.
`duplicate directive: post`	The annotation block has more than one `# post:` line.
`unsupported type: Foo`	The type `Foo` is not recognized. Supported types: `I64`, `Str`, `Array<I64>`, `Array<Str>`, `Hash<Str, I64>`, `Hash<Str, Str>`.
`parameter count mismatch: sig declares N but body has M`	The number of types in the `# sig:` line does not match the number of parameters in `my (...) = @_;`.
`references unknown variable $x`	The precondition or postcondition uses a variable that is not a function parameter and is not `$result`.
`invalid expression in annotation`	The expression in `# pre:` or `# post:` has a syntax error.

These occur when parsing the function body.

Error	Cause and Fix
`invalid syntax at line:column`	The function body contains Perl syntax that is not part of the supported subset. See Language Reference for what is supported.

These occur during static type analysis of the function body.

Error	Cause and Fix
`undeclared variable $x`	The variable `$x` is used without a prior `my $x` declaration.
`uninitialized variable $x`	The variable `$x` was declared with `my $x;` but read before being assigned a value. Initialize it: `my $x = 0;`.
`type mismatch`	An operator received the wrong type. For example, using `+` on strings or `eq` on integers.
`array index must be I64`	An array access `$arr[$i]` used a non-integer index.
`unsafe substring start`	The `substr` start position could be negative or out of bounds. Add a precondition to constrain it.

These occur during path exploration and verification.

Error	Cause and Fix
`recursive call graph detected`	The function calls itself directly or through a chain of calls. Recursion is not supported.
`exceeded maximum number of symbolic paths (1024)`	The function has too many branches. Reduce branching or increase `--max_paths`. See Configuration.
`exceeded loop unroll bound on a feasible path`	A loop iterates more than `max_loop_unroll` times on a feasible input. Tighten the precondition to bound iterations or increase `--max_loop_unroll`.
`can reach a die statement on a feasible path`	A `die` (or `croak`/`confess`) statement is reachable given the precondition. Either the precondition is too weak or the die is intentional and should be guarded more tightly.
`no valid execution paths`	Every execution path hits an arithmetic error (like division by zero). The function has no valid behavior to verify.
`extern contract evaluation failed`	An extern function’s precondition or postcondition expression could not be evaluated (e.g., it references an undefined variable or has a type error). Check that the extern annotations are correct and that all referenced variables are in scope.
`assertion failed on a feasible path`	An `assert` statement evaluates to false on at least one feasible execution path. Either the assertion is wrong or the precondition needs tightening.

These occur during Z3 solver interaction.

Error	Cause and Fix
`solver returned unknown`	The Z3 solver could not determine satisfiability within the timeout. Try increasing `--solver_timeout_ms` or simplifying the function.