Proof Portal

Sign in
Projects

jsonparser

ProbeLabs23 findings · 123 requirements

The fastest JSON parser for Go — formally verified with ReqProof (real library, master).

Map
Component

parser

123 requirements allocated to this component across category functional.

Open in graphDiscuss
123 requirements · 90/123 implemented · 123/123 tested.

Contracts

Interface contracts this component is a producer or consumer of.

No interface contracts

This component neither produces nor consumes a declared interface contract.

Responsibilities

the requirements this component owns, by intent — filter for coverage gaps
Requirement (by intent)CoverageGap
Library users shall retrieve values from JSON byte payloads…STKSTK-REQ-001ITD
Library users shall retrieve string values with JSON…STKSTK-REQ-002ITD
Library users shall extract known numeric and boolean JSON…STKSTK-REQ-003ITD
Library users shall traverse arrays and objects and extract…STKSTK-REQ-004ITD
Library users shall update or delete addressed JSON values…STKSTK-REQ-005ITD
Library users shall retrieve addressed JSON values as…STKSTK-REQ-006ITD
Library users shall parse raw JSON scalar tokens into Go…STKSTK-REQ-007ITD
When the JSON input is well formed, a key path is provided,…SYSSYS-REQ-001ITD
When GetString addresses a JSON string value whose raw…SYSSYS-REQ-002ITD
When GetInt addresses a JSON number token that is parseable…SYSSYS-REQ-003ITD
When GetFloat addresses a JSON number token that is…SYSSYS-REQ-004ITD
When GetBoolean addresses a well-formed JSON boolean token,…SYSSYS-REQ-005ITD
When ArrayEach addresses a well-formed non-empty JSON…SYSSYS-REQ-006ITD
When ObjectEach addresses a well-formed non-empty JSON…SYSSYS-REQ-007ITD
When EachKey is called with one or more requested key…SYSSYS-REQ-008ITD
When Set is called with a provided path, the parser shall…SYSSYS-REQ-009ITD
When Delete is called without a path, the parser shall…SYSSYS-REQ-010ITD
When GetUnsafeString addresses a JSON string value, the…SYSSYS-REQ-011ITD
When ParseBoolean receives a valid raw boolean token, the…SYSSYS-REQ-012ITD
When ParseFloat receives a well-formed floating-point…SYSSYS-REQ-013ITD
When ParseString receives a well-formed raw JSON string…SYSSYS-REQ-014ITD
When ParseInt receives a syntactically well-formed integer…SYSSYS-REQ-015ITD
When the JSON input is well formed, a key path is provided,…SYSSYS-REQ-016ITD
When the JSON input is incomplete or truncated before…SYSSYS-REQ-017ITD
When the JSON input is well formed and no key path is…SYSSYS-REQ-018ITD
When the input is empty and a key path is provided, the…SYSSYS-REQ-019ITD
When the current path segment is an object key and it is…SYSSYS-REQ-020ITD
When the current path segment is a valid in-bounds array…SYSSYS-REQ-021ITD
When the current path segment is intended as an array index…SYSSYS-REQ-022ITD
When the current path segment is a valid array index but…SYSSYS-REQ-023ITD
When a JSON object member key is escaped in the payload and…SYSSYS-REQ-024ITD
When the addressed value is a JSON string, Get shall return…SYSSYS-REQ-025ITD
When the input is malformed outside the addressed token…SYSSYS-REQ-026ITD
When the addressed token cannot be classified as string,…SYSSYS-REQ-027ITD
When ArrayEach addresses a well-formed empty JSON array,…SYSSYS-REQ-028ITD
When ArrayEach receives malformed or otherwise unusable…SYSSYS-REQ-029ITD
When ObjectEach addresses a well-formed empty JSON object,…SYSSYS-REQ-030ITD
When ObjectEach receives malformed or otherwise unusable…SYSSYS-REQ-031ITD
When ObjectEach addresses a well-formed object and the…SYSSYS-REQ-032ITD
When Delete is called with a provided path and the…SYSSYS-REQ-033ITD
When Delete is called with a provided path, the addressed…SYSSYS-REQ-034ITD
When Delete is called with a provided path but the input is…SYSSYS-REQ-035ITD
When ParseBoolean receives an invalid boolean token, the…SYSSYS-REQ-036ITD
When ParseFloat receives a malformed numeric token, the…SYSSYS-REQ-037ITD
When ParseString receives a malformed encoded string…SYSSYS-REQ-038ITD
When ParseInt receives an integer token whose magnitude…SYSSYS-REQ-039ITD
When ParseInt receives a non-integer or otherwise malformed…SYSSYS-REQ-040ITD
When the JSON input is truncated at a value boundary (eSYSSYS-REQ-041ITD
When the JSON input is truncated in the middle of a…SYSSYS-REQ-042ITD
When the JSON input is truncated in the middle of a key…SYSSYS-REQ-043ITD
When internal helper tokenEnd returns len(data) as a…SYSSYS-REQ-044ITD
When internal helper stringEnd returns -1 indicating no…SYSSYS-REQ-045ITD
When internal helper blockEnd returns -1 indicating no…SYSSYS-REQ-046ITD
When the current path segment is a negative array index (eSYSSYS-REQ-047ITD
When Delete is called on input that is truncated at a value…SYSSYS-REQ-048ITD
When Delete calls internalGet and internalGet returns an…SYSSYS-REQ-049ITD
When Delete is called with an array-element path on input…SYSSYS-REQ-050ITD
When Set is called on truncated JSON input where the path…SYSSYS-REQ-051ITD
When ArrayEach iterates a well-formed array and the Get…SYSSYS-REQ-052ITD
When ArrayEach encounters an array element that is…SYSSYS-REQ-053ITD
When ObjectEach encounters an object entry that is…SYSSYS-REQ-054ITD
When ArrayEach encounters a malformed delimiter between…SYSSYS-REQ-055ITD
When Delete is called on input that is truncated…SYSSYS-REQ-056ITD
When ParseBoolean receives a partial boolean literal (eSYSSYS-REQ-057ITD
When ParseInt receives integer tokens at the exact int64…SYSSYS-REQ-058ITD
When ParseInt receives an integer token that is exactly one…SYSSYS-REQ-059ITD
When ParseString receives a string literal containing a…SYSSYS-REQ-060ITD
When ParseString encounters a UTF-16 high surrogate escape…SYSSYS-REQ-061ITD
When ParseString encounters a UTF-16 high surrogate escape…SYSSYS-REQ-062ITD
When ParseString encounters a string literal ending with a…SYSSYS-REQ-063ITD
When ParseInt receives an empty byte slice, the parser…SYSSYS-REQ-064ITD
When ParseFloat receives an empty byte slice, the parser…SYSSYS-REQ-065ITD
When ParseBoolean receives an empty byte slice, the parser…SYSSYS-REQ-066ITD
When ParseString receives an empty byte slice, the parser…SYSSYS-REQ-067ITD
When Set is called with a path that resolves to a location…SYSSYS-REQ-068ITD
When Set is called with a multi-level path where…SYSSYS-REQ-069ITD
When Set is called without any key path, the parser shall…SYSSYS-REQ-070ITD
When GetString is called on malformed input where the…SYSSYS-REQ-071ITD
When GetString addresses a JSON string value containing a…SYSSYS-REQ-072ITD
When GetString addresses a value that is not a JSON string…SYSSYS-REQ-073ITD
When GetString is called on empty input, the parser shall…SYSSYS-REQ-074ITD
When GetInt is called on malformed input where the…SYSSYS-REQ-075ITD
When GetInt addresses a JSON number token whose magnitude…SYSSYS-REQ-076ITD
When GetInt addresses a value that is not a JSON number (eSYSSYS-REQ-077ITD
When GetInt is called on empty input, the parser shall…SYSSYS-REQ-078ITD
When GetBoolean addresses a value that appears to be a…SYSSYS-REQ-079ITD
When GetUnsafeString is called on malformed input where the…SYSSYS-REQ-080ITD
When GetUnsafeString is called on empty input, the parser…SYSSYS-REQ-081ITD
When GetUnsafeString is called on input truncated at a…SYSSYS-REQ-082ITD
When ArrayEach is called on input truncated at a value…SYSSYS-REQ-083ITD
When ObjectEach is called on input truncated mid-structure…SYSSYS-REQ-084ITD
When EachKey encounters a tokenEnd sentinel value…SYSSYS-REQ-085ITD
When Get is called twice with identical JSON input and…SYSSYS-REQ-086ITD
When Get is called on a JSON byte slice, the parser shall…SYSSYS-REQ-087ITD
When Get is called with a nil byte slice as input, the…SYSSYS-REQ-088ITD
When Get is called on JSON input with deeply nested…SYSSYS-REQ-089ITD
When GetString is called twice with identical JSON input…SYSSYS-REQ-090ITD
When GetString is called with a nil byte slice as input,…SYSSYS-REQ-091ITD
When GetString is called on a JSON string containing…SYSSYS-REQ-092ITD
When GetString is called on JSON containing Unicode edge…SYSSYS-REQ-093ITD
When GetInt, GetFloat, or GetBoolean is called twice with…SYSSYS-REQ-094ITD
When GetInt, GetFloat, or GetBoolean is called with a nil…SYSSYS-REQ-095ITD
When GetInt is called on JSON containing numeric edge cases…SYSSYS-REQ-096ITD
When ArrayEach, ObjectEach, or EachKey is called twice with…SYSSYS-REQ-097ITD
When ArrayEach, ObjectEach, or EachKey is called with a nil…SYSSYS-REQ-098ITD
When ArrayEach or ObjectEach is called on JSON with deeply…SYSSYS-REQ-099ITD
When Set is called twice on the same input with the same…SYSSYS-REQ-100ITD
When Set or Delete is called with a nil byte slice as…SYSSYS-REQ-101ITD
When Set or Delete is called with key paths containing…SYSSYS-REQ-102ITD
When GetUnsafeString is called twice with identical JSON…SYSSYS-REQ-103ITD
When GetUnsafeString is called with a nil byte slice as…SYSSYS-REQ-104ITD
When GetUnsafeString is called on JSON containing values…SYSSYS-REQ-105ITD
When ParseBoolean, ParseInt, ParseFloat, or ParseString is…SYSSYS-REQ-106ITD
When ParseBoolean, ParseInt, ParseFloat, or ParseString is…SYSSYS-REQ-107ITD
When ParseString is called on a byte slice containing…SYSSYS-REQ-108ITD
When ParseInt is called on edge-case numeric tokens such as…SYSSYS-REQ-109ITD
When Set targets an array-index path component [N] where N…SYSSYS-REQ-110ITD
When any key path component is the empty string, the parser…SYSSYS-REQ-111ITD
GetArrayLen returns the number of elements in the addressed…SYSSYS-REQ-112ITD
EachKeyWildcard, ArrayEachWildcard, and SetWildcard accept…SYSSYS-REQ-113ITD
ParsePath converts a JSONPath-style string (root $SYSSYS-REQ-114ITD
When a Config with AllowSingleQuotes=true is provided, the…SYSSYS-REQ-115ITD
A ReaderParser shall provide path-based access to JSON data…SYSSYS-REQ-116ITD

Findings 0 open · 5 resolved

Open (0)

known issues, coverage gaps and checks that still need attention

No open findings — everything here is resolved or historical.

Resolved / historical (5)

fixed defects, accepted risks and closed known issues — kept for the record

Attached code & tests

traced files across this component’s requirements, deduplicated by path
Code(8 files)
  • aliases.goaliases.go
  • append.goappend.go
  • config.goconfig.go
  • escape.goescape.go
  • fuzz.gofuzz.go
  • parser.goparser.go
  • reader_parser.goreader_parser.go
  • wildcard.gowildcard.go
Tests(42 files)
  • aliases_test.goaliases_test.go
  • append_test.goappend_test.go
  • array_each_err_test.goarray_each_err_test.go
  • benchmark_delete_test.gobenchmark/benchmark_delete_test.go
  • benchmark_large_payload_test.gobenchmark/benchmark_large_payload_test.go
  • benchmark_medium_payload_test.gobenchmark/benchmark_medium_payload_test.go
  • benchmark_set_test.gobenchmark/benchmark_set_test.go
  • benchmark_small_payload_test.gobenchmark/benchmark_small_payload_test.go
  • bytes_test.gobytes_test.go
  • bytes_unsafe_test.gobytes_unsafe_test.go
  • config_test.goconfig_test.go
  • coverage_closure_test.gocoverage_closure_test.go
  • dead_code_audit_oob_test.godead_code_audit_oob_test.go
  • dead_code_audit_test.godead_code_audit_test.go
  • deep_spec_test.godeep_spec_test.go
  • empty_key_path_test.goempty_key_path_test.go
  • encoding_json_fuzz_test.goencoding_json_fuzz_test.go
  • encoding_json_regression_test.gobenchmark/encoding_json_regression_test.go
  • escape_test.goescape_test.go
  • fuzz_native_test.gofuzz_native_test.go
  • issues_56_107_229_test.goissues_56_107_229_test.go
  • json_fuzz_test.gojson_fuzz_test.go
  • len_uint_test.golen_uint_test.go
  • mcdc_code_supplement_test.gomcdc_code_supplement_test.go
  • mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
  • mcdc_supplement_test.gomcdc_supplement_test.go
  • obligation_evidence_test.goobligation_evidence_test.go
  • obligation_property_test.goobligation_property_test.go
  • optimization_equiv_test.gooptimization_equiv_test.go
  • parser_error_test.goparser_error_test.go
  • parser_test.goparser_test.go
  • path_compiler_test.gopath_compiler_test.go
  • path_compiler.gopath_compiler.go
  • path_fuzz_test.gopath_fuzz_test.go
  • property_test.goproperty_test.go
  • reader_parser_test.goreader_parser_test.go
  • reference_oracle_test.goreference_oracle_test.go
  • set_spec_test.goset_spec_test.go
  • sys_req_110_111_witness_test.gosys_req_110_111_witness_test.go
  • v131_regression_test.gov131_regression_test.go
  • v150_mcdc_witness_test.gov150_mcdc_witness_test.go
  • wildcard_test.gowildcard_test.go

How this component connects

Open in graph
Mapping this component’s neighbourhood…

Discussions

Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.

Sign in to discuss this with the proof team.Sign in