From 4c4f597943c9eeb93fb7ef66b30d66ce92dddcd8 Mon Sep 17 00:00:00 2001 From: czjaso Date: Tue, 2 Dec 2025 11:19:44 -0800 Subject: [PATCH 1/9] Fix array parsing to reject missing commas between elements --- source/core_json.c | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/source/core_json.c b/source/core_json.c index d8694f0c..7cb21ad4 100644 --- a/source/core_json.c +++ b/source/core_json.c @@ -934,11 +934,12 @@ static bool skipSpaceAndComma( const char * buf, * * @note Stops advance if a value is an object or array. */ -static void skipArrayScalars( const char * buf, +static bool skipArrayScalars( const char * buf, size_t * start, size_t max ) { size_t i = 0U; + bool ret = true; coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); @@ -953,11 +954,18 @@ static void skipArrayScalars( const char * buf, if( skipSpaceAndComma( buf, &i, max ) != true ) { + /* After parsing a scalar, we must either have a comma (followed by more content) + * or be at a closing bracket. If neither, the array is malformed. */ + if( ( i >= max ) || !isSquareClose_( buf[ i ] ) ) + { + ret = false; + } break; } } *start = i; + return ret; } /** @@ -1071,7 +1079,7 @@ static bool skipScalars( const char * buf, { if( !isSquareClose_( buf[ i ] ) ) { - skipArrayScalars( buf, start, max ); + ret = skipArrayScalars( buf, start, max ); } } else From 10fd66c1e27b083528a8e6ca30fa21d4fda1f485 Mon Sep 17 00:00:00 2001 From: czjaso Date: Tue, 2 Dec 2025 11:42:09 -0800 Subject: [PATCH 2/9] Fix collection parsing to reject missing commas between elements --- source/core_json.c | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/source/core_json.c b/source/core_json.c index 7cb21ad4..5c6ca62d 100644 --- a/source/core_json.c +++ b/source/core_json.c @@ -960,6 +960,7 @@ static bool skipArrayScalars( const char * buf, { ret = false; } + break; } } @@ -1159,14 +1160,22 @@ static JSONStatus_t skipCollection( const char * buf, { depth--; - if( ( skipSpaceAndComma( buf, &i, max ) == true ) && - isOpenBracket_( stack[ depth ] ) ) + if( skipSpaceAndComma( buf, &i, max ) == true ) { if( skipScalars( buf, &i, max, stack[ depth ] ) != true ) { ret = JSONIllegalDocument; } } + else + { + /* After closing a nested collection, if there is no comma found when calling + * skipSpaceAndComma, then we must be at the end of the parent collection. */ + if( ( i < max ) && !isMatchingBracket_( stack[ depth ], buf[ i ] ) ) + { + ret = JSONIllegalDocument; + } + } break; } From eebe8bc5c3b20a93607880870d34396df8526810 Mon Sep 17 00:00:00 2001 From: czjaso Date: Tue, 2 Dec 2025 12:22:09 -0800 Subject: [PATCH 3/9] Fix escape sequence parsing to reject invalid control character escapes --- source/core_json.c | 8 -------- 1 file changed, 8 deletions(-) diff --git a/source/core_json.c b/source/core_json.c index 5c6ca62d..c6776c39 100644 --- a/source/core_json.c +++ b/source/core_json.c @@ -477,14 +477,6 @@ static bool skipEscape( const char * buf, break; default: - - /* a control character: (NUL,SPACE) */ - if( iscntrl_( c ) ) - { - i += 2U; - ret = true; - } - break; } } From e5c12ff28b2f1799f646b8c8ec6291301bc290c0 Mon Sep 17 00:00:00 2001 From: czjaso Date: Tue, 2 Dec 2025 12:54:22 -0800 Subject: [PATCH 4/9] Allow \u0000 escape sequences in JSON strings --- source/core_json.c | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/source/core_json.c b/source/core_json.c index c6776c39..e9e3cf5b 100644 --- a/source/core_json.c +++ b/source/core_json.c @@ -321,8 +321,6 @@ static uint8_t hexToInt( char c ) * * @return true if a valid escape sequence was present; * false otherwise. - * - * @note For the sake of security, \u0000 is disallowed. */ static bool skipOneHexEscape( const char * buf, size_t * start, @@ -358,7 +356,7 @@ static bool skipOneHexEscape( const char * buf, } } - if( ( i == end ) && ( value > 0U ) ) + if( i == end ) { ret = true; *outValue = value; @@ -382,8 +380,6 @@ static bool skipOneHexEscape( const char * buf, * * @return true if a valid escape sequence was present; * false otherwise. - * - * @note For the sake of security, \u0000 is disallowed. */ #define isHighSurrogate( x ) ( ( ( x ) >= 0xD800U ) && ( ( x ) <= 0xDBFFU ) ) #define isLowSurrogate( x ) ( ( ( x ) >= 0xDC00U ) && ( ( x ) <= 0xDFFFU ) ) @@ -437,8 +433,6 @@ static bool skipHexEscape( const char * buf, * * @return true if a valid escape sequence was present; * false otherwise. - * - * @note For the sake of security, \NUL is disallowed. */ static bool skipEscape( const char * buf, size_t * start, @@ -457,9 +451,6 @@ static bool skipEscape( const char * buf, switch( c ) { - case '\0': - break; - case 'u': ret = skipHexEscape( buf, &i, max ); break; From 684af6de3e9c947eb07a3dfeba4ff30d41a5a2ca Mon Sep 17 00:00:00 2001 From: czjaso Date: Tue, 2 Dec 2025 16:18:49 -0800 Subject: [PATCH 5/9] Fix unit tests and skipOneHexEscape logic for overflows. --- source/core_json.c | 7 +++---- test/unit-test/core_json_utest.c | 21 ++------------------- 2 files changed, 5 insertions(+), 23 deletions(-) diff --git a/source/core_json.c b/source/core_json.c index e9e3cf5b..a01c3931 100644 --- a/source/core_json.c +++ b/source/core_json.c @@ -331,17 +331,16 @@ static bool skipOneHexEscape( const char * buf, size_t i = 0U, end = 0U; uint16_t value = 0U; - coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); - coreJSON_ASSERT( outValue != NULL ); + coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) && ( outValue != NULL ) ); i = *start; #define HEX_ESCAPE_LENGTH ( 6U ) /* e.g., \u1234 */ /* MISRA Ref 14.3.1 [Configuration dependent invariant] */ /* More details at: https://github.com/FreeRTOS/coreJSON/blob/main/MISRA.md#rule-143 */ /* coverity[misra_c_2012_rule_14_3_violation] */ - end = ( i <= ( SIZE_MAX - HEX_ESCAPE_LENGTH ) ) ? ( i + HEX_ESCAPE_LENGTH ) : SIZE_MAX; + end = i + HEX_ESCAPE_LENGTH; - if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) ) + if( ( end > i ) && ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) ) { for( i += 2U; i < end; i++ ) { diff --git a/test/unit-test/core_json_utest.c b/test/unit-test/core_json_utest.c index f3c29866..8759dde1 100644 --- a/test/unit-test/core_json_utest.c +++ b/test/unit-test/core_json_utest.c @@ -103,7 +103,7 @@ "\"foo\":\"abc\",\"" FIRST_QUERY_KEY "\":" FIRST_QUERY_KEY_ANSWER "}" #define JSON_DOC_VARIED_SCALARS_LENGTH ( sizeof( JSON_DOC_VARIED_SCALARS ) - 1 ) -#define MULTIPLE_VALID_ESCAPES "\\\\ \\\" \\/ \\b \\f \\n \\r \\t \\\x12" +#define MULTIPLE_VALID_ESCAPES "\\\\ \\\" \\/ \\b \\f \\n \\r \\t \\u0001" #define MULTIPLE_VALID_ESCAPES_LENGTH ( sizeof( MULTIPLE_VALID_ESCAPES ) - 1 ) #define JSON_DOC_QUERY_KEY_NOT_FOUND "{\"hello\": \"world\"}" @@ -354,12 +354,6 @@ "\":{\"" SECOND_QUERY_KEY "\" : \"\\uD83D\\uD83D\"}}" #define UNICODE_BOTH_SURROGATES_HIGH_LENGTH ( sizeof( UNICODE_BOTH_SURROGATES_HIGH ) - 1 ) -/* For security, \u0000 is disallowed. */ -#define UNICODE_ESCAPE_SEQUENCE_ZERO_CP \ - "{\"foo\":\"abc\",\"" FIRST_QUERY_KEY \ - "\":{\"" SECOND_QUERY_KEY "\" : \"\\u0000\"}}" -#define UNICODE_ESCAPE_SEQUENCE_ZERO_CP_LENGTH ( sizeof( UNICODE_ESCAPE_SEQUENCE_ZERO_CP ) - 1 ) - /* /NUL escape is disallowed. */ #define NUL_ESCAPE \ "{\"foo\":\"abc\",\"" FIRST_QUERY_KEY \ @@ -580,6 +574,7 @@ void test_JSON_Validate_Legal_Documents( void ) jsonStatus = JSON_Validate( JSON_DOC_MULTIPLE_VALID_ESCAPES, JSON_DOC_MULTIPLE_VALID_ESCAPES_LENGTH ); + TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus ); jsonStatus = JSON_Validate( JSON_DOC_LEGAL_UTF8_BYTE_SEQUENCES, @@ -802,10 +797,6 @@ void test_JSON_Validate_Illegal_Documents( void ) UNICODE_BOTH_SURROGATES_HIGH_LENGTH ); TEST_ASSERT_EQUAL( JSONIllegalDocument, jsonStatus ); - jsonStatus = JSON_Validate( UNICODE_ESCAPE_SEQUENCE_ZERO_CP, - UNICODE_ESCAPE_SEQUENCE_ZERO_CP_LENGTH ); - TEST_ASSERT_EQUAL( JSONIllegalDocument, jsonStatus ); - jsonStatus = JSON_Validate( UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE, UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE_LENGTH ); TEST_ASSERT_EQUAL( JSONIllegalDocument, jsonStatus ); @@ -1506,14 +1497,6 @@ void test_JSON_Search_Illegal_Documents( void ) &outValueLength ); TEST_ASSERT_EQUAL( JSONNotFound, jsonStatus ); - jsonStatus = JSON_Search( UNICODE_ESCAPE_SEQUENCE_ZERO_CP, - UNICODE_ESCAPE_SEQUENCE_ZERO_CP_LENGTH, - COMPLETE_QUERY_KEY, - COMPLETE_QUERY_KEY_LENGTH, - &outValue, - &outValueLength ); - TEST_ASSERT_EQUAL( JSONNotFound, jsonStatus ); - jsonStatus = JSON_Search( UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE, UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE_LENGTH, COMPLETE_QUERY_KEY, From 92ab41f6ed12edb5dec36fb887ac8fdc90c48de8 Mon Sep 17 00:00:00 2001 From: czjaso Date: Tue, 2 Dec 2025 16:51:07 -0800 Subject: [PATCH 6/9] Fix coverage. --- tools/unity/coverage.cmake | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/tools/unity/coverage.cmake b/tools/unity/coverage.cmake index 3cdbd316..165567dc 100644 --- a/tools/unity/coverage.cmake +++ b/tools/unity/coverage.cmake @@ -14,7 +14,8 @@ execute_process( COMMAND lcov --directory ${CMAKE_BINARY_DIR} --base-directory ${CMAKE_BINARY_DIR} --initial --capture - --rc lcov_branch_coverage=1 + --ignore-errors source + --rc branch_coverage=1 --rc genhtml_branch_coverage=1 --output-file=${CMAKE_BINARY_DIR}/base_coverage.info ) @@ -45,7 +46,8 @@ execute_process(COMMAND ruby # capture data after running the tests execute_process( COMMAND lcov --capture - --rc lcov_branch_coverage=1 + --ignore-errors source + --rc branch_coverage=1 --rc genhtml_branch_coverage=1 --base-directory ${CMAKE_BINARY_DIR} --directory ${CMAKE_BINARY_DIR} @@ -60,10 +62,10 @@ execute_process( --add-tracefile ${CMAKE_BINARY_DIR}/second_coverage.info --output-file ${CMAKE_BINARY_DIR}/coverage.info --no-external - --rc lcov_branch_coverage=1 + --rc branch_coverage=1 ) execute_process( - COMMAND genhtml --rc lcov_branch_coverage=1 + COMMAND genhtml --rc branch_coverage=1 --branch-coverage --output-directory ${CMAKE_BINARY_DIR}/coverage ${CMAKE_BINARY_DIR}/coverage.info From 94ed2de38020f69e87f7a417c602d8dc264beb84 Mon Sep 17 00:00:00 2001 From: czjaso Date: Wed, 3 Dec 2025 11:49:22 -0800 Subject: [PATCH 7/9] Fix coverage workflow. --- .github/workflows/ci.yml | 2 +- tools/unity/coverage.cmake | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4881aa00..381b3e50 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -29,7 +29,7 @@ jobs: run: | make -C build/ coverage declare -a EXCLUDE=("\*test\*" "\*CMakeCCompilerId\*" "\*mocks\*" "\*source\*") - echo ${EXCLUDE[@]} | xargs lcov --rc lcov_branch_coverage=1 -r build/coverage.info -o build/coverage.info + echo ${EXCLUDE[@]} | xargs lcov --rc lcov_branch_coverage=1 --ignore-errors unused -r build/coverage.info -o build/coverage.info lcov --rc lcov_branch_coverage=1 --list build/coverage.info - name: Check Coverage uses: FreeRTOS/CI-CD-Github-Actions/coverage-cop@main diff --git a/tools/unity/coverage.cmake b/tools/unity/coverage.cmake index 165567dc..8e80bed9 100644 --- a/tools/unity/coverage.cmake +++ b/tools/unity/coverage.cmake @@ -6,6 +6,7 @@ execute_process( COMMAND lcov --directory ${CMAKE_BINARY_DIR} --base-directory ${CMAKE_BINARY_DIR} --zerocounters + --rc lcov_branch_coverage=1 COMMAND mkdir -p ${CMAKE_BINARY_DIR}/coverage ) @@ -15,7 +16,7 @@ execute_process( COMMAND lcov --directory ${CMAKE_BINARY_DIR} --initial --capture --ignore-errors source - --rc branch_coverage=1 + --rc lcov_branch_coverage=1 --rc genhtml_branch_coverage=1 --output-file=${CMAKE_BINARY_DIR}/base_coverage.info ) @@ -47,7 +48,7 @@ execute_process(COMMAND ruby execute_process( COMMAND lcov --capture --ignore-errors source - --rc branch_coverage=1 + --rc lcov_branch_coverage=1 --rc genhtml_branch_coverage=1 --base-directory ${CMAKE_BINARY_DIR} --directory ${CMAKE_BINARY_DIR} @@ -62,10 +63,10 @@ execute_process( --add-tracefile ${CMAKE_BINARY_DIR}/second_coverage.info --output-file ${CMAKE_BINARY_DIR}/coverage.info --no-external - --rc branch_coverage=1 + --rc lcov_branch_coverage=1 ) execute_process( - COMMAND genhtml --rc branch_coverage=1 + COMMAND genhtml --rc lcov_branch_coverage=1 --branch-coverage --output-directory ${CMAKE_BINARY_DIR}/coverage ${CMAKE_BINARY_DIR}/coverage.info From 8c5a83009455b9e09cf456947b6decbe8f91b9ba Mon Sep 17 00:00:00 2001 From: czjaso Date: Wed, 3 Dec 2025 11:58:59 -0800 Subject: [PATCH 8/9] Increase complexity threshold, set formatting to check to run on ubuntu-latest. --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 381b3e50..abad151c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -44,7 +44,7 @@ jobs: uses: FreeRTOS/CI-CD-Github-Actions/complexity@main with: path: ./ - horrid_threshold: 12 + horrid_threshold: 14 doxygen: runs-on: ubuntu-latest @@ -66,7 +66,7 @@ jobs: path: ./ formatting: - runs-on: ubuntu-20.04 + runs-on: ubuntu-latest steps: - uses: actions/checkout@v3 - name: Check formatting From ef1f39c83da3de5f2c4c4687cdb590c99da1e9b8 Mon Sep 17 00:00:00 2001 From: czjaso Date: Thu, 4 Dec 2025 16:57:54 -0800 Subject: [PATCH 9/9] Update CBMC proofs. --- loop_invariants.patch | 66 ++++++++++++++----------- test/cbmc/proofs/JSON_Validate/Makefile | 1 + 2 files changed, 38 insertions(+), 29 deletions(-) diff --git a/loop_invariants.patch b/loop_invariants.patch index 581f1dfd..88ad7b6d 100644 --- a/loop_invariants.patch +++ b/loop_invariants.patch @@ -1,11 +1,11 @@ diff --git a/source/core_json.c b/source/core_json.c -index d8694f0..761c44b 100644 +index a01c393..ad48f28 100644 --- a/source/core_json.c +++ b/source/core_json.c @@ -63,6 +63,21 @@ typedef union #define isCurlyOpen_( x ) ( ( x ) == '{' ) #define isCurlyClose_( x ) ( ( x ) == '}' ) - + +/** + * Renaming all loop-contract clauses from CBMC for readability. + * For more information about loop contracts in CBMC, see @@ -26,7 +26,7 @@ index d8694f0..761c44b 100644 * @@ -79,6 +94,9 @@ static void skipSpace( const char * buf, coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) ); - + for( i = *start; i < max; i++ ) + assigns( i ) + loopInvariant( *start <= i && i <= max ) @@ -36,7 +36,7 @@ index d8694f0..761c44b 100644 { @@ -103,6 +121,13 @@ static size_t countHighBits( uint8_t c ) size_t i = 0; - + while( ( n & 0x80U ) != 0U ) + assigns( i, n ) + loopInvariant ( @@ -61,9 +61,9 @@ index d8694f0..761c44b 100644 + decreases( j ) { i++; - -@@ -346,6 +378,12 @@ static bool skipOneHexEscape( const char * buf, - if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) ) + +@@ -343,6 +375,12 @@ static bool skipOneHexEscape( const char * buf, + if( ( end > i ) && ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) ) { for( i += 2U; i < end; i++ ) + assigns( value, i ) @@ -74,10 +74,10 @@ index d8694f0..761c44b 100644 + decreases( end - i ) { uint8_t n = hexToInt( buf[ i ] ); - -@@ -523,6 +561,9 @@ static bool skipString( const char * buf, + +@@ -505,6 +543,9 @@ static bool skipString( const char * buf, i++; - + while( i < max ) + assigns( i ) + loopInvariant( *start + 1U <= i && i <= max ) @@ -85,9 +85,9 @@ index d8694f0..761c44b 100644 { if( buf[ i ] == '"' ) { -@@ -581,6 +622,9 @@ static bool strnEq( const char * a, +@@ -563,6 +604,9 @@ static bool strnEq( const char * a, coreJSON_ASSERT( ( a != NULL ) && ( b != NULL ) ); - + for( i = 0; i < n; i++ ) + assigns( i ) + loopInvariant( i <= n ) @@ -95,9 +95,9 @@ index d8694f0..761c44b 100644 { if( a[ i ] != b[ i ] ) { -@@ -696,6 +740,9 @@ static bool skipDigits( const char * buf, +@@ -678,6 +722,9 @@ static bool skipDigits( const char * buf, saveStart = *start; - + for( i = *start; i < max; i++ ) + assigns( value, i ) + loopInvariant( *start <= i && i <= max ) @@ -105,9 +105,9 @@ index d8694f0..761c44b 100644 { if( !isdigit_( buf[ i ] ) ) { -@@ -945,6 +992,9 @@ static void skipArrayScalars( const char * buf, +@@ -928,6 +975,9 @@ static bool skipArrayScalars( const char * buf, i = *start; - + while( i < max ) + assigns( i ) + loopInvariant( *start <= i && i <= max ) @@ -115,9 +115,9 @@ index d8694f0..761c44b 100644 { if( skipAnyScalar( buf, &i, max ) != true ) { -@@ -991,6 +1041,13 @@ static bool skipObjectScalars( const char * buf, +@@ -982,6 +1032,13 @@ static bool skipObjectScalars( const char * buf, i = *start; - + while( i < max ) + assigns( i, *start, comma ) + loopInvariant( @@ -129,11 +129,11 @@ index d8694f0..761c44b 100644 { if( skipString( buf, &i, max ) != true ) { -@@ -1118,6 +1175,14 @@ static JSONStatus_t skipCollection( const char * buf, +@@ -1109,6 +1166,14 @@ static JSONStatus_t skipCollection( const char * buf, i = *start; - + while( i < max ) -+ assigns( i, depth, c, __CPROVER_object_whole( stack ), ret ) ++ assigns( i, depth, c, ret, __CPROVER_object_whole( stack ) ) + loopInvariant( + -1 <= depth && depth <= JSON_MAX_DEPTH + && *start <= i && i <= max @@ -144,9 +144,17 @@ index d8694f0..761c44b 100644 { c = buf[ i ]; i++; -@@ -1407,6 +1472,9 @@ static bool objectSearch( const char * buf, +@@ -1144,6 +1209,7 @@ static JSONStatus_t skipCollection( const char * buf, + + if( skipSpaceAndComma( buf, &i, max ) == true ) + { ++ __CPROVER_assume( isOpenBracket_(stack[depth])); + if( skipScalars( buf, &i, max, stack[ depth ] ) != true ) + { + ret = JSONIllegalDocument; +@@ -1406,6 +1472,9 @@ static bool objectSearch( const char * buf, skipSpace( buf, &i, max ); - + while( i < max ) + assigns( i, key, keyLength, value, valueLength ) + loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max ) @@ -154,9 +162,9 @@ index d8694f0..761c44b 100644 { if( nextKeyValuePair( buf, &i, max, &key, &keyLength, &value, &valueLength ) != true ) -@@ -1474,6 +1542,9 @@ static bool arraySearch( const char * buf, +@@ -1473,6 +1542,9 @@ static bool arraySearch( const char * buf, skipSpace( buf, &i, max ); - + while( i < max ) + assigns( i, currentIndex, value, valueLength ) + loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max && currentIndex < i ) @@ -164,7 +172,7 @@ index d8694f0..761c44b 100644 { if( nextValue( buf, &i, max, &value, &valueLength ) != true ) { -@@ -1539,6 +1610,9 @@ static bool skipQueryPart( const char * buf, +@@ -1538,6 +1610,9 @@ static bool skipQueryPart( const char * buf, while( ( i < max ) && !isSeparator_( buf[ i ] ) && !isSquareOpen_( buf[ i ] ) ) @@ -174,9 +182,9 @@ index d8694f0..761c44b 100644 { i++; } -@@ -1585,6 +1659,17 @@ static JSONStatus_t multiSearch( const char * buf, +@@ -1584,6 +1659,17 @@ static JSONStatus_t multiSearch( const char * buf, coreJSON_ASSERT( ( max > 0U ) && ( queryLength > 0U ) ); - + while( i < queryLength ) + assigns( i, start, queryStart, value, length ) + loopInvariant( @@ -191,4 +199,4 @@ index d8694f0..761c44b 100644 + decreases( queryLength - i ) { bool found = false; - + diff --git a/test/cbmc/proofs/JSON_Validate/Makefile b/test/cbmc/proofs/JSON_Validate/Makefile index 9bbf9bc1..0a361d0e 100644 --- a/test/cbmc/proofs/JSON_Validate/Makefile +++ b/test/cbmc/proofs/JSON_Validate/Makefile @@ -12,5 +12,6 @@ USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical USE_FUNCTION_CONTRACTS += skipAnyScalar USE_FUNCTION_CONTRACTS += skipCollection +USE_FUNCTION_CONTRACTS += skipSpace include ../Makefile-json.common