Cause a regeneration of the _start method if a --function is provided #338
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
This isn't complete as at the moment as we call |
thk123
commented
Dec 7, 2016
src/cbmc/cbmc_parse_options.cpp
Outdated
| if(cmdline.isset("function")) | ||
| { | ||
| const symbolt &desired_entry_function= | ||
| symbol_table.lookup(cmdline.get_value("function")); |
There was a problem hiding this comment.
Make more robust to invalid input
src/cbmc/cbmc_parse_options.cpp
Outdated
| @@ -690,6 +692,20 @@ int cbmc_parse_optionst::get_goto_program( | |||
| return 6; | |||
| } | |||
|
|
|||
|
|
|||
| // All input files were binary | |||
| if(cmdline.isset("function")) | |||
There was a problem hiding this comment.
Should this be done if no binaries? It isn't needed but also doesn't harm.
thk123
commented
Dec 7, 2016
src/cbmc/cbmc_parse_options.cpp
Outdated
| @@ -690,6 +692,20 @@ int cbmc_parse_optionst::get_goto_program( | |||
| return 6; | |||
| } | |||
|
|
|||
|
|
|||
| // All input files were binary | |||
There was a problem hiding this comment.
This comment is just wrong.
|
There is a lot of common code between I won't do that for this PR but should create an issue to do this as would make this more straight forward. |
thk123
force-pushed
the
bug/function-flag-on-goto-program
branch
from
fb95b52
to
a5c32dd
Compare
|
@tautschnig I'd appreciate your feedback on this. It isn't quire ready to be merged as it needs some regression tests. Also I haven't had much luck testing this works with Java as whenever I try to run a Java program through either goto-cc or cbmc with a |
|
@thk123, goto-cc does not work for java. So, we can ignore this aspect for the time being. |
|
@thk123, can you please add a few tests? |
|
@peterschrammel I have added tests. I also checked that it fixed #176 (it does). |
thk123
force-pushed
the
bug/function-flag-on-goto-program
branch
from
a187164
to
8ea248a
Compare
|
This PR is "dependent" on #343 and should not be merged until that PR is. |
tautschnig
requested changes
Dec 11, 2016
src/ansi-c/ansi_c_entry_point.cpp
Outdated
| @@ -519,3 +551,4 @@ bool ansi_c_entry_point( | |||
|
|
|||
| return false; | |||
| } | |||
|
|
|||
There was a problem hiding this comment.
Don't add blank lines at the end of files.
| @@ -291,7 +321,7 @@ bool ansi_c_entry_point( | |||
| const code_typet::parameterst ¶meters= | |||
| to_code_type(symbol.type).parameters(); | |||
|
|
|||
| if(symbol.name==standard_main) | |||
| if(symbol.name==ID_main) | |||
There was a problem hiding this comment.
What is the rationale for this change?
There was a problem hiding this comment.
Then I'd suggest to also drop standard_main completely from the codebase. Could you please add a commit doing so?
There was a problem hiding this comment.
Yes, the use use of the standard_main parameter looks a bit dodgy. The only places where it is used are in src/cpp/cpp_language.cpp and src/goto-cc/compile.cpp, and there "main" is passed... So, it's not entirely clear why this parameter is needed at all.
src/cbmc/cbmc_parse_options.cpp
Outdated
| if(desired_entry_function!=symbol_table.symbols.end()) | ||
| { | ||
| languaget *language=get_language_from_mode( | ||
| desired_entry_function->second.mode); |
There was a problem hiding this comment.
assert or even throw if language is null.
There was a problem hiding this comment.
Addressed this in new location - rebuild_goto_start_functiont::operator()
src/cbmc/cbmc_parse_options.cpp
Outdated
| { | ||
| languaget *language=get_language_from_mode( | ||
| desired_entry_function->second.mode); | ||
| language->regenerate_start_function( |
There was a problem hiding this comment.
@kroening Am I right that language should be wrapped in a unique_ptr here as that would be a memory leak?
There was a problem hiding this comment.
I have swapped to using unique_ptr as that seems to communicate intent clearer. However, if is potential memory leak otherwise, I think get_language_from_mode has a misleading name (get to me certainly doesn't suggest creating a new object. This code is now in rebuild_goto_start_functiont::operator()
| @@ -57,6 +57,16 @@ void java_bytecode_languaget::modules_provided(std::set<std::string> &modules) | |||
| // modules.insert(translation_unit(parse_path)); | |||
| } | |||
|
|
|||
| bool java_bytecode_languaget::generate_start_function( | |||
There was a problem hiding this comment.
Please insert a comment header
src/util/language.cpp
Outdated
| #include <util/config.h> | ||
| #include <util/symbol.h> | ||
| #include <util/symbol_table.h> | ||
| #include <goto-programs/goto_functions.h> |
There was a problem hiding this comment.
This seems scary: util should not depend on goto programs in any way. Also, the other headers should just be "config.h" etc.
src/util/language.cpp
Outdated
| // Implement in derived languagets | ||
| assert(0); | ||
| return true; | ||
| } |
There was a problem hiding this comment.
Maybe this is a lazy cop-out but I didn't make it abstract as don't know how to provide implementations for some of the languages. I could make it abstract and provide a stub method that asserts in the derived?
There was a problem hiding this comment.
Yes, please copy&paste this into the deriving languages. This forces people adding a new language to think about it, while the current implementation would hide that matter.
src/util/language.cpp
Outdated
| } | ||
|
|
||
| return return_code; | ||
| } |
There was a problem hiding this comment.
I'm sorry, this can't live in util/ - that should be in one of linking or goto-programs.
thk123
force-pushed
the
bug/function-flag-on-goto-program
branch
3 times, most recently
from
c7994d4
to
d9bc65b
Compare
|
@tautschnig I believe I have addressed all your feedback. |
tautschnig
requested changes
Dec 12, 2016
src/cpp/cpp_language.cpp
Outdated
| { | ||
| // Implement in derived languagets | ||
| assert(0); | ||
| return true; |
There was a problem hiding this comment.
The comment above no longer fits; and most likely you should just invoke the code from ansi-c in the cpp case.
| @@ -0,0 +1,95 @@ | |||
| /*******************************************************************\ | |||
| Module: C Test Case Generator | |||
There was a problem hiding this comment.
Is that really the appropriate module? It doesn't seem to be an accurate description now.
| function again. | ||
|
|
||
| \*******************************************************************/ | ||
| bool rebuild_goto_start_functiont::operator()(const std::string entry_function) |
There was a problem hiding this comment.
The parameter type should be const irep_idt&
| auto language= | ||
| std::unique_ptr<languaget>( | ||
| get_language_from_mode( | ||
| desired_entry_function->second.mode)); |
There was a problem hiding this comment.
@kroening: Please review/comment whether what I had suggested is actually necessary.
There was a problem hiding this comment.
@tautschnig, to which suggestion are you referring?
There was a problem hiding this comment.
@peterschrammel I believe @tautschnig is referring to this comment: #338 (comment)
Am I right that language should be wrapped in a
unique_ptrhere as that would be a memory leak?
Interestingly this causes Jenkins to not compile under clang, I'm hoping because I missed a #include <memory> at the top of the file, just checking now.
There was a problem hiding this comment.
Including memory has fixed this compile error.
| if(desired_entry_function==symbol_table.symbols.end()) | ||
| { | ||
| error() << "main symbol `" << entry_function; | ||
| error() << "' not found" << messaget::eom; |
There was a problem hiding this comment.
I believe eom (without the extra messaget::) should suffice here, as this class inherits from messaget.
| #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H | ||
|
|
||
| #include <util/message.h> | ||
| #include <util/symbol_table.h> |
There was a problem hiding this comment.
Nit picking a forward declaration class symbol_tablet; would suffice here.
There was a problem hiding this comment.
I agree, however @peterschrammel said in a different review to prefer includes to forward declarations. Perhaps this should be added to the coding standards (whichever way we choose).
There was a problem hiding this comment.
@thk123 I don't think I have access to that discussion, so I'd appreciate if you could email it to me or share in some other way. My views in this area is largely guided by "Large-scale C++ Software Design" by John Lakos. Whichever way the decision goes: yes, this should go in the coding standards.
There was a problem hiding this comment.
Not much said, @peterschrammel said he would discuss this with you, but the gist of Peter's position is using includes everywhere it better than mixing includes when necessary with forward declarations.
There was a problem hiding this comment.
Unfortunately I don't have access to the book at the moment, but http://www.umich.edu/~eecs381/handouts/IncompleteDeclarations.pdf has some discussion.
My main concern/argument in favour of forward declarations is compile time, because of reduced number of dependencies (in incremental builds) and fewer files having to be opened and parsed.
src/util/language.cpp
Outdated
| @@ -8,6 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com | |||
|
|
|||
| #include "language.h" | |||
| #include "expr.h" | |||
| #include <util/config.h> | |||
| #include <util/symbol.h> | |||
| #include <util/symbol_table.h> | |||
There was a problem hiding this comment.
Additional includes when there is no change to the code?
thk123
force-pushed
the
bug/function-flag-on-goto-program
branch
2 times, most recently
from
68dee7b
to
d3d1705
Compare
|
@tautschnig Save the question about forward declarations I have addressed these, apologies for the embarrassing copy/paste errors. For the "real" diff you can go here: https://github.com/diffblue/cbmc/pull/338/files/bf778a559a5a4b2f54c1deca2efdf902d72d0538..d3d1705e2f47c02dac5cadd876d791e3a77b41fd |
|
@mgudemann Comments addressed - will squash when I do a rebase. |
added 10 commits
September 13, 2017 13:37
If the user provides a --function argument, tell the languaget to regenerate the entry function to call this function. Previously if the program had been precompiled (using goto-cc), the start function that was used in the original generation would be used again meaning the --function argument was ignored. Removed erroneous comment
Check the symbol actually exists before trying to regenerate the _start function.
Rather than calling the final method, call a refactored out method that is just responsible for generating the _start body.
As with the ANSI C version, the Java version undergoes a simmilar refactor: splitting out the start generation from final so that it can be regenerated on demand. 2 The entry function in Java now has some parameters that need to passed to it. Since they are member variables in the java_bytecode_langauge they can just be passed in from the virtual regenerate call.
Ensure that despite the prescence of a main method being compiled as the entry point, we can still override it using --function in CBMC.
Moved the function for discarding the symbol and GOTO function and calling the languaget::generate_start_function into a class in goto- programs. This was done as util should not depend on goto-programs.
Made the generat_start_function abstract to ensure new langugages are at least aware they should provide implemention for this method. CPP and JSIL languages have stub method that asserts for now.
Rather than have a parameter which specifies the entry function, use the appropriate ID. This saves having three seperate places with the string "main" hard coded.
Clang warns for files that inconsistently use the override keyword so added the missing ones to jsil_language.
thk123
force-pushed
the
bug/function-flag-on-goto-program
branch
2 times, most recently
from
66c3f2b
to
26ddfcc
Compare
mgudemann
approved these changes
Sep 13, 2017
added 6 commits
September 13, 2017 14:52
symex and goto-analyze (through the goto_modelt class) now support setting the --function flag on precompiled .gb files. Refactored out the function flag and its help function to rebuild_goto_start_functions. Used this extracted flag in goto-analyze, symex and CBMC. Added tests that check both goto-analyze and symex when ran with the --function flag actually generate the correct _start function. Also added tests for when it isn't a precompiled binary. Added these new folders to the overal test suite
The java bytecode entry point relied on things working a little differently. Firstly, the function name is transformed to allow simpler function names to be passed in. As such the rebuild_entry_point cannot be responsible for looking up the symbol. This in turn involved a new way of identifying the mode to use (using the existing entry points mode) Secondly, as the lanuages are destroyed after the parsing phase, we must re-provide the message handler as this is used by the entry point generation. Finally, the java_bytecode_entry_point adds a new symbol to the symbol table, so we remove all symbols that are in the scope of the original entry point.
As we now regenerate the entry point, variable names have changed. This means these tests don't fail for this.
thk123
force-pushed
the
bug/function-flag-on-goto-program
branch
from
26ddfcc
to
2d006cb
Compare
thk123
force-pushed
the
bug/function-flag-on-goto-program
branch
from
2d006cb
to
22f06fd
Compare
peterschrammel
approved these changes
Sep 14, 2017
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
08f269c Merge pull request diffblue#1388 from smowton/merge-develop-20170914 e3f3abd Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914 4df244c Merge pull request diffblue#1383 from reuk/reuk/sync-projects f25db0a Merge pull request diffblue#189 from diffblue/smowton/fix/remove_debug_code 1fae64c Remove stray use of overlay_map 1264b4d Re-enable old function signatures for test-gen compat e54c0e9 Merge pull request diffblue#338 from thk123/bug/function-flag-on-goto-program 63c9a1e Merge pull request diffblue#1374 from reuk/reuk/maintain-pointer-invariants 00e4555 Fix up CMake build (unrelated) 81f1300 Use PRECONDITION in std_types.h a9806c0 Ensure pointer invariants are maintained a46ad62 Regenerate malformed binary blobs f77822b Merge pull request diffblue#1380 from diffblue/remove-musketeer 22f06fd Correcting windows build 3ede81b Merge pull request diffblue#1293 from reuk/cmake-develop 92a52a5 Corrected doxygen errors c6f1430 Ensure symex and goto-analyzer regenerate functions e37d3d5 Disable failing test in the symex directory 15b89fc Weaked the tests for pointer-function-parameters dee89b0 Fixing the method to work with java_bytecode 1ccd1a2 Add support for using the --function flag to goto-analyze and symex 0732580 Adding missing overrides 71dec3d Use ID_main as the default name for entry function 2aea88d Made generate_start_function abstract f0d6d72 Refactored the regenerate function into goto-programs 71e6800 Added regression test for using --function on a GOTO program 94b7185 Implemented generate_start_function for Java cd416bc Call generate_start_function only when regenerating the start function ee5fb93 Protect against invalid function label 2a3d876 Adding explanatory comment f347a22 Cause a regeneration of the entry method if a --function is provided 69d05a9 Merge pull request diffblue#1382 from pkesseli/bugfix/language-opaque-stubs d45325c Merge pull request diffblue#1378 from thk123/bugfix/fix-symex-appveyor 444f256 Add initial value to languaget::generate_opaque_stubs 91e733d Manually disable some failing tests 41bafc0 Merge pull request diffblue#1375 from pkesseli/bugfix/uncaught-exceptions-invariant a31f1d9 remove musketeer af8d46f Reverting manually commited fixes e73a884 Attempt to fix the symex appveyor build 0496142 Account for replaced functions in exceptions_map 2816b80 revert symex regression until Appvoyer works 6a2fd50 added symex to Appveyor build a2834d0 Map wrappers: forward more of the std::map interface 0a668ae Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2 8cd4490 Merge pull request diffblue#1373 from diffblue/symex-trace-fix 5d2d07b enable symex regression testing 5195d24 avoid confusion between SSA lhs and full lhs during assignment 430218f option is now --trace 746bff5 remove_returns missing in symex 211355d comments on test 3896110 output statements 8fc714d use __CPROVER_assert 728ac5b Merge pull request diffblue#1367 from reuk/reuk/disable-alpine-in-travis 73b4357 Merge pull request diffblue#1339 from diffblue/initialize_goto_model 4febd10 Merge pull request diffblue#1364 from diffblue/phread-create-fix 0cfd7b0 Remove PRE_COMMAND scaffolding 04b4f63 Merge pull request diffblue#186 from diffblue/cleanup/misc 577fa6c Tightened up usage of maps 8782103 Merge pull request diffblue#1365 from smowton/smowton/feature/more_map_forwarding 4dde3c5 Disable glucose in Travis 91684da Clean up CMake files after diffblue#1321 7d4e9b5 Make CMake release flags similar to Makefile build 5ee349f Control SAT library from makefiles ad486f8 Set up glucose externalproject 5afa929 Quote paths in flex/bison commands 9afbced Disable 32-bit builds in Travis d953327 Enable caching for CMake builds (hopefully) 6251055 Fix and refactor library_check target 3c36aa5 Enable CMake in Travis f6e4968 Enable running tests from CMake e609bbb Add CMake howto to COMPILING file 22c2ab9 Add CMakeLists 6facf74 Map wrappers: forward more of the std::map interface b846858 Merge pull request diffblue#1291 from LAJW/optional 3ddd377 clean-out ill-modeled optimization in string comparisons 95c5e63 Disable Alpine in Travis fe60e60 pthread_create arguments null/nonnull fix 7d30cde missing copyright header 8c4ff7b remove spurious references to langapi/language_ui.h e4498ca brief list of symbols, from language_uit fc4d44a use goto_modelt 9469552 use initialize_goto_model in CBMC/goto-analyse/etc 40fe0f8 simplify API of goto_convert 40557df Used range iterators d4e89fd Tidy up symbol_tablet::move c125146 Merge pull request diffblue#1245 from tautschnig/run-diagnostic 435c0bf Merge pull request diffblue#1321 from reuk/reuk/remove-unused-files 08a4077 Make the child process that failed to execvp exit 4928f69 Diagnostic output if run/execve fails 5863a75 Merge pull request diffblue#1333 from tautschnig/remove-c_sizeof 498718f Code readability 2217501 Remove unused files 1c8d81a Merge pull request diffblue#1356 from smowton/smowton/feature/test_pl_add_dry_run 56b5e25 Merge pull request diffblue#1358 from thk123/feature/decrease-message-spam 359a3e3 Modified verbosity for loaded message 296349c Add dry-run mode to test.pl f6d94cf clean out an unused method 3613ebc When possible, update array types before typechecking initializer 3273bf5 Fix type casts from initializer lists to arrays of unspecified size 1fa569f sizeof(*(void*)) is sizeof(char) d79067e Remove long-deprecated c_sizeof in favour of size_of_expr et al. 254f133 Merge pull request diffblue#1323 from janmroczkowski/janmroczkowski/goto_modelt-output-const 388a25e Make uncaught_exceptions_analysis.output const 211fcc2 Make path_nodet.output const 9be84ea Make automatont.output const 567eaa7 Make basic_blockst.output const ebbbf5f Make goto_modelt.output const ae584df Move optional unit tests into util directory 4dbf939 Manually fix optional 43d0602 Add unit tests for nonstd::optional 8584bb0 Add nonstd/optional.hpp library 281e384 Workaround for travis performing shallow clones with wrong branch git-subtree-dir: cbmc git-subtree-split: 08f269c
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
cc8db21 Merge pull request diffblue#367 from diffblue/allredj/optional-test-runner-timeout 54f278e Merge pull request diffblue#355 from diffblue/allredj/string-exceptions 80e17d8 Add tests for StringBuffer exceptions 50fe786 Add tests for StringBuilder exceptions 403bb47 Add tests for String exceptions 5f20fa8 Add exceptions to String models f06c5dd Merge pull request diffblue#353 from diffblue/allredj/SecureRandom 2357fb1 TestRunner: Set global process timeout to 500 secs a1e9bc0 TestRunner: Add optional timeout d2d0e1e TestRunner: Prevent deadlock on output streams 8c2f6ec Merge pull request diffblue#363 from diffblue/antonia/public-static-fields b0d1038 Allow custom javadoc tags in all places in models 91b51cb Add new restriction on static fields to readme 5d5237b Update 'Writing models' section in readme cea6f14 Model for SecureRandom 53b572b Force SecureRandom mock in TestRunner 1c50faa Empty Random and SecureRandom models 7653be1 Import Random and SecureRandom from JDK 79d7e50 Update File javadoc to take bugs into account 0bd4ffb Add tests for File fields 5f714c8 Prepare File.spec for new test format 419bb11 Enable public static fields in File and String ac47de9 Merge pull request diffblue#361 from diffblue/antonia/public-System-fields 31c934c Add tests for public static fields of System 1489356 Prepare existing System tests for new format 2b4f4a8 Re-enable out, in and err fields in System model c8bd0eb Merge pull request diffblue#362 from diffblue/jeannie/DisableTestsDueToTG2098 2b183fa Updates javadocs for java.util.Properties for TG-2098. da777b5 Renames spec files to remove spaces and make consistent. 7005075 Disables tests in java.util.Properties due to TG-2098 5c9652b Merge pull request diffblue#360 from diffblue/antonia/gcloud-comment bbfa9f9 Merge pull request diffblue#354 from diffblue/antonia/model-common-Date-methods 6ddfee0 Add ticket number to commented out gcloud line c2f5bf5 Add @diffblue.mock java tag 8c032d8 Delete legacy Date tests fa15801 Add tests for Date 1f7a722 Mock Date in TestRunner cdd4037 Simple model for Date with constant timestamp e0b859f Copy jdk version of Date af0c931 Merge pull request diffblue#358 from diffblue/allredj/tmp-gcloud-fix 6c3baf8 Temporarily disable GCloud update e188f92 Merge pull request diffblue#349 from diffblue/allredj/gauge-dump-mvn-error-to-stdout d8f016b Gauge: Dump mvn error message into stdout 7137e47 Merge pull request diffblue#324 from diffblue/feature/TG-2020/deeptest-utils-update 216248a Updating runner to use the new deeptest-utils repo 0aeeac3 Merge pull request diffblue#352 from diffblue/allredj/buffered-writer-missing-null-check 67b76b1 Fix missing null check in BufferedWriter's nondet-init b0a3882 Merge pull request diffblue#350 from diffblue/jeannie/DisableSometimesFailingHashtableTest b8cf2df Disables tests that use nondet key/value for Hashtable due to TG-2098. 0714583 Adding a noop for Hashtable tests (no testing scope change). 459a3ce Merge pull request diffblue#337 from diffblue/jeannie/EnableHashtablePropertiesTests 5918596 Enables tests for Properties and Hashtable that require custom initialisers. 8c0b6ab Merge pull request diffblue#348 from diffblue/antonia/disable-TG-2098-tests 1ecfffe Merge pull request diffblue#347 from diffblue/allredj/lower-initial-capacity-bound 8b5e399 Disable test with varying running time 2e75972 Lower max initialCapacity to prevent JVM runtime failures 82cf0a8 Merge pull request diffblue#328 from diffblue/jeannie/Properties 85c5380 Merge pull request diffblue#346 from diffblue/jeannie/DisableFailingTestsDueToTG2356 df669a7 Adds tests for java.util.Properties model. TG-2067 9a840e5 Adds javadocs for java.util.Properties model; TG-2067. b1c480c Adds model for java.util.Properties. TG-2067 546c4b8 Marks all methods as notModelled(). TG-2067 15f7a4f Makes initial commit for Properties.java. TG-2067 453919a Updates javadocs for java.util.Arrays. c054c05 Merge pull request diffblue#345 from diffblue/antonia/mockito-powermock-versions 3b37fe6 Disabling tests that fail due to TG-2356 / TG-1404. ce082f6 Update remaining pom files into new format 57dcf33 Use compatible Mockito and Powermock versions 226fa3e Merge pull request diffblue#340 from diffblue/romain/QA_HashSet_iterator c38cac1 Level1 tests for iterators on HashSets ebd5043 Merge pull request diffblue#344 from diffblue/jeannie/DisableHashSetTests 5b79203 Disables failing tests due to TG-2327. 525a731 Merge pull request diffblue#343 from diffblue/romain/fix-test-clone-arraylist 673792f Deactivate test with HashSet of ArrayList aa1ca7e Merge pull request diffblue#339 from diffblue/jeannie/FixCustomEqualsHashMap acfc29b Merge pull request diffblue#331 from diffblue/romain/regression/TG-1245 7f7d3ff Merge pull request diffblue#335 from diffblue/romain/QA_HashSet_clone 5c9cd0f Disables HashMap test regarding TG-2315. b751a09 Fixes HashMap test regarding TG-2018. 12336a7 Level 1 tests for HashSet.clone 19a38e8 Regression test for TG-1245 (Object.getClass) 992437b Merge pull request diffblue#341 from diffblue/romain/update-class-files 38be638 Correction of a test 6bfc2b2 Forgotten class file 18d1cc0 Merge pull request diffblue#319 from diffblue/romain/QA-HashSet 6ba37d1 Merge pull request diffblue#338 from diffblue/bugfix/TG1877-Bugfix-regressiontest 1d596b2 Merge pull request diffblue#327 from diffblue/jeannie/Hashtable f682e28 Tag long test of HashSet 080b6aa Remove tests duplicating L1Constructor_Collection 89643ba Level 1 test - HashSet constructor and class tests 9f83291 Remove old tests from ArrayList.spec 3822552 Add tests for TG-1877 to the new bug test suite 8a4e6a8 Adds tests for Hashtable. TG-2176 5c3f51d Merge pull request diffblue#326 from diffblue/allredj/Update-test-header-in-TestRunner 72a9f72 Adds model for Hashtable. TG-2176 d56fbbd Marks all methods as notModelled(). TG-2176 4f0a4ae Make initial commit for Hashtable.java and Dictionary.java. TG-2176 3ab91b8 Merge pull request diffblue#336 from diffblue/antonia/disable-Write12-test 5a7e84a Update test headers according to Platform 27cf91b Move maven configs to master-pom.xml 9907cc2 Merge pull request diffblue#332 from diffblue/feature/TG-2020/centralise-artifact-name 910a6a6 Tag ByteArrayOutputStream.Write12 as 'long' 23dde95 Updating POM file to use property in the master-pom 92b1dca Adding a master POM to specify all dependencies in one place 857bd3c Merge pull request diffblue#333 from diffblue/forejtv/remove-some-codeowners a475e10 Merge pull request diffblue#330 from diffblue/allredj/enable-TG-656-tests 25ecdfe Remove forejtv and peterschrammel from code owners 1145774 Merge pull request diffblue#325 from diffblue/antonia/HashMap-inner-classes 326482a Clean up model methods spec file fdf6041 [TG-656] Enable passing exception tests b029c6f Delete old iterator tests 515f163 Add tests for HashMap$Values edbe13f Add tests for HashMap$KeySet 7037882 Add tests for HashMap$EntrySet 4a77660 Override Values.remove() in model 0b8cac8 Improve running time of remove() methods e57e731 Small fixes for null cases in HashMap$EntrySet b411ef3 Merge pull request diffblue#322 from diffblue/antonia/method-body-tests e808809 Merge pull request diffblue#323 from diffblue/romain/script-generalize-test 3f1eb24 Put method body tests into new format e90f611 Update powermock dependencies in new pom.xml ae460cd Create folder for method body Maven project 0ad8972 Move known-bug method body tests to end of file b71f824 Move method body tests into separate file af9f9a5 Merge pull request diffblue#311 from diffblue/allredj/Testrunner-message-on-missing-method 0a70f78 Script specializing method to different types 7f5d25b Improve TestRunner failure messages 4b7c200 Merge pull request diffblue#315 from diffblue/justin/alTestTidyup 9d005ba Addressing review comments progress 2 7fc3602 Merge pull request diffblue#318 from diffblue/allredj/QA-HashMap 4bcc63f Add tests in new format 4c74354 Add constraints on constructors args f623a6a Merge pull request diffblue#321 from diffblue/allredj/add-constraints-on-capacity 0aa1cde Add constraints on constructors args 85da460 Merge pull request diffblue#320 from diffblue/antonia/prevent-Travis-debug-mode-crashes c01c883 Addressing review comments progress 1 f965eae Prevent Travis build crashes with set +e 2f5c657 Add and refactor ArrayList tests into new format a144089 Merge pull request diffblue#317 from diffblue/antonia/disable-ArrayList-test-TG-2098 44b865e Disable ArrayList test affected by TG-2098 950b3cb Merge pull request diffblue#316 from diffblue/antonia/enable-HashSet-tests 52c8aa4 Re-enable HashSet tests for new model/constructor c1ac42a Merge pull request diffblue#308 from diffblue/antonia/model-HashSet-using-array-field 5f1422f Temporarily disable HashSet tests 898eceb Update limits on method calls in HashSet javadoc 0488845 Update HashSet.spec and limits on number of calls 6ba92bd Add test for HashSet.clone() 03013dc Add new HashSet test using Collection constructor 12b741e Model HashSet using an array instead of a HashMap 1e16b87 Merge pull request diffblue#314 from diffblue/lajw/array-list-arrays-tests a333fd5 Add test for ArrayList of Arrays bbbece5 Merge pull request diffblue#312 from diffblue/allredj/testrunner-lush-specs ac16beb Merge pull request diffblue#306 from diffblue/doc/update-string-doc-TG-1724 75934df Merge pull request diffblue#313 from diffblue/allredj/travis-skip-long-future 019806d Skip long and future tests in Travis c15a87e TestRunner: Add functionality to simplify specs dfcfee7 Typo in StringBuilder.java comment 3a84d72 Correcting exception documentation in String.java b573c7a Document support of String(Builder|Buffer) Classes 4756a96 Document missing exception throws in StringBuffer 40bed6f Document missing exception throws in String model 679d3a3 Merge pull request diffblue#307 from diffblue/jeannie/SystemArrayCopyQA 0fc655c Puts tests into QA format for System.arraycopy. 1adfb51 Merge pull request diffblue#310 from diffblue/jeannie/UpdateGitIgnore 0dc376d Removes tika from the .gitignore file because it was removed. 025d1b2 Removes reference to tika tests in .travis.yml file. 0bf6558 Reinstates .gitignore file after conflict during rebase. f574057 Merge pull request diffblue#302 from diffblue/justin/newqascript ecb6d38 Address PR review comments eedf614 Add bash script that automates some QA workflows along with usage instructions fc95298 Merge pull request diffblue#304 from diffblue/test/reactivate-tests-deactivated-by-PR301 f2f6786 Revert "Temporarily deactivate a test" 3b40452 Adds tests for StringBuilder append(Object). These are all currently disabled. 07af9e7 Print more useful output about discarded tests 270457d Print more output about line errors 29defd6 Group java.util import statements in TestRunner 16fa02c Temporarily deactivate a test beab774 Correct test charAt_Fail f9135af Replace charAt occurences by CProverString.charAt 30df36c Use CProverString to model String.substring 16172f9 Use CProverString.charAt to model String.charAt 68675f7 Add a CProverString class to use internal methods 453a262 Use goal coverage in TestRunner "lines" tests dc77ad4 Add doc about travis error report on README 6728da0 Don't fail if report is not present 51f95f4 Enable test that was forgotten in PR 295 cea6c05 Add test for floating point precision of floats in custom initalizers 61fb30c Disables test that was randomly failing CI. TG-1891 d9e2c34 Adds more tests for HashMap with generics. TG-1401 a28c379 Adds documentation for HashMap. 646cdb0 Add tests for generics support of ArrayList 67f99ad Make imports and linebreaks consistent in tests 0678c26 Adds more tests for HashSet, namely for custom initialisers and addAll. c3ee8d3 Adds addAll function separately. Adds documentation. 1fa7e5c Increase Maven compilation speed 66cb693 Factor test verification 2902bac Add error message when bad Maven dir is given 4317579 Compress and save html report on each ML build b660af6 Adding CProver.notModelled calls in StringBuffer 30eaf5f Add diffblue tags to StringBuffer model 34b607b Comment on internal models of StringBuffer methods 2db6dc5 Moving "modelled internally" comments in methods ea1b900 Adding diffblue tags to StringBuilder methods 3d64388 Marking notModelled StringBuilder methods b8d5101 Put original String.contentEquals code in comment d1d074d Correct model of toUpperCase(Locale) 87dea39 Correct comments for String.getChars dcb3183 Add untested and todo tags to overview.html c74e3de Add untested and todo tags to Readme f90ce62 Comment unused imports 0769e20 Commenting out unused private methods 8366ca7 Marking not modelled String methods 772ce3d Adding tags to method documentations 88b4bda Add diffblue.todo and untested tags 16e957e Modify command to increase gauge plugin timeout 05c4d2e Update README.md 8e5e31a Convert "verify" tests to "generate" tests in specs e3fe09d Add steps for test generation only dabdc1a Refactor test verification steps 393eeba Add new Gauge step "Verify Tests in Maven project" 87eb11a Modify spec files for new mvn setup command d8808f7 Modify Maven setup Gauge command 0da5a56 Typo in StringBuilder model e02661c Reintroduce doc and code in StringBuffer model 94a8ebf Reintroduce doc and code in StringBuilder d2b955b Comment about utility functions specific to models 93579f8 Reintroduce String Library documentation and code 54089f8 Enable test verification for BitSet 913ac12 Implements iterator() method for Arrays$ArrayList inner class (Arrays.asList). TG-1727 e08d030 Add test for TG-1786 1fac27d Workaround for bug TG-1786 in HashMap model f9d5b91 Disables BitSet functional test for clear. TG-1775 38dc647 Disables functional test for ArrayList iterator. TG-1775 1a7e4ac Add verification of tests for BitSet c1ff99f Model for BitSet 485339a Adding bitset from JDK 3092f08 Add test for handling user-defined type as an element of ArrayList d93f9a6 verification of tests for DataInputStream efc186b model for DataInputStream 527d82a JDK version of DataInputStream 811689f java.io.DataInput interface from JDK 8287a56 Marking FilterInputStream as supported, and adding cproverNondetInitialize f63aa29 JDK version of FilterInputStream 43808d8 Keep all generated test files a35c96e Add doc to Integer.java fd68471 Add doc to Boolean.java cba6e76 Implements model for Arrays.asList() 7d3c23e Marking methods as notModelled() in Arrays.java. 0b30e9b Initial commit for Arrays class file. 19f106a Disables test with Gauge issue on TravisCI. c5b89f6 Enables tests for HashMap/HashSet as argument or return value. b2bd7f0 Enables tests for HashMap/HashSet as argument or return value. 4468773 Activate ArrayList return value tests c0d9006 Add ArrayList test that checks for side effects aaec548 Comment out custom ArrayList model variable 838f304 Disable test that randomly fails on Travis 9a0f626 Add ArrayList and HashMap constraints for modCount ee6f284 Add tests for return value check of ArrayList 85592d9 Check for "tested" instead of "covered" 92500be Use new platform parameter in TestRunner.java 3399a22 Modify test to match HashSet's NondetInitialize ba008ab Add NondetInitialize constraint to Class model 52880ee Add constraint in HashSet to speed up test gen 37c789a Disable PutAllAndGet.test for HashMap 71fe858 Replace validate for HashSet 27e58e7 Replace validate for HashMap 6ed6a99 Replace validate for ArrayList and AbstractList d38044c Replace validate for BufferedReader and related a2e6cd5 Enable ByteArrayOutputStream's Write12.test 116d10f Replace validate for ByteArrayOutputStream 1c8e115 Enable PrintStream's Depth.test 269bb28 Replace validate for PrintStream + related classes 09fd660 Correct getPrimitiveClass for String 140e8fa Add tests for Class.toString 1bc6127 Correct Class.isPrimitive model 1fe9d8d Adding Java.lang.Math test scenarios. (diffblue#233) 93ec334 Skip a test until models-library#261 is merged da5e93b Enables tests for HashSet that require Float and Double equals(). 928b4e2 Adds tests for equals() in Double and Float models. 020e400 Implements method equals() in Double and Float models. e7b4b1e Add new test for custom class without nested class 08affc8 Rename CustomClass to StaticClass, enable test 933a99a Update TestRunner paths c1c7ed0 Remove redundant test ArrayListObjectToBoolean ebaa2c2 Renamed tests to more informative filenames 80570cb Test for ArrayList argument possibly null e5c0330 Additional tests for ArrayList as argument TG-1230 79e86ab Address TODOs that depend on custom initialisers 3492363 Improves constructor that takes collection. Adds iterator, toArray methods. 2ff7175 Adds tests for HashSet. fcf24d4 Adds model for HashSet. 299851c Initial commit for HashSet model. 4beb116 Increase gauge plugin timeout 3c28f8b Mark test for constructor body as known-bug 97f5df3 Small fixes in HashMap 67f6479 Mark HashMap-as-argument tests as known-bug 69a2d78 Add CODEOWNERS 49f7149 Update README.md 56193b3 Split String test_data file e61e374 Enable ArrayList tests 07c84df Run tests in verbose mode e05c5de Add test for arraycopy with ArrayStoreException 9485f07 Add test for arraycopy on itself 0ba83ef Rename test methods as "test" b761e19 Split tests: 1 method per java file d4606d6 Add knownbug test for System.arraycopy of char[] 7955d75 Add System.arraycopy test specifications 965045e Add test and test class file for System.arraycopy 34aba57 Model for System.arraycopy e7df5a9 TG-1394 Setup javadoc 29563a9 All add package information from original JDK 301c209 Correct line numbers covered in OSName2 080ee25 Activate tests for System.getProperty fa5178b Updates .spec file for StringReaderRead4.java test failing CI. ca216e0 Mark HashMapValues.test as known-bug c8aaa80 Add tests for HashMap acfb0d2 Model for HashMap 629a7e7 Copy map classes and interfaces from jdk 478f28f Test for NPE in getBytes with string argument cd8ce59 Throw NullPointerException in getBytes of null 2be372a Use develop branch of test-gen in models-lib CI 1e43155 Adds readline() method to BufferedReader model. 15a3e8c Simplifies some code blocks. Adds back in synchronized blocks for Reader, StringReader, BufferedReader. 89122d7 StringReader working apart from next side affect check issue. 76e950b Adding in recompiled SimpleNPE.class. c8abf9b Removing ambiguously-cased classes for SimpleNPE.class ce7f8bb Small optimisation in constructor a7263fe Small fix for an assume statement that wasn't used da61bb4 Change Object[] to E[] so cbmc will recognise type ee1c756 Remove documention of plug from Readme.md 2f442f2 Test for getBytes without arguments be9139e Model for getBytes with no argument 14aa8fc Split Init.java test_data files into separate files d2aa1c4 Rename specs/jdk to specs/java 22f4cbe Rename test_data/java-library to test_data/functional 2b95dd9 Rename test_data/init to test_data/maven 611e74b Update .gitignore files ffd6fc9 Move init specs to their repsective location in specs/jdk faf8c89 Move specs/util into specs/jdk 1526ee5 Remove plug 4571e79 Add a model for String initialization from array 3ce365e Style: delete trailing whitespaces 19c195c Model for String.toCharArray 1e435df Avoid Strings in ArrayList test f747e81 Enable previously disabled assertion tests 899974e Add tests for most common ArrayList methods 35d05d8 Model for ArrayList and superclasses 7d1ac36 Copy list classes and interfaces from jdk 6259ae1 Mark as knownbug all tests with System.getProperty 87907c8 Update Gauge Maven plugin version in pom.xml 330f242 Add test for getBytes(Charset) with tag knownbug c561bf3 Adding tests for getBytes fedcb81 Style: untabify babfff8 New version of getBytes without static members d10408c Marking test for System.getProperty as knownbug 7712f7b Adding models for BufferedReader close() and constructors. c653b66 Removes File(URI) constructor because there is no URI model. Reinstates NullPointerExceptions. d5a9ad4 Updates models for BufferedReader as notModelled and Reader to model only first constructor. d4b5231 Add tests for System.exit and System.getProperty 282c935 Model for System: exit and (partial) getProperty def14b6 Copied System.java from jdk 7e450e7 Model for toString for subclasses of Throwable d5edf8d Tests for Throwable.toString 071c234 Updated model for Throwable and Exception 4778547 Add line coverage functionality to TestRunner c79fcbd Remove bad line in spec file 8675619 Adds models for Math.max and Math.min TG-836 4a75655 Initial commit for Math model f9f94ea Removing tika tests from Travis. 08cc1ff Recompile all test java files as some of the class files were found to be out-of-date f82552c Run tika tests in travis f1633fd Tag functions with low coverage as known-bug ae1f545 Modify TestRunner to detect incomplete coverage e13ed94 Use CProver implementation in String.replace for Char Sequences b723273 Java util arrays (diffblue#198) 4397193 Enable skipped tests for ByteArrayOutputStream 1f2b1ef Further simplified the File model so tests pass 882497f Updates models for four File constructors. TG-777 0d04723 Initial commit for File model. 6cdba8d Updated setup script d401c31 Use cprover functions in long-to-string conversions aad3499 Tests for new methods in PrintStream dbf6758 Model for print(ln)(Object) and printf 77fb2ba Cleanup String.java model 51b3144 Update TestRunner.java to use new platform values 443a2cb Add tests for some methods in Character.java 8d9cc57 Model for Character.valueOf 4a4e5fc Add construction tests for ByteArrayOutputStream f9a7a13 Add constraints to ByteArrayOutputStream 20d14e1 Linting 7ceb450 Adding Java.lang.Math Test scenarios. (diffblue#188) 1597eab Remove unused makefile 0632300 Small improvements to TestRunner 4cd5a90 Merge pull request diffblue#182 from diffblue/allredj/update-testrunner-options dbaf047 Update Gauge TestRunner options 5c94e8d Skip tests that fail with new platform options 8eeea1e Disable an invalid test a51c521 Merge pull request diffblue#183 from diffblue/antonia/printstream 893e47b Add tests for PrintStream.print(ln) functions 0d1ddc7 Added empty CharArrayWriter model with constraints 630decb Added empty StreamEncoder model with constraints 40c6cf8 Added constraints for Writer objects 9025e60 Update spec file for PrintStream e91c9b3 Empty model for OutputStreamWriter with constraints fb44939 Copy OutputStreamWriter.java from jdk aa37293 Empty model for FilterOutputStream ce0a697 Copy FilterOutputStream.java from jdk 4607f8a Empty model for BufferedWriter with constraints 6ac4952 Copy BufferedWriter.java from jdk 1dce5e9 Empty model for Writer f25b1f0 Copy Writer.java from jdk 1ea396a Model PrintStream.print(ln) b369b15 Copy PrintStream.java from jdk 6b17714 Merge pull request diffblue#186 from diffblue/lucas/fix/IntegerLong 480f37a Removed the toUnsignedString0 method from the Integer class 0df6efe Merge pull request diffblue#185 from diffblue/lucas/simplify/IntegerLong 0b038d3 The toString methods are implemented internally in cbmc b10f24a Merge pull request diffblue#178 from diffblue/reuk/multiple-tests-in-class eb87853 Allow several tests in generated_test class 7e4e92b Merge pull request diffblue#177 from diffblue/reuk/fix-travis bc4ed2b Fix pip usages in Travis 8ed0590 Fix Travis build issues git-subtree-dir: benchmarks/LIBRARIES/models git-subtree-split: cc8db21ff99d5bddf4eb55004b32708129d25d53
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
…of_file_names_of_summaries SEC-16: Bugfix/restrict length of file names of summaries
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Issue: #175
If the user provides a --function argument, tell the
languagetto regenerate the _start function to call this function. Previously if the program had been precompiled (using goto-cc), the start function thatwas used in the original generation would be used again meaning the --function argument was ignored.
This PR is dependent on #343
Real diff: https://github.com/diffblue/cbmc/pull/338/files/cf755ef77320e996be587bde46416f6fd1e17f39..1443d3b2ebee5950b0d422b076943574bad1cef9