Fix java harness for main() #1768

peterschrammel · 2018-01-26T01:12:20Z

This PR fixes 3 bugs:

the elements of the String[] args of main() must be non-null
the main() method was not correctly recognized (for two different reasons)
~~3. the maybe-null/not-null initialization of the elements of String[] was broken~~ fixed in the meanwhile

~~The regression tests require #1735 to pass (I'll rebase after that one has been merged).~~

romainbrenguier · 2018-01-26T09:23:25Z

src/java_bytecode/java_entry_point.cpp

    bool has_correct_type=
      to_code_type(function.type).return_type().id()==ID_empty &&
      (!to_code_type(function.type).has_this()) &&
      parameters.size()==1 &&
      parameters[0].type().full_eq(string_array_type);
-    is_main=(named_main && has_correct_type);
+    bool public_access = function.type.get(ID_access) == ID_public;
+    is_main=(named_main && has_correct_type && public_access);


spacing is not consistent, can you run clang-format

romainbrenguier · 2018-01-26T09:36:34Z

regression/cbmc-java/main-args-elements-non-null2/Main.java

+      if(args.length>0)
+      {
+	String s = args[0];
+	int i = s.length(); // must not fail


indentation look wrong

romainbrenguier · 2018-01-26T09:45:16Z

regression/cbmc-java/main-args-elements-non-null3/Main.java

+  public static void main(String[] args)
+  {
+    if(args.length>0)
+      assert(args[0] == null); // must fail


Since with your changes strings will be null when --refine-strings is not activated, does that mean that args.length will always be 0?

smowton

Some problems with the tests when --java-throw-runtime-exceptions is not enabled, and the "null if string-refinement is not enabled" behaviour sounds odd.

Also I have a feeling this might be the only user we'll ever see of max_nonnull_tree_depth? Not sure if there's a better solution, but it seems an odd thing for the object factory to be able to do when anyone else wanting to use that feature sounds unlikely.

smowton · 2018-01-26T09:54:36Z

regression/cbmc-java/main-args-elements-non-null2/Main.java

+	int i = s.length(); // must not fail
+      }
+    }
+    catch(Exception e) {


This won't happen without --java-throw-runtime-exceptions. Perhaps it would be better to simply assert s != null?

smowton · 2018-01-26T09:55:35Z

regression/cbmc-java/main-args-elements-non-null4/Main.java

+      {
+	String s = args[0];
+	if(s != null) {
+	  int i = s.length(); // definitely must not fail


Again the exception path is unreachable, but what are you testing for here?

smowton · 2018-01-26T09:56:33Z

regression/cbmc-java/main-args-non-null2/Main.java

+    try {
+      int i = args.length; // args must be non-null
+    }
+    catch(Exception e) {


Same situation -- exception is unreachable whatever happens due to no --java-throw-runtime-exceptions.

smowton · 2018-01-26T09:59:02Z

src/java_bytecode/java_object_factory.cpp

@@ -687,7 +687,8 @@ static bool add_nondet_string_pointer_initialization(
  const struct_typet &struct_type =
    to_struct_type(ns.follow(to_symbol_type(obj.type())));

-  if(!struct_type.has_component("data") || !struct_type.has_component("length"))
+  // if no String model is loaded then we cannot construct a String object
+  if(struct_type.get_bool(ID_incomplete_class))


No String model does not imply incomplete-class -- for example, we might have a real java.lang.String in the classpath.

smowton · 2018-01-26T10:00:04Z

src/java_bytecode/java_object_factory.cpp

@@ -858,8 +860,10 @@ void java_object_factoryt::gen_nondet_pointer_init(

  // Alternatively, if this is a void* we *must* initialise with null:
  // (This can currently happen for some cases of #exception_value)
+  // Also, if the String model is not loaded then we can only


??? Even if we have an incomplete java.lang.String, we can supply { @class_identifier = "java.lang.String" }

thk123

I'm pretty sure your last commit is wrong - specifically, I don't think Ljava.lang.String; is a valid signature/descriptor type string (the dots should be slashes in bytecode strings).

More generally, I think a better approach to certain inputs being not null might be to mark them in the symbol table in some way (perhaps allowing future models to specify parts that are non-null and parts that are not in a more granular manner).

There are lots of tests with quite a lot of overlap, but I think one that checks that more than the first element is guaranteed to be non-null in suitable cases is missing:

public class Main
{
  public static void main(String[] args)
  {
    if(args.length>1)
      assert(args[0] != null); // must hold
      assert(args[1] != null); // must hold
  }
}

thk123 · 2018-02-16T15:12:10Z

src/java_bytecode/java_entry_point.cpp

    bool has_correct_type=
      to_code_type(function.type).return_type().id()==ID_empty &&
      (!to_code_type(function.type).has_this()) &&
      parameters.size()==1 &&
      parameters[0].type().full_eq(string_array_type);
-    is_main=(named_main && has_correct_type);
+    bool public_access = function.type.get(ID_access) == ID_public;


Prefer storing function.type in a code_typet and use get_access rather than direct irep access.

thk123 · 2018-02-16T15:13:24Z

src/goto-programs/convert_nondet.cpp

@@ -34,7 +34,7 @@ static goto_programt::targett insert_nondet_init_code(
  const goto_programt::targett &target,


Nit: typo in commit "Fix java harness for main()"

argument to the main() functio

(function)

thk123 · 2018-02-16T15:21:16Z

src/java_bytecode/java_entry_point.cpp

-      !assume_init_pointers_not_null && !is_main && !is_this;
+    object_factory_parameterst parameters = object_factory_parameters;
+    if(assume_init_pointers_not_null || is_main || is_this)
+      parameters.max_nonnull_tree_depth = 1;


If it is_main doesn't this want to be 2?

I see this is fixed in a later commit

thk123 · 2018-02-16T15:24:21Z

regression/cbmc-java/main-args-elements-non-null3/Main.java

+  public static void main(String[] args)
+  {
+    if(args.length>0)
+      assert(args[0] == null); // must fail


Not sure what this test tests that the first test doesn't?

thk123 · 2018-02-16T15:31:09Z

src/java_bytecode/java_types.cpp

@@ -273,7 +273,7 @@ std::string gather_full_class_name(const std::string &src)

  class_name = erase_type_arguments(class_name);

-  std::replace(class_name.begin(), class_name.end(), '.', '$');
+  std::replace(class_name.begin(), class_name.end(), '$', '.');


I need to verify this more carefully - but the reason for it being this way round is to get inner inner classes being represented in a specific manner. The example in your commit message is not a valid java bytecode type descriptor by my reading of 4.2.1

thk123

Critical comments from previous review addressed - could you dismiss this if you think it requires a full re-review (looks similar enough to me)

thk123 · 2018-02-28T13:01:05Z

src/java_bytecode/java_entry_point.cpp

    bool has_correct_type=
      to_code_type(function.type).return_type().id()==ID_empty &&
      (!to_code_type(function.type).has_this()) &&
      parameters.size()==1 &&
      parameters[0].type().full_eq(string_array_type);
-    is_main=(named_main && has_correct_type);
+    bool public_access = to_code_type(function.type).get_access() == ID_public;


Nit: you've already done a to_code_type on function.type (twice) so might as well put it out into a local var

peterschrammel · 2018-03-08T00:00:40Z

@smowton, ready for re-review.

allow_null only considered the immediate pointer, but did not allow forcing sub-objects to be non-null. This is required for example to ensure the array elements of the argument to the main() function to be non-null. The depth argument starts from 1 now to allow the immediate pointer to be maybe null when max_nonnull_tree_depth is 0.

peterschrammel · 2018-06-10T21:56:25Z

TG bump is passing

9441a92 Merge pull request diffblue#2317 from tautschnig/c++-attributes-lists cad7b3a Merge pull request diffblue#2297 from romainbrenguier/bugfix/starts-with 7a6277d Reformat documentation without latex 0c56151 Add test for StartsWith d599dfc Allow duplicate instantiations of the same constant string 6763669 Correct starts_with for offset out of bound case 71f80e1 Deprecates add_axioms_for_is_suffix 8ee1c16 Merge pull request diffblue#2340 from tautschnig/c++-cassert 39a5631 Enabled failed-tests output in cbmc-cpp fafe4d9 C++ front-end: support =delete method declarations e3de3f6 Re-enable access control checks df85911 Fix access in test b092a13 char16_t and char32_t are typedefs in Visual Studio 1e00fcf Default to C++14 as language standard accepted by the C++ front-end on Windows 61ec7fc Merge pull request diffblue#2331 from diffblue/arch_flags_tests 8b2fc41 mark gcc tests as 'gcc-only' to prevent execution by goto-cl on Windows ebf7c7e fix return values of __builtin_classify_type 57ed2bc fix gcc_attributes10 2796025 Merge pull request diffblue#2329 from diffblue/msvc_packed_union 37c0b83 Merge pull request diffblue#2309 from qaphla/regression be6f3c9 Merge pull request diffblue#2346 from peterschrammel/fix-class-models-nondet d49ea09 Added an initial set of tests for contracts, which (expectedly) either fail or will need to be redone once the new flags are added in. d17c990 Merge pull request diffblue#2321 from tautschnig/vs-temporary-filet 43d008a Merge pull request diffblue#2347 from diffblue/smt2-bounds-checks dfff111 Merge pull request diffblue#2348 from tautschnig/c++-block-pointer 1d93fa1 Visual Studio packs bit-fields differently bffb1ca smt2_parser: avoid access to vector without prior size check e6d76e5 Merge pull request diffblue#2349 from tautschnig/document-gcc-req 7d0195a Fix allow-null initialization logic for class models 5a50203 Merge pull request diffblue#2308 from smowton/smowton/feature/must-not-throw-annotation bd74d87 Merge pull request diffblue#2343 from tautschnig/c++-auto d08a75a Document the required GCC/G++ version as >= 5.0 612fc38 C++ front-end: Type check Apple block pointers 278e506 Merge pull request diffblue#2345 from tautschnig/c++-array-ini af83568 C++11 auto type specifier 24ba2a0 Tests for proper pre-C++11 handling of "auto" 830c1d8 Revert "parse C++11 auto declarations" f3a3e79 Merge pull request diffblue#2344 from tautschnig/c++-vs-enum ce4884e C++ front-end: maintain #array_ini flag 19cfa50 Visual Studio supports C11 _Alignof e0d56da Support Visual Studio's forward enum declarations ab60852 Add org.cprover.MustNotThrow method attribute 5b8897e Merge pull request diffblue#2342 from tautschnig/constructor 12e8f46 Merge pull request diffblue#2341 from tautschnig/c++-qualified bc568b7 Only parameter-free constructors can be static initializer functions 57a14b0 C++ front-end: qualified template specialisation can just be accepted bcf8e61 Use temporary_filet for automatic resource management 1d95ab4 Permit compound literals in place of PODs e229b4c Typecheck initializer lists 999ad15 Swap order of subtypes in construction of merged_type nodes 4a47de6 Mark already-typechecked types as such d5183fb Permit GCC attributes after struct/class in class declaration d82f554 Permit asm post-declarator mixed in any order with other qualifiers fde09ca C++ front-end: parse GCC attributes 1f9deb3 Merge pull request diffblue#2333 from tautschnig/reduce-test-memory-footprint 04a8c35 Merge pull request diffblue#2334 from tautschnig/c++-virtual 0216dbd Merge pull request diffblue#2336 from tautschnig/c++-pointer-to-member 73d688d Merge pull request diffblue#2270 from peterschrammel/fix-stub-identifiers 13a1afc Merge pull request diffblue#2338 from tautschnig/c++-enum-operator 4ff6d5c Merge pull request diffblue#2337 from tautschnig/c++-enum-class 21bbecc Reduce memory cost of test by using a scalar variable instead of an array 439d6d3 Merge pull request diffblue#2332 from diffblue/goto-cc-warning-syntax a8f9fd9 C++ front-end: support pointer to non-method members 2f34833 C++ operator overload over enum tag types 4637f87 Fix virtual table construction f3550ea Cleanup: is_virtual is trivally true in this context a172c34 C++ virtual tables: fix inconsistent string suffixes ec5425e Code cleanup a7502c9 C++: support enum class 9e9f251 Prefix identifiers in stubs with function name 774060b Merge pull request diffblue#1768 from peterschrammel/fix-java-main-harness 3cb8bcf Deduplicate string tests 9b19015 Fix tests with incorrect main methods b047091 Simplify main method detection for Java b726dd1 Add regression tests for initialization of Java main args 7348c74 Elements of String array argument to Java main cannot be null 751c040 Simplify check whether String model is present 7a3a07f fix test result for goto-cl 8f2a82e Generalize allow_null to max_nonnull_tree_depth bbe8cca Java main method must be public 86b143b Merge pull request diffblue#2316 from tautschnig/ssa-perf-fix a6d32eb Merge pull request diffblue#2323 from tautschnig/vs-float 86687f7 Fix typos in doxygen f2ec10e Merge pull request diffblue#2320 from tautschnig/vs-return-type 0f2cc3a Merge pull request diffblue#2330 from diffblue/msvc-utf8 bdd5bbb ask CL preprocessor for UTF-8 output 1df3b9d Merge pull request diffblue#2325 from tautschnig/vs-empty-files ecee38d Remove useless cpp files ae1d039 Merge pull request diffblue#2322 from tautschnig/vs-cstring aeafc49 Merge pull request diffblue#2311 from diffblue/aws-codebuild-windows d4cd32d AWS codebuild buildspec for Windows 2c21295 missing dependency in Makefile 3fcdae1 Merge pull request diffblue#2319 from tautschnig/vs-linker-warning 6c22191 Merge pull request diffblue#2312 from diffblue/missing-iterator-headers 6a16f85 Merge pull request diffblue#2324 from tautschnig/vs-big-int-copyright d9a2339 Merge pull request diffblue#2327 from mre/patch-1 363291a Fix typo 8d6335a big-int copyright line c15f47f Mark floating-point constants as float 7e03746 Avoid using C string functions 3e8eff4 Fix the return type to match the class member types 1cb3d4d Avoid Visual Studio linker warning 33787ed missing <iterator> header 223d872 Revert undocumented change of 27153d1 63acc5b Merge pull request diffblue#2303 from smowton/smowton/fix/initialize-before-class-literal-init f927ae9 Merge pull request diffblue#2313 from smowton/smowton/admin/coverity-travis 6982f86 Improve coverity Travis build 894a20f Merge pull request diffblue#2294 from tautschnig/c++-built-ins 4edecbc Rename add_cprover_X_library to cprover_X_library_factory 1201ffe C++ front-end: Use C factory for compiler builtins 0451f1e C++ front-end now has its own library ed05d3e Refactor add_cprover_library to make parts re-usable by the C++ front-end 0ea6143 Make link_to_library independent of the C front-end c8702ab CPROVER library linking: move status message to front-end c471f72 jdiff: remove C library d597d90 Remove unused include 6877b21 Merge pull request diffblue#2305 from tautschnig/c++-operator da5ce90 Fix operator parsing 0d04f37 Merge pull request diffblue#2239 from mgudemann/bugfix/generics/fix_infinite_recursion 2e83ec9 Zero-initialize Class literals before calling initializer function b7725b8 Merge pull request diffblue#2306 from tautschnig/c++-qualifiers 0612749 Merge pull request diffblue#2304 from tautschnig/appveyor-warnings e54bba2 Merge pull request diffblue#2293 from tautschnig/c++-decltype-bit-field d196cf7 Add regression test for recursive generic-parameters 934c555 Do not lose method qualifiers d7b1572 Doxygen update 2d9970c Clarify and correct 04565b4 Un-deprecate to_integer(constant_exprt) feb59ab Use not-as-deprecated version of to_integer e23a1bb Avoid deprecated code_typet() constructor aef48c2 Avoid implicit cast int -> bool c5de7ba Merge pull request diffblue#2296 from smowton/smowton/fix/restore-float128 8c08946 decltype(bit field type) is the underlying subtype 9160e99 Merge pull request diffblue#2292 from tautschnig/c++-windows 7b61482 Extend cbmc ts18661 test 4180e65 Add test for gcc-5 b46e4bf Improve gcc-4 and -7 tests b0d1f9e Restore _Float128 support by default 22b9182 Merge pull request diffblue#2165 from tautschnig/interpreter-member-offset 5fd18a9 Enable C++ regression tests on AppVeyor 8d86e44 Prevent regression failures of cpp tests on windows 9adf5f1 Configure C++ language standard in goto-cl 10a4685 Merge pull request diffblue#2219 from tautschnig/nondet-initializer e12cb04 Merge pull request diffblue#2298 from tautschnig/move-printf_formatter 71c1227 Merge pull request diffblue#2299 from tautschnig/no-c_qualifier 339fcbd Merge pull request diffblue#2300 from tautschnig/no-c_typecast 0a77ce0 Do not use c_qualifiers on goto-program expressions d089ddd Do not use c_typecast in pointer-analysis 60ab7ec Array/vector sizes can be size_t 4031eac Non-negative array/vector sizes are invariants cf41a88 nondet_initializer to build deep non-deterministic expressions 626fb98 Rename zero_initializer to expr_initializer in preparation of generalisation bc15b1b Move zero_initializer to util 7716f3f Remove unused include cc23b20 Move printf_formatter to goto-programs 2ed63f5 Merge pull request diffblue#2156 from tautschnig/gcc-8-fixes 260156f Merge pull request diffblue#2288 from peterschrammel/code-type-const 2bea6fc Merge pull request diffblue#2274 from peterschrammel/travis-new-doxygen c6cfb02 Merge pull request diffblue#2291 from tautschnig/c++-fixes-1 80112d8 Make CMake regression test set match the Makefile one 63c5a32 Install doxygen 1.8.14 on travis 1bd942f Remove redundant invariants 11005ec Remove duplicate save_scope fc670b5 Do not lint .h files in regression/ 763d4d1 Style improvements 204c60f Failing regression test from diffblue#933 1132562 Failing regression test from diffblue#661 fe8ef6d Whitespace cleanup, comment type fixed 5bb13db Initial set of mini-system-c tests 3564324 Line break 402b29b Fix broken comment frame 8480d96 Fix command-line option syntax a3a4696 Fix syntax errors in C++ regression tests f2c60cf Do not use assert without prior declaration 7c053bf Merge pull request diffblue#2290 from diffblue/flt_rounds 4a7a389 Merge pull request diffblue#2262 from karkhaz/kk-rm-noop-depth-lookup 43b41a4 Simplify return f6586ed Rename functions to `get_recursively_instantiated_type` b0fde14 Doxygen update, clarification 8b4920e Return input pointer_type in case of no instantiation 05ff12d Clarifications and corrections 2c5e0b8 Return bound if no concrete instantiation is found 26e5433 Add unit test for mutually recursive generic parameters 6ff2993 Choose mapped-to type when doing higher depth search 31004f5 Search through stack for instantiation 3264023 Fix Typo 258e3ae Track recursion for generic type parameter definition 7360696 Use `std::vector` instead of `std::stack` 8f094e2 added model for FreeBSD __flt_rounds 98379b3 Interpreter: simplify code by not using member_offset_iterator 64cd733 Make code_typet declarations const 6d5e446 Merge pull request diffblue#2240 from diffblue/get-gcc-version b618d94 Merge pull request diffblue#2269 from peterschrammel/parameters-code-type 2a72bf2 Merge pull request diffblue#2268 from allredj/trigger-testgen 78794e2 undo parts of diffblue#2185 e040723 _FloatX support based on gcc version cd6ecec goto-cc now reports version of installed gcc fd910a7 added gcc_versiont 09a4e6c run() can now redirect stderr 32fd0c2 Return original type instead of nil in original_return_type 29bf299 Test for incomplete code_typet construction 05a5efb Use the two-param code_typet constructor 103c7b7 Add missing module definitions 724a36c Add two-param code_typet constructors and deprecate the default one 63a5131 Make sure code_typet is fully constructed 61b9647 Revert 0b3170d: Stabilize clinit wrapper function type parameters da34ceb Merge pull request diffblue#2283 from tautschnig/appveyor-fix 4d70915 Merge pull request diffblue#2279 from diffblue/void-star-arithmetic d668583 Merge pull request diffblue#2282 from diffblue/unused-lambda-capture 2a2907e Unstall AppVeyor by checking for the correct file path 7bad913 the 'this' capture is not used d24f773 Merge pull request diffblue#2233 from thomasspriggs/global_null_message_handler 690613d Merge pull request diffblue#2275 from tautschnig/gcc-case-range e8ff243 Merge pull request diffblue#2225 from cesaro/extended-java-models 5242dc9 Merge pull request diffblue#2265 from smowton/smowton/fix/dont-advertise-ignored-methods 6eab2f9 document why sizeof(void) works 690d10b Merge pull request diffblue#1956 from romainbrenguier/refactor/prop_conv_straightforward2 fc33598 Implement GCC's switch-case ranges e8d26ae Merge pull request diffblue#2267 from LAJW/lajw/always-load-cprover-nondet-initialize c6d2dba JBMC: Added java-models-library dependency e5f3c41 Use a reference with exception types that use vtables 7211280 Silence spurious GCC 8 warning 0c00835 Do not use parentheses around the declared symbol 4f3c102 Silence Minisat's use of realloc on non-POD and fix and use its xrealloc 3082d9d Merge pull request diffblue#2029 from tautschnig/remove-asm c14677b Java frontend: don't advertise ignored methods f8df76a Merge pull request diffblue#2276 from tautschnig/c-string-zero bb1bae9 Merge pull request diffblue#2184 from tautschnig/human-readable-output d35c2ac Refactoring in boolbvt::convert_byte_extract 523f8ae Zero-length C string operations should not yield pointer checks a673e5d Add test verifying that the cproverNondetInitialize method is always loaded 4d67ed5 goto-instrument: Remove inline asm before doing various operations 6f51513 Print (at debug level) the current SSA step being converted b0fce60 Print (at debug level) the size of assignments during symex e515f26 List all candidate functions for a function pointer at debug verbosity 9717af2 messaget helper to encapsulate if(debug-verbosity) { complex output } e698be9 Cleanup: use most suitable symbol_exprt constructor 07ef32d remove_const_function_pointerst::functionst only holds symbol expressions 75f021c Print current depth in BMC progress debug logging 65f0ec0 Provide a source location when analysis finds constness is lost 6f72d9b Split binary string in plain-text output of goto trace in groups of 8 0ff1384 Remove unused local variable e05dad5 Clang format include order. 8e20ac6 Use global `null_message_handlert` instead of duplicates. dab421c Add global instance of `null_message_handlert` 1a4fc92 Merge pull request diffblue#2089 from tautschnig/remove-skip-cleanup 971a34b Always load cprover-nondet-initialize d58eeb4 Add webhook to invoke a Diffblue-specific function 1b43ee9 Refactoring in boolbvt::convert_bitwise adc2d5d Make convert_abs take an abs_exprt parameter b837b8a Remove useless throws in boolbvt::convert_index 52d0fe4 Make build_offset_map return an offset_mapt 2dc7bee Replacing throws by invariants in boolbv convert 15ce938 Enable remove_skip to soundly remove skips with labels 3f34c1a Explicitly invoke goto_program.update() where remove_skip is not used 6bac80e Run remove_skip in passes that may introduce skips 533775c Remove redundant calls to compute_{location,loop}_numbers e9cdffd remove_skip includes goto_{program,functions}.update(), avoid redundant calls cfb733a Make remove_skip call goto_program.update() 91d47c2 remove_skip implementation restricted to a range of instructions 41d38bc Remove unused includes of remove_skip.h c9ead2c Avoid redundant calls to remove_skip 6298c18 Fix wrong function description 9e355e9 Use make_skip to turn an instruction into a SKIP b055179 Relax test: there need not be any code at the end of the block to cover f1a5d6a Make functions non-empty so that the test remains stable under skip cleanup 1bd4f04 JBMC: Minor fix, removing superfluous padding from converter b5ebe6b Remove string lookups from goto_symext main loop e77cabc Remove optionst member from goto_symext git-subtree-dir: cbmc git-subtree-split: 9441a92

peterschrammel requested review from cesaro, kroening, mgudemann, smowton, tautschnig and thk123 as code owners January 26, 2018 01:12

peterschrammel added the do not merge label Jan 26, 2018

peterschrammel requested a review from romainbrenguier January 26, 2018 01:13

romainbrenguier approved these changes Jan 26, 2018

View reviewed changes

smowton reviewed Jan 26, 2018

View reviewed changes

peterschrammel mentioned this pull request Feb 14, 2018

Add support for inheritence of Java static fields. Fixes TG-2457 #1826

Merged

thk123 suggested changes Feb 16, 2018

View reviewed changes

tautschnig assigned peterschrammel Feb 21, 2018

peterschrammel force-pushed the fix-java-main-harness branch from 38d2b1e to eba2914 Compare February 26, 2018 23:50

thk123 approved these changes Feb 28, 2018

View reviewed changes

peterschrammel force-pushed the fix-java-main-harness branch 2 times, most recently from 3b86148 to 4d0f984 Compare March 7, 2018 23:01

peterschrammel removed the do not merge label Mar 7, 2018

smowton approved these changes Mar 8, 2018

View reviewed changes

peterschrammel added the do not merge label Mar 8, 2018

peterschrammel force-pushed the fix-java-main-harness branch from 4d0f984 to 8727c09 Compare March 26, 2018 18:51

peterschrammel added the Java Front End label Apr 28, 2018

peterschrammel force-pushed the fix-java-main-harness branch 2 times, most recently from 8fc4ae5 to 8714235 Compare May 29, 2018 15:43

peterschrammel requested a review from chrisr-diffblue as a code owner May 29, 2018 15:43

Fix typos in doxygen

86687f7

peterschrammel force-pushed the fix-java-main-harness branch from 8714235 to f36ce57 Compare June 10, 2018 10:38

peterschrammel added 2 commits June 10, 2018 11:41

Java main method must be public

bbe8cca

peterschrammel force-pushed the fix-java-main-harness branch 2 times, most recently from fc7a95c to 95e1d9e Compare June 10, 2018 17:04

peterschrammel mentioned this pull request Jun 10, 2018

Reduce redundancy between jbmc-string and strings-smoke-tests #2022

Closed

24 tasks

peterschrammel added bugfix and removed do not merge labels Jun 10, 2018

peterschrammel force-pushed the fix-java-main-harness branch from 95e1d9e to cb0a5a1 Compare June 10, 2018 17:21

peterschrammel added 6 commits June 10, 2018 23:03

Simplify check whether String model is present

751c040

Elements of String array argument to Java main cannot be null

7348c74

Add regression tests for initialization of Java main args

b726dd1

Simplify main method detection for Java

b047091

Fix tests with incorrect main methods

9b19015

Deduplicate string tests

3cb8bcf

peterschrammel force-pushed the fix-java-main-harness branch from cb0a5a1 to 3cb8bcf Compare June 10, 2018 22:05

peterschrammel merged commit 774060b into diffblue:develop Jun 10, 2018

peterschrammel deleted the fix-java-main-harness branch June 10, 2018 22:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix java harness for main() #1768

Fix java harness for main() #1768

peterschrammel commented Jan 26, 2018 •

edited

Loading

romainbrenguier Jan 26, 2018

romainbrenguier Jan 26, 2018

romainbrenguier Jan 26, 2018

smowton left a comment

smowton Jan 26, 2018

smowton Jan 26, 2018

smowton Jan 26, 2018

smowton Jan 26, 2018

smowton Jan 26, 2018

thk123 left a comment

thk123 Feb 16, 2018

thk123 Feb 16, 2018

thk123 Feb 16, 2018

thk123 Feb 16, 2018

thk123 Feb 16, 2018

thk123 Feb 16, 2018

thk123 left a comment

thk123 Feb 28, 2018

peterschrammel commented Mar 8, 2018

peterschrammel commented Jun 10, 2018

		@@ -34,7 +34,7 @@ static goto_programt::targett insert_nondet_init_code(
		const goto_programt::targett &target,

Fix java harness for main() #1768

Fix java harness for main() #1768

Conversation

peterschrammel commented Jan 26, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented Mar 8, 2018

peterschrammel commented Jun 10, 2018

peterschrammel commented Jan 26, 2018 •

edited

Loading