Skip to content

Commit 96fdb9e

Browse files
author
thk123
committed
Moved the logic of select_pointer_type into test-gen
The base classs behaviour now leaves the type untouched. This requires no further testing so the original tests are now removed. The select_pointer_type class is now passed in to allow configurable behaviour. However, on this branch the behaviour is trivial.
1 parent 3279e56 commit 96fdb9e

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+61
-506
lines changed
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.

regression/cbmc-java/instance-method-user-interface-field/TestClass.java

Lines changed: 0 additions & 44 deletions
This file was deleted.

regression/cbmc-java/instance-method-user-interface-field/test.desc

Lines changed: 0 additions & 5 deletions
This file was deleted.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.

regression/cbmc-java/instance-method-user-interface-two-fields-different/TestClass.java

Lines changed: 0 additions & 61 deletions
This file was deleted.

regression/cbmc-java/instance-method-user-interface-two-fields-different/test.desc

Lines changed: 0 additions & 7 deletions
This file was deleted.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.

regression/cbmc-java/static-method-user-interface-param/TestClass.java

Lines changed: 0 additions & 42 deletions
This file was deleted.

regression/cbmc-java/static-method-user-interface-param/test.desc

Lines changed: 0 additions & 6 deletions
This file was deleted.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.

regression/cbmc-java/static-method-user-interface-two-params-different/TestClass.java

Lines changed: 0 additions & 57 deletions
This file was deleted.

regression/cbmc-java/static-method-user-interface-two-params-different/test.desc

Lines changed: 0 additions & 8 deletions
This file was deleted.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.

regression/cbmc-java/static-method-user-interface-two-params-same/TestClass.java

Lines changed: 0 additions & 41 deletions
This file was deleted.

regression/cbmc-java/static-method-user-interface-two-params-same/test.desc

Lines changed: 0 additions & 6 deletions
This file was deleted.

src/goto-programs/convert_nondet.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Reuben Thomas, [email protected]
1414
#include "goto-programs/goto_model.h"
1515
#include "goto-programs/remove_skip.h"
1616

17+
#include <memory>
1718
#include "java_bytecode/java_object_factory.h" // gen_nondet_init
1819

1920
#include "util/irep_ids.h"
@@ -88,6 +89,7 @@ static goto_programt::targett insert_nondet_init_code(
8889
allocation_typet::DYNAMIC,
8990
!nullable,
9091
max_nondet_array_length,
92+
std::make_shared<select_pointer_typet>(),
9193
update_in_placet::NO_UPDATE_IN_PLACE);
9294

9395
// Convert this code into goto instructions

src/java_bytecode/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ SRC = bytecode_info.cpp \
22
character_refine_preprocess.cpp \
33
ci_lazy_methods.cpp \
44
expr2java.cpp \
5-
get_concrete_class_alphabetically.cpp \
65
jar_file.cpp \
76
java_bytecode_convert_class.cpp \
87
java_bytecode_convert_method.cpp \

0 commit comments

Comments
 (0)