Definition at line 73 of file java_object_factory.cpp.

Definition at line 1112 of file java_object_factory.cpp.

Generate codet for assigning an individual element inside the array.

Parameters

element The lhs expression that will be assigned the new element.

update_in_place Should the code allow for the object to updated in place.

element_type The type of the element to create.

depth The depth in the object tree.

location Source location to use for synthesized code

Returns

Synthesized code using the object factory to create an element of the type and assign it into element.

Definition at line 1227 of file java_object_factory.cpp.

Definition at line 1117 of file java_object_factory.cpp.

We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet(int); assume(0 < = i < $VALUES.length); expr = $VALUES[i]; where $VALUES is a variable generated by the Java compiler and which gives the possible values of a particular enum subtype (this is the same array that is returned by Enum.values()).

This may fail if the $VALUES static field is not present. Ensuring that field is in the symbol table when this method may be applicable is the driver program's responsibility: for example, ci_lazy_methods.cpp makes some effort to retain this field when a stub method might refer to it.

Returns

true on success

Definition at line 1470 of file java_object_factory.cpp.

Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects as necessary and nondet-initializing their members, or if MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects.

Extra constraints might be added to initialized objects, based on options recorded in object_factory_parameters.

Parameters

assignments A code block where the initializing assignments will be appended to.

expr Lvalue expression to initialize.

is_sub If true, expr is a substructure of a larger object, which in Java necessarily means a base class.

skip_classid If true, skip initializing @class_identifier.

lifetime Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)

depth Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing.

override_type If not empty, initialize with override_type instead of expr.type(). Used at the moment for reference arrays, which are implemented as void* arrays but should be init'd as their true type with appropriate casts.

update_in_place NO_UPDATE_IN_PLACE: initialize expr from scratch MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ and MUST_ cases. MUST_UPDATE_IN_PLACE: reinitialize an existing object

location Source location associated with nondet-initialization.

Definition at line 995 of file java_object_factory.cpp.

Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree.

It allocates child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects.

Parameters

assignments The code block we are building with initialization code.

expr Pointer-typed lvalue expression to initialize.

lifetime Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)

depth Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing.

pointer_type The type of the pointer we are initalizing

update_in_place

• NO_UPDATE_IN_PLACE: initialize expr from scratch
• MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ and MUST_ cases.
• MUST_UPDATE_IN_PLACE: reinitialize an existing object

location Source location associated with nondet-initialization.

Definition at line 471 of file java_object_factory.cpp.

Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects.

After initialization calls validation method expr.cproverNondetInitialize() if it was provided by the user.

Parameters

assignments The code block to append the new instructions to

expr Struct-typed lvalue expression to initialize

is_sub If true, expr is a substructure of a larger object, which in Java necessarily means a base class

skip_classid If true, skip initializing @class_identifier

lifetime Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)

struct_type The type of the struct we are initializing

depth Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing

update_in_place Enum instance with the following meaning. NO_UPDATE_IN_PLACE: initialize expr from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input

location Source location associated with nondet-initialization

Definition at line 761 of file java_object_factory.cpp.

Generate codet assignments to initalize the selected concrete type.

Generated code looks as follows (here A = replacement_pointer.subtype()):

// allocate memory for a new object, depends on lifetime A { ... } tmp_object;

// non-det init all the fields of A A.x = NONDET(...) A.y = NONDET(...)

// assign expr with a suitably casted pointer to new_object A * p = &tmp_object

Parameters

assignments A block of code where we append the generated code

lifetime Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)

replacement_pointer The type of the pointer we actually want to create

depth Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing

location Source location associated with nondet-initialization

Returns

A symbol expression of type replacement_pointer corresponding to a pointer to object tmp_object (see above)

Definition at line 689 of file java_object_factory.cpp.

Initializes the pointer-typed lvalue expression expr to point to an object of type target_type, recursively nondet-initializing the members of that object.

Code emitted mainly depends on update_in_place:

When in NO_UPDATE_IN_PLACE mode, the code emitted looks like:

When in MUST_UPDATE_IN_PLACE mode, all code is emitted by a recursive call to gen_nondet_init in MUST_UPDATE_IN_PLACE mode, and looks like:

It is illegal to call the function with MAY_UPDATE_IN_PLACE.

Parameters

[out] assignments A code_blockt where the initialization code will be emitted to.

expr Pointer-typed lvalue expression to initialize. The pointed type equals target_type.

target_type Structure type to initialize, which may not match *expr (for example, expr might be have type void*). It cannot be a pointer to a primitive type because Java does not allow so.

lifetime Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)

depth Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing.

update_in_place NO_UPDATE_IN_PLACE: initialize expr from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input

location Source location associated with nondet-initialization.

Definition at line 189 of file java_object_factory.cpp.

Definition at line 59 of file java_object_factory.cpp.

Every time the non-det generator visits a type and the type is generic (either a struct or a pointer), the following map is used to store and look up the concrete types of the generic parameters in the current scope.

Note that not all generic parameters need to have a concrete type, e.g., the method under test is generic. The types are removed from the map when the scope changes. Note that in different depths of the scope the parameters can be specialized with different types so we keep a stack of types for each parameter.

Definition at line 49 of file java_object_factory.cpp.

Log for reporting warnings and errors in object creation.

Definition at line 62 of file java_object_factory.cpp.

Definition at line 33 of file java_object_factory.cpp.

Resolves pointer types potentially using some heuristics, for example to replace pointers to interface types with pointers to concrete implementations.

Definition at line 57 of file java_object_factory.cpp.

This is employed in conjunction with the depth above.

Every time the non-det generator visits a type, the type is added to this set. We forbid the non-det initialization when we see the type for the second time in this set AND the tree depth becomes >= than the maximum value above.

Definition at line 39 of file java_object_factory.cpp.

The symbol table.

Definition at line 52 of file java_object_factory.cpp.