Proof Portal

jsonparser

ProbeLabs23 findings · 123 requirements

Showing the current git stateNo audit has been synced for this project yet — verification results (proof status, coverage, solver signals) appear once an audit is published.proof-demod79405e

Requirements Explorer

Scan, sort, group and trace every requirement — from stakeholder needs down to code, tests and docs.

Requirements

123

STK 7 · SYS 116 · SW 0 · INT 0

With implementation

73%

90 of 123

With tests

100%

123 of 123

With docs

100%

123 of 123

Coverage gaps

policy-required missing traces

Level

Group by

Expand to

Showing 123 of 123

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