diff --git a/docs/doxygen/include/size_table.md b/docs/doxygen/include/size_table.md
index 6872985a..dbc91357 100644
--- a/docs/doxygen/include/size_table.md
+++ b/docs/doxygen/include/size_table.md
@@ -9,12 +9,12 @@
| core_json.c |
- 3.1K |
+ 3.0K |
2.5K |
| Total estimates |
- 3.1K |
+ 3.0K |
2.5K |
diff --git a/loop_invariants.patch b/loop_invariants.patch
index f6a76b1d..581f1dfd 100644
--- a/loop_invariants.patch
+++ b/loop_invariants.patch
@@ -1,32 +1,32 @@
diff --git a/source/core_json.c b/source/core_json.c
-index 901b2e1..8bdd89c 100644
+index d8694f0..761c44b 100644
--- a/source/core_json.c
+++ b/source/core_json.c
-@@ -62,6 +62,21 @@ typedef union
- #define isSquareOpen_( x ) ( ( x ) == '[' )
- #define isSquareClose_( x ) ( ( x ) == ']' )
-
+@@ -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
+ * https://diffblue.github.io/cbmc/contracts-user.html.
+ */
+#ifdef CBMC
-+#define loopInvariant(...) __CPROVER_loop_invariant(__VA_ARGS__)
-+#define decreases(...) __CPROVER_decreases(__VA_ARGS__)
-+#define assigns(...) __CPROVER_assigns(__VA_ARGS__)
++ #define loopInvariant(...) __CPROVER_loop_invariant(__VA_ARGS__)
++ #define decreases(...) __CPROVER_decreases(__VA_ARGS__)
++ #define assigns(...) __CPROVER_assigns(__VA_ARGS__)
+#else
-+#define loopInvariant(...)
-+#define decreases(...)
-+#define assigns(...)
++ #define loopInvariant(...)
++ #define decreases(...)
++ #define assigns(...)
+#endif
+
/**
* @brief Advance buffer index beyond whitespace.
*
-@@ -78,6 +93,9 @@ static void skipSpace( const char * buf,
+@@ -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 )
@@ -34,9 +34,9 @@ index 901b2e1..8bdd89c 100644
{
if( !isspace_( buf[ i ] ) )
{
-@@ -102,6 +120,13 @@ static size_t countHighBits( uint8_t c )
+@@ -103,6 +121,13 @@ static size_t countHighBits( uint8_t c )
size_t i = 0;
-
+
while( ( n & 0x80U ) != 0U )
+ assigns( i, n )
+ loopInvariant (
@@ -48,7 +48,7 @@ index 901b2e1..8bdd89c 100644
{
i++;
n = ( n & 0x7FU ) << 1U;
-@@ -210,6 +235,13 @@ static bool skipUTF8MultiByte( const char * buf,
+@@ -211,6 +236,13 @@ static bool skipUTF8MultiByte( const char * buf,
/* The bit count is 1 greater than the number of bytes,
* e.g., when j is 2, we skip one more byte. */
for( j = bitCount - 1U; j > 0U; j-- )
@@ -61,8 +61,8 @@ index 901b2e1..8bdd89c 100644
+ decreases( j )
{
i++;
-
-@@ -345,6 +377,12 @@ static bool skipOneHexEscape( const char * buf,
+
+@@ -346,6 +378,12 @@ static bool skipOneHexEscape( const char * buf,
if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
{
for( i += 2U; i < end; i++ )
@@ -74,10 +74,10 @@ index 901b2e1..8bdd89c 100644
+ decreases( end - i )
{
uint8_t n = hexToInt( buf[ i ] );
-
-@@ -522,6 +560,9 @@ static bool skipString( const char * buf,
+
+@@ -523,6 +561,9 @@ static bool skipString( const char * buf,
i++;
-
+
while( i < max )
+ assigns( i )
+ loopInvariant( *start + 1U <= i && i <= max )
@@ -85,9 +85,9 @@ index 901b2e1..8bdd89c 100644
{
if( buf[ i ] == '"' )
{
-@@ -580,6 +621,9 @@ static bool strnEq( const char * a,
+@@ -581,6 +622,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,17 +95,9 @@ index 901b2e1..8bdd89c 100644
{
if( a[ i ] != b[ i ] )
{
-@@ -681,6 +725,7 @@ static bool skipAnyLiteral( const char * buf,
- * false otherwise.
- */
- #define MAX_FACTOR ( MAX_INDEX_VALUE / 10 )
-+
- static bool skipDigits( const char * buf,
- size_t * start,
- size_t max,
-@@ -695,6 +740,9 @@ static bool skipDigits( const char * buf,
+@@ -696,6 +740,9 @@ static bool skipDigits( const char * buf,
saveStart = *start;
-
+
for( i = *start; i < max; i++ )
+ assigns( value, i )
+ loopInvariant( *start <= i && i <= max )
@@ -113,9 +105,9 @@ index 901b2e1..8bdd89c 100644
{
if( !isdigit_( buf[ i ] ) )
{
-@@ -944,6 +992,9 @@ static void skipArrayScalars( const char * buf,
+@@ -945,6 +992,9 @@ static void skipArrayScalars( const char * buf,
i = *start;
-
+
while( i < max )
+ assigns( i )
+ loopInvariant( *start <= i && i <= max )
@@ -123,9 +115,9 @@ index 901b2e1..8bdd89c 100644
{
if( skipAnyScalar( buf, &i, max ) != true )
{
-@@ -986,6 +1037,13 @@ static bool skipObjectScalars( const char * buf,
+@@ -991,6 +1041,13 @@ static bool skipObjectScalars( const char * buf,
i = *start;
-
+
while( i < max )
+ assigns( i, *start, comma )
+ loopInvariant(
@@ -137,9 +129,9 @@ index 901b2e1..8bdd89c 100644
{
if( skipString( buf, &i, max ) != true )
{
-@@ -1082,6 +1140,14 @@ static JSONStatus_t skipCollection( const char * buf,
+@@ -1118,6 +1175,14 @@ static JSONStatus_t skipCollection( const char * buf,
i = *start;
-
+
while( i < max )
+ assigns( i, depth, c, __CPROVER_object_whole( stack ), ret )
+ loopInvariant(
@@ -152,9 +144,9 @@ index 901b2e1..8bdd89c 100644
{
c = buf[ i ];
i++;
-@@ -1363,6 +1429,9 @@ static bool objectSearch( const char * buf,
+@@ -1407,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 )
@@ -162,9 +154,9 @@ index 901b2e1..8bdd89c 100644
{
if( nextKeyValuePair( buf, &i, max, &key, &keyLength,
&value, &valueLength ) != true )
-@@ -1430,6 +1499,9 @@ static bool arraySearch( const char * buf,
+@@ -1474,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 )
@@ -172,7 +164,7 @@ index 901b2e1..8bdd89c 100644
{
if( nextValue( buf, &i, max, &value, &valueLength ) != true )
{
-@@ -1495,6 +1567,9 @@ static bool skipQueryPart( const char * buf,
+@@ -1539,6 +1610,9 @@ static bool skipQueryPart( const char * buf,
while( ( i < max ) &&
!isSeparator_( buf[ i ] ) &&
!isSquareOpen_( buf[ i ] ) )
@@ -182,9 +174,9 @@ index 901b2e1..8bdd89c 100644
{
i++;
}
-@@ -1541,6 +1616,17 @@ static JSONStatus_t multiSearch( const char * buf,
+@@ -1585,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(
@@ -199,4 +191,4 @@ index 901b2e1..8bdd89c 100644
+ decreases( queryLength - i )
{
bool found = false;
-
+
diff --git a/source/core_json.c b/source/core_json.c
index a47dcc49..d8694f0c 100644
--- a/source/core_json.c
+++ b/source/core_json.c
@@ -60,6 +60,8 @@ typedef union
#define isMatchingBracket_( x, y ) ( isCurlyPair_( x, y ) || isSquarePair_( x, y ) )
#define isSquareOpen_( x ) ( ( x ) == '[' )
#define isSquareClose_( x ) ( ( x ) == ']' )
+#define isCurlyOpen_( x ) ( ( x ) == '{' )
+#define isCurlyClose_( x ) ( ( x ) == '}' )
/**
* @brief Advance buffer index beyond whitespace.
@@ -1047,6 +1049,7 @@ static bool skipScalars( const char * buf,
size_t max,
char mode )
{
+ size_t i = 0U;
bool modeIsOpenBracket = ( bool ) isOpenBracket_( mode );
bool ret = true;
@@ -1060,13 +1063,24 @@ static bool skipScalars( const char * buf,
skipSpace( buf, start, max );
- if( mode == '[' )
- {
- skipArrayScalars( buf, start, max );
- }
- else
+ i = *start;
+
+ if( i < max )
{
- ret = skipObjectScalars( buf, start, max );
+ if( mode == '[' )
+ {
+ if( !isSquareClose_( buf[ i ] ) )
+ {
+ skipArrayScalars( buf, start, max );
+ }
+ }
+ else
+ {
+ if( !isCurlyClose_( buf[ i ] ) )
+ {
+ ret = skipObjectScalars( buf, start, max );
+ }
+ }
}
return ret;
diff --git a/test/unit-test/core_json_utest.c b/test/unit-test/core_json_utest.c
index c5107562..f3c29866 100644
--- a/test/unit-test/core_json_utest.c
+++ b/test/unit-test/core_json_utest.c
@@ -146,6 +146,12 @@
"\":{\"" SECOND_QUERY_KEY "\" : \"" COMPLETE_QUERY_KEY_ANSWER "\"}} "
#define JSON_DOC_LEGAL_TRAILING_SPACE_LENGTH ( sizeof( JSON_DOC_LEGAL_TRAILING_SPACE ) - 1 )
+#define JSON_DOC_LEGAL_EMPTY_OBJECT "{\"foo\":{}}"
+#define JSON_DOC_LEGAL_EMPTY_OBJECT_LENGTH ( sizeof( JSON_DOC_LEGAL_EMPTY_OBJECT ) - 1 )
+
+#define JSON_DOC_LEGAL_EMPTY_ARRAY "{\"foo\":[]}"
+#define JSON_DOC_LEGAL_EMPTY_ARRAY_LENGTH ( sizeof( JSON_DOC_LEGAL_EMPTY_ARRAY ) - 1 )
+
/* A single scalar is still considered a valid JSON document. */
#define SINGLE_SCALAR "\"l33t\""
#define SINGLE_SCALAR_LENGTH ( sizeof( SINGLE_SCALAR ) - 1 )
@@ -564,6 +570,14 @@ void test_JSON_Validate_Legal_Documents( void )
JSON_DOC_LEGAL_TRAILING_SPACE_LENGTH );
TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );
+ jsonStatus = JSON_Validate( JSON_DOC_LEGAL_EMPTY_OBJECT,
+ JSON_DOC_LEGAL_EMPTY_OBJECT_LENGTH );
+ TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );
+
+ jsonStatus = JSON_Validate( JSON_DOC_LEGAL_EMPTY_ARRAY,
+ JSON_DOC_LEGAL_EMPTY_ARRAY_LENGTH );
+ TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );
+
jsonStatus = JSON_Validate( JSON_DOC_MULTIPLE_VALID_ESCAPES,
JSON_DOC_MULTIPLE_VALID_ESCAPES_LENGTH );
TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );