CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
assignments_from_json.cpp File Reference
+ Include dependency graph for assignments_from_json.cpp:

Go to the source code of this file.

Classes

struct  object_creation_infot
 Values passed around between most functions of the recursive deterministic assignment algorithm entered from assign_from_json. More...
 
struct  get_or_create_reference_resultt
 

Functions

static java_class_typet followed_class_type (const exprt &expr, const symbol_table_baset &symbol_table)
 
static bool has_enum_type (const exprt &expr, const symbol_table_baset &symbol_table)
 
static bool is_enum_with_type_equal_to_declaring_type (const exprt &expr, const symbol_table_baset &symbol_table, const java_class_typet &declaring_class_type)
 This function is used as a workaround until reference-equal objects defined across several classes are tracked correctly.
 
static std::optional< std::string > get_type (const jsont &json)
 If the argument has a "@type" key, return the corresponding value, else return an empty optional.
 
static bool has_id (const jsont &json)
 Return true iff the argument has a "@id" key.
 
static bool is_reference (const jsont &json)
 Return true iff the argument has a "@ref" key.
 
static std::string get_id_or_reference_value (const jsont &json)
 Return the unique ID of all objects that are reference-equal to this one.
 
static std::string get_enum_id (const exprt &expr, const jsont &json, const symbol_table_baset &symbol_table)
 Return a unique ID for an enum, based on its type and name field.
 
static bool has_nondet_length (const jsont &json)
 Return true iff the argument has a "@nondetLength": true entry.
 
static jsont get_untyped (const jsont &json, const std::string &object_key)
 For typed versions of primitive, string or array types, looks up their untyped contents with the key specific to their type.
 
static jsont get_untyped_primitive (const jsont &json)
 get_untyped for primitive types.
 
static json_arrayt get_untyped_array (const jsont &json, const typet &element_type)
 get_untyped for array types.
 
static jsont get_untyped_string (const jsont &json)
 get_untyped for string types.
 
static std::optional< java_class_typetruntime_type (const jsont &json, const std::optional< std::string > &type_from_array, const symbol_table_baset &symbol_table)
 Given a JSON representation of a (non-array) reference-typed object and a type inferred from the type of a containing array, get the runtime type of the corresponding pointer expression.
 
static std::optional< std::string > element_type_from_array_type (const jsont &json, const std::optional< std::string > &type_from_array)
 Given a JSON representation of an array and a type inferred from the type of a containing array, get the element type by removing the leading '['.
 
code_with_references_listt assign_from_json_rec (const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
 Entry point of the recursive deterministic assignment algorithm.
 
static code_with_references_listt assign_primitive_from_json (const exprt &expr, const jsont &json)
 One of the base cases (primitive case) of the recursion.
 
static code_frontend_assignt assign_null (const exprt &expr)
 One of the base cases of the recursive algorithm.
 
static code_with_references_listt assign_array_data_component_from_json (const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
 In the case of an assignment of an array given a JSON representation, this function assigns the data component of the array, which contains the array elements.
 
static std::pair< symbol_exprt, code_with_references_listtnondet_length (allocate_objectst &allocate, source_locationt loc)
 Declare a non-deterministic length expression.
 
static std::pair< code_with_references_listt, exprtassign_det_length_array_from_json (const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where expr represents an array which is not flagged with @nondetLength.
 
static code_with_references_listt assign_nondet_length_array_from_json (const exprt &array, const jsont &json, const exprt &given_length_expr, const std::optional< std::string > &type_from_array, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where expr represents an array which is flagged with @nondetLength.
 
static code_frontend_assignt assign_string_from_json (const jsont &json, const exprt &expr, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where expr represents a string.
 
static code_with_references_listt assign_struct_components_from_json (const exprt &expr, const jsont &json, object_creation_infot &info)
 Helper function for assign_struct_from_json which recursively assigns values to all of the fields of the Java object represented by expr (the components of its type and all of its parent types).
 
static code_with_references_listt assign_struct_from_json (const exprt &expr, const jsont &json, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where expr is a struct, which is the result of dereferencing a pointer that corresponds to the Java object described in json.
 
static code_with_references_listt assign_non_enum_pointer_from_json (const exprt &expr, const jsont &json, object_creation_infot &info)
 Same as assign_pointer_from_json without special cases (enums).
 
static code_with_references_listt assign_enum_from_json (const exprt &expr, const jsont &json, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where the expression to be assigned a value is an enum constant that is referenced outside of the definition of its type.
 
static code_with_references_listt assign_pointer_from_json (const exprt &expr, const jsont &json, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where expr is a pointer to a struct, whose type is the same as the runtime-type of the corresponding Java object.
 
static code_with_references_listt assign_pointer_with_given_type_from_json (const exprt &expr, const jsont &json, const java_class_typet &runtime_type, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where expr is a pointer to a struct, and runtime_type is the runtime type of the corresponding Java object, which may be more specific than the type pointed to by expr.type() (the compile-time type of the object).
 
static get_or_create_reference_resultt get_or_create_reference (const exprt &expr, const std::string &id, object_creation_infot &info)
 Helper function for assign_reference_from_json.
 
static code_with_references_listt assign_reference_from_json (const exprt &expr, const jsont &json, const std::optional< std::string > &type_from_array, object_creation_infot &info)
 One of the cases in the recursive algorithm: the case where expr corresponds to a Java object that is reference-equal to one or more other Java objects represented in the initial JSON file.
 
code_with_references_listt assign_from_json (const exprt &expr, const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > &needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references)
 Given an expression expr representing a Java object or primitive and a JSON representation json of the value of a Java object or primitive of a compatible type, adds statements to block to assign expr to the deterministic value specified by json.
 

Function Documentation

◆ assign_array_data_component_from_json()

static code_with_references_listt assign_array_data_component_from_json ( const exprt expr,
const jsont json,
const std::optional< std::string > &  type_from_array,
object_creation_infot info 
)
static

In the case of an assignment of an array given a JSON representation, this function assigns the data component of the array, which contains the array elements.

expr is a pointer to the array containing the component.

Definition at line 392 of file assignments_from_json.cpp.

◆ assign_det_length_array_from_json()

static std::pair< code_with_references_listt, exprt > assign_det_length_array_from_json ( const exprt expr,
const jsont json,
const std::optional< std::string > &  type_from_array,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where expr represents an array which is not flagged with @nondetLength.

The length of the array is given by symbol given_length_expr. We assume that an array with this symbol as its length has already been allocated and that expr has been assigned to it. We constraint the length of the array to be the number of elements, which is known and constant. For the assignment of the array elements, see assign_array_data_component_from_json. For the overall algorithm, see assign_from_json_rec.

Returns
code for the assignment and length of the created array.

Definition at line 457 of file assignments_from_json.cpp.

◆ assign_enum_from_json()

static code_with_references_listt assign_enum_from_json ( const exprt expr,
const jsont json,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where the expression to be assigned a value is an enum constant that is referenced outside of the definition of its type.

(See is_enum_with_type_equal_to_declaring_type for this temporary distinction. See assign_from_json for details about the recursion.) Once reference-equality of fields in different classes is supported, this function can be removed.

Definition at line 623 of file assignments_from_json.cpp.

◆ assign_from_json()

code_with_references_listt assign_from_json ( const exprt expr,
const jsont json,
const irep_idt function_id,
symbol_table_baset symbol_table,
std::optional< ci_lazy_methods_neededt > &  needed_lazy_methods,
size_t  max_user_array_length,
std::unordered_map< std::string, object_creation_referencet > &  references 
)

Given an expression expr representing a Java object or primitive and a JSON representation json of the value of a Java object or primitive of a compatible type, adds statements to block to assign expr to the deterministic value specified by json.

The expected format of the JSON representation is mostly the same as that of the json-io serialization library (https://github.com/jdereg/json-io) if run with the following options, as of version 4.10.1:

  • A type name map with identity mappings such as ("java.lang.Boolean", "java.lang.Boolean") for all primitive wrapper types, java.lang.Class, java.lang.String and java.util.Date. That is, we are not using the json-io default shorthands for those types.
  • WRITE_LONGS_AS_STRINGS should be set to true to avoid a loss of precision when representing longs.

Some examples of json-io representations that may not be obvious include:

  • The representation of a Java object generally may or may not contain a "@type" key. The value corresponding to such a key specifies the runtime type of the object (or the boxed type if the object is primitive). If no "@type" key is present, it is assumed that the runtime type is the same as the compile-time type. Most reference-typed objects are represented as JSON objects (i.e. key-value maps) either way, so the "@type" key is just an additional key in the map. However, primitive types, arrays and string types without a "@type" key are not represented as JSON objects. For example, "untyped" ints are just represented as e.g. 1234, i.e. a JSON number. The "typed" version of this int then becomes {"@type":"java.lang.Integer","value":1234}, i.e. a JSON object, with the original ("untyped") JSON number stored in the "value" entry. For arrays, the corresponding key is called "@items", not "value". Typed versions of primitive types are probably not necessary, but json-io will sometimes produce such values, which is why we support both typed and untyped versions.
  • The way we deal with reference-equal objects is that they all get assigned the same ID, and exactly one of them will have an {"@id": some_ID} entry, in addition to its usual representation. All the other objects with this ID are represented simply as {"@ref": some_ID}, with no further entries.

The above rule has the following exceptions:

  • It seems that strings are always printed in "primitive" representation by json-io, i.e. they are always JSON strings, and never JSON objects with a @type key. For cases where we don't know that an expression has a string type (e.g. if its type is generic and specialized to java.lang.String), we need to sometimes represent strings as JSON objects with a @type key. In this case, the content of the string will be the value associated with a value key (similarly to StringBuilder in json-io). See get_untyped_string.
  • json-io does not include the ordinal field of enums in its representation, but our algorithm depends on it being present. It may be possible to rewrite parts of it to set the ordinal depending on the order of elements seen in the $VALUES array, but it would generally make things more complicated.

For examples of JSON representations of objects, see the regression tests for this feature in jbmc/regression/jbmc/deterministic_assignments_json.

Known limitations:

  • If two reference-equal objects are defined in the same function, they are correctly assigned the same value. However, the case where they are defined in two different functions is not supported. The object that is stored as a {"@ref":1} or similar will generally either point to a freshly allocated symbol or an out-of-scope symbol. The {"@id":1} (or similar) object may be assigned correctly, or it may point to an out-of-scope symbol. This is because the symbol for the shared value is currently allocated dynamically. To fix this limitation, static allocation would have to be used instead, together with a static boolean to keep track of whether or not the symbol has been allocated already.
  • The special floating-point values NaN and positive/negative infinity are not supported. Note that in json-io 4.10.1, these are printed as "null". Future versions of json-io will support these values, and this function should be consistent with that if possible.
  • json-io prints \uFFFF as a single character, which is not read correctly by the JSON parser.
  • Not all assignments have source locations, and those that do only link to a function, not a line number.

For parameter documentation, see object_creation_infot.

Definition at line 914 of file assignments_from_json.cpp.

◆ assign_from_json_rec()

code_with_references_listt assign_from_json_rec ( const exprt expr,
const jsont json,
const std::optional< std::string > &  type_from_array,
object_creation_infot info 
)

Entry point of the recursive deterministic assignment algorithm.

Parameters
exprexpression to assign a deterministic value to. In the case of the entry point, this is either a pointer to a struct, or an expression corresponding to a Java primitive.
jsona JSON representation of the deterministic value to assign.
type_from_arrayif expr was found as an element of an array, the element type of this array.
inforeferences used throughout the recursive algorithm.

Definition at line 850 of file assignments_from_json.cpp.

◆ assign_non_enum_pointer_from_json()

static code_with_references_listt assign_non_enum_pointer_from_json ( const exprt expr,
const jsont json,
object_creation_infot info 
)
static

Same as assign_pointer_from_json without special cases (enums).

Definition at line 600 of file assignments_from_json.cpp.

◆ assign_nondet_length_array_from_json()

static code_with_references_listt assign_nondet_length_array_from_json ( const exprt array,
const jsont json,
const exprt given_length_expr,
const std::optional< std::string > &  type_from_array,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where expr represents an array which is flagged with @nondetLength.

The length of the array is given by symbol given_length_expr. We assume that an array with this symbol as its length has already been allocated and that expr has been assigned to it. We constrain the length of the array to be greater or equal to the number of elements specified in json. For the assignment of the array elements, see assign_array_data_component_from_json. For the overall algorithm, see assign_from_json_rec.

Returns
code for the assignment and length of the created array.

Definition at line 485 of file assignments_from_json.cpp.

◆ assign_null()

static code_frontend_assignt assign_null ( const exprt expr)
static

One of the base cases of the recursive algorithm.

See assign_from_json_rec.

Definition at line 383 of file assignments_from_json.cpp.

◆ assign_pointer_from_json()

static code_with_references_listt assign_pointer_from_json ( const exprt expr,
const jsont json,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where expr is a pointer to a struct, whose type is the same as the runtime-type of the corresponding Java object.

See assign_from_json_rec.

Definition at line 665 of file assignments_from_json.cpp.

◆ assign_pointer_with_given_type_from_json()

static code_with_references_listt assign_pointer_with_given_type_from_json ( const exprt expr,
const jsont json,
const java_class_typet runtime_type,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where expr is a pointer to a struct, and runtime_type is the runtime type of the corresponding Java object, which may be more specific than the type pointed to by expr.type() (the compile-time type of the object).

See assign_from_json_rec.

Definition at line 683 of file assignments_from_json.cpp.

◆ assign_primitive_from_json()

static code_with_references_listt assign_primitive_from_json ( const exprt expr,
const jsont json 
)
static

One of the base cases (primitive case) of the recursion.

For characters, the encoding in json is assumed to be UTF-8. See assign_from_json_rec.

Definition at line 342 of file assignments_from_json.cpp.

◆ assign_reference_from_json()

static code_with_references_listt assign_reference_from_json ( const exprt expr,
const jsont json,
const std::optional< std::string > &  type_from_array,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where expr corresponds to a Java object that is reference-equal to one or more other Java objects represented in the initial JSON file.

See assign_from_json_rec. Such an object will either have the key-value pair @id: some_key in json, together with a full representation of the object, or it will only have one key-value pair, @ref: some_key. For each key, there is only one @id field in the JSON file. A special case is enums, which are always represented as a full object without any @id or @ref keys. This is mostly the same as the output from json-io for enums, except that in our representation, we need to include the ordinal field so that e.g. switch statements on enums will work. We keep track of object IDs using a map from IDs to symbol expressions. Usually the ID is the some_key from the example above, except for enums, where the ID is of the form my.package.name.EnumName.CONSTANT. The first time we see an ID (@id, @ref or enum constant), we allocate a symbol for it. The first time we see the full representation of the object (@id or enum constant) we initialize the allocated memory. This strategy may need to be changed to support reference-equality of fields across several different classes (e.g. as soon as we find a @ref for the first time we might want to search the whole initial JSON file for the corresponding @id).

Definition at line 794 of file assignments_from_json.cpp.

◆ assign_string_from_json()

static code_frontend_assignt assign_string_from_json ( const jsont json,
const exprt expr,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where expr represents a string.

See assign_from_json_rec.

Definition at line 512 of file assignments_from_json.cpp.

◆ assign_struct_components_from_json()

static code_with_references_listt assign_struct_components_from_json ( const exprt expr,
const jsont json,
object_creation_infot info 
)
static

Helper function for assign_struct_from_json which recursively assigns values to all of the fields of the Java object represented by expr (the components of its type and all of its parent types).

Definition at line 528 of file assignments_from_json.cpp.

◆ assign_struct_from_json()

static code_with_references_listt assign_struct_from_json ( const exprt expr,
const jsont json,
object_creation_infot info 
)
static

One of the cases in the recursive algorithm: the case where expr is a struct, which is the result of dereferencing a pointer that corresponds to the Java object described in json.

See assign_from_json_rec.

Definition at line 572 of file assignments_from_json.cpp.

◆ element_type_from_array_type()

static std::optional< std::string > element_type_from_array_type ( const jsont json,
const std::optional< std::string > &  type_from_array 
)
static

Given a JSON representation of an array and a type inferred from the type of a containing array, get the element type by removing the leading '['.

Types for arrays are stored in the format "[Lmy.package.name.ClassName;". In this case, the returned value would be "Lmy.package.name.ClassName;". type_from_array would only have a value if this array is stored within another array, i.e. within a ClassName[][]. Keeping track of array types in this way is necessary to assign generic arrays with no compile-time types.

Parameters
jsonJSON representation of an array. If it contains a @type field, this takes priority over type_from_array.
type_from_arraymay contain a type name from a containing array.
Returns
if the type of an array was given, the type of its elements.

Definition at line 307 of file assignments_from_json.cpp.

◆ followed_class_type()

static java_class_typet followed_class_type ( const exprt expr,
const symbol_table_baset symbol_table 
)
static

Definition at line 68 of file assignments_from_json.cpp.

◆ get_enum_id()

static std::string get_enum_id ( const exprt expr,
const jsont json,
const symbol_table_baset symbol_table 
)
static

Return a unique ID for an enum, based on its type and name field.

This is needed for the enum workaround until reference-equality across different classes is supported. See is_enum_with_type_equal_to_declaring_type.

Definition at line 171 of file assignments_from_json.cpp.

◆ get_id_or_reference_value()

static std::string get_id_or_reference_value ( const jsont json)
static

Return the unique ID of all objects that are reference-equal to this one.

This is the value corresponding to a "@id" or "@ref" key. See has_id and is_reference.

Definition at line 159 of file assignments_from_json.cpp.

◆ get_or_create_reference()

static get_or_create_reference_resultt get_or_create_reference ( const exprt expr,
const std::string &  id,
object_creation_infot info 
)
static

Helper function for assign_reference_from_json.

Look up the given id in the reference map and gets or creates the symbol for it. In the case of arrays, if the first time we see an ID is in a @ref object (rather than @id), we do not know what the length of the array will be, so we need to allocate an array of nondeterministic length. The length will be constrained (in assign_nondet_length_array_from_json) once we find the corresponding @id object.

Parameters
exprexpression representing the Java object for which a symbol is retrieved or allocated.
idkey in the reference map for this object
inforeferences used throughout the recursive algorithm.
Returns
a pair: the first element is true if a new symbol was allocated for the given ID and false if the ID was found in the reference map. The second element has the symbol expression(s) for this ID.

Definition at line 739 of file assignments_from_json.cpp.

◆ get_type()

static std::optional< std::string > get_type ( const jsont json)
static

If the argument has a "@type" key, return the corresponding value, else return an empty optional.

A runtime type that is different from the objects compile-time type should be specified in json in this way. Type values are of the format "my.package.name.ClassName".

Definition at line 120 of file assignments_from_json.cpp.

◆ get_untyped()

static jsont get_untyped ( const jsont json,
const std::string &  object_key 
)
static

For typed versions of primitive, string or array types, looks up their untyped contents with the key specific to their type.

See the examples on assign_from_json for the terminology used here (typed vs. untyped).

Definition at line 202 of file assignments_from_json.cpp.

◆ get_untyped_array()

static json_arrayt get_untyped_array ( const jsont json,
const typet element_type 
)
static

get_untyped for array types.

char arrays are treated as a special case as they are represented as an array of a single String element by json-io, rather than an array of one or more char elements.

Definition at line 225 of file assignments_from_json.cpp.

◆ get_untyped_primitive()

static jsont get_untyped_primitive ( const jsont json)
static

get_untyped for primitive types.

Definition at line 215 of file assignments_from_json.cpp.

◆ get_untyped_string()

static jsont get_untyped_string ( const jsont json)
static

get_untyped for string types.

Note that this differs from the standard serialization of java.lang.String in json-io, but is consistent with the serialization of StringBuilder and StringBuffer.

Definition at line 252 of file assignments_from_json.cpp.

◆ has_enum_type()

static bool has_enum_type ( const exprt expr,
const symbol_table_baset symbol_table 
)
static

Definition at line 76 of file assignments_from_json.cpp.

◆ has_id()

static bool has_id ( const jsont json)
static

Return true iff the argument has a "@id" key.

The presence of such a key means that there exist objects that are reference-equal to this object. The corresponding value is the unique ID of all objects that are reference- equal to this one. All other key-value pairs of json should be as usual.

Definition at line 136 of file assignments_from_json.cpp.

◆ has_nondet_length()

static bool has_nondet_length ( const jsont json)
static

Return true iff the argument has a "@nondetLength": true entry.

If such an entry is present on a JSON representation of an array, it means that the array should be assigned a nondeterministic length, constrained to be at least the number of elements specified for this array.

Definition at line 189 of file assignments_from_json.cpp.

◆ is_enum_with_type_equal_to_declaring_type()

static bool is_enum_with_type_equal_to_declaring_type ( const exprt expr,
const symbol_table_baset symbol_table,
const java_class_typet declaring_class_type 
)
static

This function is used as a workaround until reference-equal objects defined across several classes are tracked correctly.

Once reference-equality works in all cases, this function can be removed. Until then, in the case of an enum expression that needs to be assigned a value, we distinguish between two cases: 1) the declaring class of the enum expression is the same as the type of the enum expression. For example, for an enum Pet {DOG, CAT}, the declaring class of the expression Pet.DOG is Pet, and the type of the expression is also Pet. The same is true for the expressions that represent the elements of the $VALUES array of Pet, and for any user-defined Pet-typed fields in Pet.java. In this case, initialize the expression just as a regular object that has known reference-equal objects. (Corresponds to creating the enum constant in Java or referencing it directly.) See assign_reference_from_json. 2) otherwise, initialize it by indexing the $VALUES array with the given ordinal. An example of this case would be the field pet in class MyClass { Pet pet; } (its declaring class is MyClass and its own type is Pet). See assign_enum_from_json.

Parameters
expran expression representing a Java object.
symbol_tableused for looking up the type of expr.
declaring_class_typetype of the class where expr is declared.
Returns
true if expr has an enum type and is declared within the definition of that same type, false otherwise.

Definition at line 105 of file assignments_from_json.cpp.

◆ is_reference()

static bool is_reference ( const jsont json)
static

Return true iff the argument has a "@ref" key.

The corresponding value is the unique ID of all objects that are reference- equal to this one. Any other key-value pairs of json will be ignored.

Definition at line 148 of file assignments_from_json.cpp.

◆ nondet_length()

static std::pair< symbol_exprt, code_with_references_listt > nondet_length ( allocate_objectst allocate,
source_locationt  loc 
)
static

Declare a non-deterministic length expression.

Parameters
[out]allocateallocation functor
loclocation for the created code
Returns
the length expression that has been non-deterministically created and the code declaring the expression

Definition at line 433 of file assignments_from_json.cpp.

◆ runtime_type()

static std::optional< java_class_typet > runtime_type ( const jsont json,
const std::optional< std::string > &  type_from_array,
const symbol_table_baset symbol_table 
)
static

Given a JSON representation of a (non-array) reference-typed object and a type inferred from the type of a containing array, get the runtime type of the corresponding pointer expression.

Parameters
jsonJSON representation of a non-array object. If it contains a @type field, this takes priority over type_from_array. Types for non- array objects are stored in the JSON in the format "my.package.name.ClassName".
type_from_arraymay contain an element type name given by a containing array. Such types are stored in the form "Lmy.package.name.ClassName;".
symbol_tableused to look up the type given its name.
Returns
runtime type of the object, if specified by at least one of the parameters.

Definition at line 270 of file assignments_from_json.cpp.