Throw on divide-by-zero #1200
Merged
Throw on divide-by-zero #1200
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
smowton
force-pushed
the
feature/throw-arithmetic-exception
branch
from
d0c0e2c to
77fec1f
Compare
cristina-david
approved these changes
Aug 3, 2017
cesaro
approved these changes
Aug 3, 2017
peterschrammel
requested changes
Aug 4, 2017
| const exprt &denominator, | ||
| const source_locationt &original_loc) | ||
| { | ||
| symbolt exc_symbol; |
smowton
force-pushed
the
feature/throw-arithmetic-exception
branch
from
77fec1f to
fb89e5a
Compare
peterschrammel
approved these changes
Aug 8, 2017
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
5a5853981 Merge pull request #1354 from NathanJPhillips/merge-develop-to-sss
5648db137 Merge latest changes from develop to Security Scanner Support
52eb7ed55 Merge pull request #1347 from NathanJPhillips/sss/merge-develop
34492dbd2 Merge pull request #1350 from diffblue/smowton/feature/improved_filter_by_diff
8425bf4bb Merge pull request #970 from diffblue/pointers-with-width
0423be77b Merge pull request #1351 from tautschnig/develop-cleanup
02c4ac6e5 Merge pull request #1303 from diffblue/cleanup-goto-inline
660f804e4 Merge develop into SSS
d3c0b5796 remove legacy constructors
ce863191b pointer types now have width
f72b7fce2 pointer_typet now requires a width
9d5d907ed fixup! Allow extra entry-points to be specified for CI lazy loading
2060b34de fixup! Added __CPROVER_array_replace to complement __CPROVER_array_set
82ab237b0 fixup! Split java nondet pass in two
f12c7909e fixup! fixup! Add --drop-unused-functions option
66719a9f8 fixup! goto-instrument --print-path-lengths: statistics about control-flow graph paths
dfd00d316 fixup! Translate exprt to/from miniBDD
24be89c7b fixup! simplify \'not exists\' to the form of \'forall not\'
191f37198 fixup! a right place to implement the quantifier handling.
d5db0bc08 fixup! added a test case for combination use of forall/exists/not.
7d261396d fixup! Replace BV_ADDR_BITS by config setting
8054162c4 fixup! Instrument string-refinement code such that null-pointer checks are detected
fd5692102 fixup! Fix and run cbmc-cover tests
b28e70122 fixup! variants of service functions for goto_modelt
389221ebe run_diff.sh shellcheck fixes
dce6ae141 Improve filter_by_diff.py and friends
3dd8fe597 Merge pull request #1352 from janmroczkowski/janmroczkowski/syntactic_diff-instead-of-pointer
2e04c176e Replace syntactic_difft pointer by automatic variable
59c882b40 Merge pull request #1294 from diffblue/goto-gcc-fix
b2397e415 Merge pull request #1346 from tautschnig/slicing-prep
dd5adf788 Properly prepare goto model for (reachability) slice
94ce608db Merge pull request #1344 from tautschnig/fix-result-checking
433e139fe Fix verbosity in goto-gcc
394722830 Do not overwrite non-zero return codes
cb467c9df Merge pull request #1173 from karkhaz/kk-synthesise-linker-symbols
85521b026 goto-gcc reads definitions from linker scripts
1fd8b87a9 Add header for magic numbers
c8f69b59c Merge pull request #1108 from karkhaz/kk-neu-cprover-remove
ede380f94 goto-gcc removes CPROVER macros for native gcc
9e4350054 remove assert()
29f1e2a6d eliminate constrained BP calls
5bfe346ea use ranged for
52cbfe8bf Merge pull request #1334 from diffblue/goto-diff-signed
db77596cd Merge pull request #1289 from tautschnig/develop-interpreter-fixes
4c1b3b358 target name wrong for signed variant of goto-diff
75bdd633c Merge pull request #1332 from tautschnig/member_offset_bits
3fdcae449 Merge pull request #1331 from tautschnig/cleanup-metachar
8555871e1 member_offset_bits: express member offset in bits instead of bytes
003482a7b MetaChar: use std::stringstream for incremental escaped-string construction
4349d9146 Merge pull request #1297 from diffblue/union-padding-fix
165ec479b Test alignment of unions
6c56f1981 Do not attempt to compute union sizes when not required
28fb804fa Merge pull request #1288 from tautschnig/develop-json
27fd210bb Use generic simplify_expr instead of local simplification rules
4d35274bd Simplify pointer_offset(constant)
52d1e04d4 Do not use default arguments for json(...)
8254a3fdf Merge pull request #1312 from peterschrammel/bugfix/java-is-internal
052c14984 Merge pull request #1255 from peterschrammel/bugfix/java-unambiguous-basic-blocks
f39e5ab91 Merge pull request #810 from tautschnig/harness-output
48845af9d Interpreter: constify mp_integer typed address parameters
4466408f2 Replace 3-valued char by enum
a01eeb72c Use invariant annotations instead of asserts
e8e16770a dump-c: output a generated environment via --harness
4c94e7c8a goto-instrument model-argc-argv: place environment in __CPROVER__start
15a67e4f7 Merge pull request #1320 from tautschnig/double-output
b6ef688a4 Fix and run cbmc-cover tests
e54bc4765 Tests for unique java bytecode instrumentation selection
bbc99d9be Remove redundant function name from goal descriptions
b85624e29 Add missing function ids to instrumented instructions
6fee43738 Debug info for unique bytecode instrumentation selection
45ca4082d Do not instrument java array built-in functions
d8fdbdb49 Regex match on files to be coverage-instrumented
e641d76f6 Use target source location for java code branches
5e7a328fe List existing goals
99d9613db Expect existing coverage file only to contain array of goals
7f374b3e9 Warn about anomalies in basic block instrumentation
f9ac37a63 Select basic block representative instruction
60eb74e7c Factor out updating of covered lines in block
317f7e851 Protect internals of basic_blockst
6a8b46fca Instruction to be instrumented representative for basic block
e8129a0b7 Merge basic blocks that are chains of unconditional gotos
4be768597 Do not add an "l" prefix to double constants when double==long double
5fb4cbfc8 Merge pull request #1243 from tautschnig/ansi-c-library-fixes
02ed3bf43 Merge pull request #1318 from diffblue/HAVE_JAVA_BYTECODE_cleanup
d5a504507 HAVE_BV_REFINEMENT and HAVE_JAVA_BYTECODE are no longer needed
45a97aabe Merge pull request #1313 from NathanJPhillips/bugfix/invariant-message
94ec79079 Clarified INVARIANT message in get_message_handler
b934a1365 Flag java internal functions as internal in JSON/XML output
4171f197f Merge pull request #1300 from LAJW/refactor/string-refinement-constructors
5bcaacd82 Merge pull request #1308 from reuk/reuk/tg-390
dc8075302 Lazy-load static symbols which are accessed through pointers
0838f611e Fix function declaration slicing
8da7c3003 Constraint generator doxygen
22d699cbe Move constexpr ifdef into a util header
6def0720b Merge pull request #1301 from diffblue/assert_false_cleanup
dbcb5816e Merge pull request #1302 from diffblue/goto-get-target
7fd2bfa53 Use_counter_example assignable via constructor
04fae6d7b Correct comment
acaad4fd2 Remove dead bv_refinementt::set_to
fd59d4726 Preprocess constexpr
107704a1a Fix is_in_conflict with conflict override
83a29dc09 Fix linter errors
40871878c Don't pass language_uit::uit as a pointer
1282d03a7 Update unit tests with new constructors
e5c45a5b8 Prefix all generator member variables with "m_"
01c6767bb Rename axioms to m_axioms
a440da734 Group generator's member variables
5368c8c2a Private get_created_strings
aa8539209 Make more generator methods private
50173d60b Make some string_constraint_generator methods static
07f6b3949 Remove unnecessary typedef
792a70d36 Hide bv_refinement members, add override specifier
abe4046b3 Better bv_refinement constructor
99c815ef1 Make string_constraint_generatort::fresh_symbol non-static
30fe11b60 Better string_constraint_generator constructor
a00b2dbc7 String refinement - remove unused public methods, fix comments
9146575b7 Better string_refinement constructor Act II
51d897a51 Better string_refinement constructor Act 1
16a0a3464 constraint generator const namespace
8043a0d82 Hide index_symbols and boolean_symbols in constraint generator
cf950aba5 Use vector instead of list for constraint_generator data
c51e35e81 Use C++11 initialization for constraint generator members
3217fe337 constraint_generator message is a member
848f2a53d Constraint gen cosmetics
22b48852e Remove usage of static in the header file
e9872a316 Merge pull request #1306 from reuk/reuk/fixup-after-919
ccdb70d3e Merge pull request #1304 from peterschrammel/bugfix/linter-copyright-check
e05deca66 Update function signatures in goto_rw, fixing build
9683cb59f Merge pull request #919 from reuk/no-std-inheritance
4e7a480ee Make linter accept alternative copyright header
c2c9f1ba6 use get_target() where appropriate
df1615957 Merge pull request #1241 from romainbrenguier/bugfix/check-axioms#874
5a04db928 replace assert(false) by UNREACHABLE
90b1ed635 Merge pull request #1281 from tautschnig/interpreter-assert-cleanup
b95359fe6 Merge pull request #1298 from diffblue/source-locations-with-working-directory
8f51b01db Adding unit test for concretize_arrays_in_expression
2c7f23c40 Concretize arrays in axioms when string solver checks axioms
e18a6bd80 Add a function interpreting arrays inside an expression
0b9811b96 Remove useless line break
88c664c49 Add a function that fill an array represented by a with expression
1fd5bb2c1 Adding return check in substitute_array_with_expr
f042ff757 Replace pad_vector by fill_in_map_as_vector
de03d9ced Function for conversion from expression to size_t
df61cebbf Better debug info
5d3771a7e Adding unit tests for next_sibling_or_parent of an iterator
f255abb98 Adding a next_sibling_or_parent iterator
9a8c06303 Setting string-max-length for several tests
6807bed03 Merge pull request #1251 from LAJW/refactor/jar_file
22a424348 Merge pull request #1299 from forejtv/json-source-location
8ebb169fb Add source location to JSON output.
964a85ce5 Make get_current_working_directory return the canonical path name
6d1be1310 Merge pull request #1282 from romainbrenguier/cleaning/assertion-in-preprocessing
a1cf34827 Refactor, fix and document jar_filet class
d099f9bbb Merge pull request #1284 from diffblue/pointer-width-fixup
f5073dff2 output the working directory for source locations in XML and json
2ae344916 Merge pull request #835 from reuk/no-raw-ptrs
e9e413e7d Merge pull request #1295 from reuk/reuk/notModelled
7b5539967 Merge pull request #1152 from thk123/feature/java-array-checker
00406facf Replacing assertions by appropriate macros in string preprocessing
5274109b8 Reduced strictness of the array check
0a99dc86b Added invariants on the correct structure of the array type
37106b6e6 Added check for a type being a valid formed Java array
5c9eb591c Merge pull request #1233 from theyoucheng/fault-localization-xml-ui
a37f09099 Suppress loading notModelled
13cc59883 Fix output of fault localization result in XML
aea00bfd1 Merge pull request #1290 from tautschnig/no-integer_constant
7d5f1158a Replace owning raw pointers with unique_ptr
b00c377c0 Fix invariant warnings
39bee7772 Add missing `empty`
96062375f Fix formatting in event graph
3fa384371 Remove inheritance from std containers in numbering.h
e2a13becc Remove inheritance from vector in expanding_vector.h
b6ca04c9b Remove inheritance from map in value_set_fi.h
3b5263ffe Remove inheritance from map in value_set.h
e5baaa80e Remove inheritance from set in propagate_const_function_pointers.cpp
93ca04bf1 Remove inheritance from vector in ilp.h
280c4fc85 Remove inheritance from list in format_strings.h
423515716 Remove inheritance from map in cfg.h
d9c3fdbc6 Remove inheritance from list in event_graph.h
ed2640d58 Remove inheritance from list in data_dp.h
377b1600e Remove inheritance from std containers in goto_rw.h
225e257b7 Merge pull request #1239 from reuk/virtual-function-unwinding
436211609 Remove constant_exprt::integer_constant
3c71a7404 Merge pull request #551 from mgudemann/update_mp_arith
fd6f91c32 Interpreter: replace assert by invariants
af2309294 Merge pull request #1286 from tautschnig/cover-minor-fixes
f71ff9f6e Merge pull request #1192 from peterschrammel/various-fixes
22016c046 Do not lint C++ regression tests
b71a9f463 Fixed whitespace around "="
a4f29adce Regression tests for pointer-to-member conversion
802044e73 Transform loop that is only executed once into if
12cc79cf0 Merge pull request #1275 from diffblue/goto-model-service-functions
72316855a avoid hard-wired pointer width
288937010 pointer_typet now requires a width
b142da433 Check for memory leaks in C++ new/delete
e49c751c9 Improve ansi-c library syntax check and run via travis
6d6834516 ansi-c library: explicit non-det initialisation, cleanup, syntax fixes
10a0c017e Pointers returned by getenv must not be manipulated
c7afb95a8 variants of service functions for goto_modelt
4f8847338 Merge pull request #1268 from diffblue/link-goto-model
8e52f8dad use invariant
efe922e0e factor out goto model linking into separate file
e64d9c917 Merge pull request #1276 from smowton/smowton/fix/java_pointer_width
a4fa59c77 Add test showing infinite unwinding
31e738292 Merge pull request #1261 from janmroczkowski/janmroczkowski/revert-private-pc-in-goto_trace_stept
3a67dc405 Merge pull request #1267 from reuk/reuk/master-into-tgs
69a82fc7f Merge pull request #1175 from karkhaz/kk-cpplint-if-zero
c8d32fdc0 Merge pull request #1269 from tautschnig/fix-array-cleanup
9d74906a4 Force Java pointers to always occupy one stack slot
3f89279dd Merge pull request #1270 from peterschrammel/contribute-readme
11be8f664 Contributing section in readme
1b20f98be Remove trailing white space
bb88fd294 Add author string to version.h
d0e572fb5 Add size/value checks to bitwise mp_arith operations
c96325bac Fix overly long lines and use iostream for debugging only
a44b36922 Merge pull request #1258 from romainbrenguier/cleaning/string-expr-function-renaming
f17b63712 Merge master into tgs
a86ed4ada Renaming string length comparing functions
e0475561a Making is_refined_string_type a non-member function
960d2c38e Merge pull request #1237 from zemanlx/feature/implement-travis-stages
0bcfc48b6 Merge pull request #1253 from peterschrammel/bugfix/json-output-arrays
f77c97db1 Merge pull request #1222 from owen-jones-diffblue/feature/java-long-to-string
92080c36f Revert "Make pc private in goto_trace_step"
87007b0f4 Tests for Long.toString and related functions
03fb38f27 Turn on Long.toString and improve implementation
2a40436a6 Regression test for java arrays json output
3399a6bed Documentation
8eab28e51 Some cleanup
ea73a2624 Consistently use ID_java_new_array for java arrays
5ccdbea4f Replace simplify_index by simplify_expr
9dd1152fd Merge pull request #1257 from romainbrenguier/cleaning/unused-string-primitives
fdfd294f1 Removing unreachable and unused code in string constraint generation
a0827d696 Merge pull request #1023 from mgudemann/feature/explicit_switch_case_numbers
051ae492b Add switch case number to source_location
70438da56 Merge pull request #1238 from cesaro/fix/tika-coredump
daeeca3eb Bugfix: adding public visibility to opaque symbols
6ce5414c7 Method add_array_types is now static
32889877e Improved debug output
5c66a46a9 Documentation
9136f2afd Merge pull request #1248 from smowton/smowton/cleanup/emacs_style
81e821c74 Unused field
ffa9b55cb Documentation + assert -> INVARIANT
49f096c68 Refactoring + documentation
98400f675 Merge pull request #1240 from thk123/bugfix/402/load-substitued-pointers-lazily
b946f9090 Merge pull request #1254 from allredj/fix-973
cbc49a4a6 Use the pointer_type_selector in lazy methods
384eb4c9a Moved the select_pointer_type to be owned by the java_bytecode_language
7ada043b7 Modified interface for select_pointer_type to take a namespace
d55c8a089 Ignore empty arrays in substitute_array_access
eb21baa2d Merge pull request #1247 from reuk/reuk/allow-glibcxx-debug-tgs
23113a51b Merge pull request #1249 from reuk/reuk/goto-trace-iterator-invariant-tgs
f1023518a Make pc private in goto_trace_step
638cf7661 Merge pull request #1242 from thk123/bugfix/971/cyclic-types-lazy-loading
ecfc981f6 Merge pull request #1206 from romainbrenguier/bugfix/correct-types-of-format-args#1202
8b84458fe Corrected comment in class_hierachy
e365f50b4 Fixed bug in cyclic types caused by refactoring of ci_lazy_methods
2e3a55056 Move Emacs style file so it affects unit tests as well as main source
c0fb7c6c9 Merge pull request #1231 from smowton/smowton/feature/invariant_with_irep
cf5914411 Add non-const target comparator
fe0d9793e Merge test description files for format
f628cc0e1 Adapt allocate_dynamic_object_with_decl to its usage
92f70d6b5 Add invariant helper that pretty-prints an irep
2cf78c7f7 Add ccache for gcc builds
565f5bf49 Merge pull request #1228 from thk123/bugfix/lazy-method-params
e78822722 Tidy up convert method to remove unnecessary else statements
c2fba4016 Remove const that stops copying
ce41adece Tidying changes in ci_lazy_methods
d75570c39 Renamed files to more consistent names
696c13901 Pulled out logic for finding the correct resolution for a given virtual call
5988e61dc Update cbmc-builder alpine container
15e98814f Standardise ccache size to 1 GB
2520c51dd Tighten up lazy loading for virtual functions implemented in base class
a0683133b Swapping asserts to invariants in one of the methods
804f5a71f Added documentation to class_hierarchy
5bc3118e9 Refactored some lazy methods code into a separte file
a029094d2 Split jobs to two stages in Travis
0e084902f Ensure fields are considered in the same way as parameters
5b0c34f42 Merge pull request #1230 from reuk/reuk/synchronized-test
cd169d6d7 Add test showing faulty synchronized behaviour
1f2bb67b8 Merge pull request #1229 from smowton/smowton/feature/use_null_check_annotation_everywhere
1b476894e Improve documentation and omit two unused parameters
4fc60e716 Disable default pointer check (replaced by java_bytecode_instrument)
8486e6c8b Instrument string-refinement code such that null-pointer checks are detected
c659d134f Merge pull request #1197 from smowton/smowton/feature/virtual_call_null_check
074a57e13 Always check for null on a member access
6609f4555 Add tests for NullPointerException on virtual call or array access
273600e55 Check for null-pointer deref on array access
3c59dc9ee Check for null this-argument at virtual callsites
04c957d6e Typecheck within assert and assume statements
870e7fffa Remove needless typecast
2662cadde Fix symbol table alteration during iteration
96826e72a Merge pull request #1227 from smowton/smowton/fix/remove_exceptions_doxygen
187e0809f Merge pull request #1223 from LAJW/test-gen-const-get-mstream
71506605d Merge pull request #1221 from smowton/smowton/feature/force_load_method
e6f02bc8c Merge pull request #1216 from mgudemann/feature/hex_float
e8f536f63 Fix remove-exceptions doxygen
51f088aaf Allow extra entry-points to be specified for CI lazy loading
ab0a35c3e Merge pull request #1220 from romainbrenguier/bugfix/substitute_array_list#275
22f3a0034 Merge pull request #1196 from smowton/smowton/fix/exception_catch
9e10715b0 Merge pull request #1224 from peterschrammel/ignore-doxygen-warnings
c38549f9f Unit test for substitute_array_list
829e37d8c Making substitute_array_list more precise
9a1289dc6 Add overview documentation for remove-exceptions.
c11bba01e Style fixes
5d534eb6c Clean up CATCH instruction code
d15c67dfb Add tests for Java finally construct
08f6b2775 Replace direct use of EXC_SUFFIX with a universal catch
4e13ea915 Implement universal exception handlers
69221aaf9 Implement Java exception catching
c9e526f12 Merge pull request #1194 from cesaro/fix/gen-nondet-init-depth
41fc7e7f6 Merge pull request #1214 from smowton/smowton/fix/restructure_java_instrument
bfb397e6f Suppress some doxygen warnings
88bc1f993 Merge pull request #1219 from LAJW/test-gen-java-escape-backslash
9c035c07a Restructure java-instrument
24e9dde21 Fixing linter warnings
c159fa260 Make message::get_mstream const
0cd10577f Merge pull request #1198 from peterschrammel/fix-json-output-constants
561f38d34 Merge pull request #1215 from jasigal/test/string-refinement-not-contains-unit-tests#884
e5c21c096 Merge pull request #1199 from peterschrammel/rename-json-java-bytecode-index
657153759 Merge pull request #1182 from LAJW/test-gen-regression-string-equals
f5ebce04b Added unit tests for `instantiate_not_contains`
21a5ed565 Factored out `string_refinementt::instantiate_not_contains`
28ca28d34 Test for java-specific output in JSON
8085d9ee8 Documentation
5ff94dee8 Use empty()
9078d1555 Rename bytecode_index -> bytecodeIndex in JSON output
84215dab8 Merge pull request #1185 from romainbrenguier/bugfix/string-bases
c3e273f0f Escape backslash, \t, \f and \b in generated tests
5759b260a Fields in java.lang.Class shall not be null
05d98154c Java gen_non_det allow_null only for root object
ff2f662a5 New option --java-max-input-tree-depth
fe46bedd4 Merge pull request #1200 from smowton/feature/throw-arithmetic-exception
3eab18524 generation of hexadecimal floating point numbers in tests
49526f728 Replace asserts
df5aa9692 Replace asserts
0f80a0251 Fix mode in input/output steps in JSON trace
6c4dba372 Fix language-specific constant printing in JSON
ce7c4985c Merge pull request #1207 from peterschrammel/debug-run-diff
fb89e5aa3 Regression test for ArithmeticException
6ed24e58e Throw ArithmeticException whenever a division-by-zero is encountered
05f62fd95 Merge pull request #1201 from LAJW/test-gen-escape-quota
8c25dcf3c Workaround for travis performing shallow clones with wrong branch
591aea0c1 Merge pull request #1193 from smowton/smowton/fix/always_initialise_exception_object
3292a93f8 Merge pull request #1208 from smowton/smowton/fix/doxygen_fixes
21735a0f2 Rename utf16_constant_array_to_ascii to utf16_constant_array_to_java
d77f0d2c9 Escape '\n', '\r' and '"' characters in generated tests
3e5c5a0c2 Merge pull request #1212 from owen-jones-diffblue/doc/doxygen-for-integer-to-string
0fcce6361 Merge pull request #1165 from LAJW/test-gen-exp-iterators
3339f4102 Fix parameter names in documentation and declaration
665dd70e6 Implement depth-first search iterators for exprt class
535ef5fdb Merge pull request #1181 from owen-jones-diffblue/feature/integer_to_string_with_radix#773
a9b2cdf0f Adding base types of the String(Builder|Buffer) classes
e3cc966c9 Fix Doxygen warnings
0a0a357ca Minor improvements to unit tests
bc3405bec Address @smowton's comments
df813eba6 Fix merge conflict
19d1b91d0 Improve signature of is_digit_with_radix
bcd5eb361 Only apply the overflow condition when needed
4db3fbda0 Calculate max string length for speed
db4f90d43 Integer.toString(int i, int radix) now works
b0d41e174 Merge pull request #1204 from smowton/merge-master-2017-08-03
127ff0469 Merge pull request #1203 from allredj/regression/warnings-1202
30860c071 Add skipped regression tests for #1202
df6a841f0 Merge pull request #1190 from allredj/bugfix/string-exception-847
c4a072bd6 Merge remote-tracking branch 'upstream/master' into merge-master-2017-08-03
86f1d2898 Merge pull request #1187 from LAJW/test-gen-any-desc
3bf46bfe9 Merge pull request #1189 from peterschrammel/object-encoding-tgs
6ec155b80 Call supert::set_to on non-symbol lhs
c1f4db15f Refactoring in string_refinementt::set_to()
ec3798fc2 Merge pull request #1184 from romainbrenguier/bugfix/stringbuilder-setlength#244
a5f87d4c0 Merge pull request #1180 from allredj/feature/auto-complete-zsh
b4262f3c7 Always allocate an exception object at throw site
ef43fc99d Output message about used object bits settings
55d4011a0 Fix getting model for object address (unsigned -> size_t)
28d478d48 Tests for overflows in pointer arithmetic
d122cfb3f Add java address space limits tests
f8bf577ce Catch command line parsing exceptions
84b0c58e9 Allow specifying object-bits via command line and language defaults
84f0af198 Fix axioms introduced for StringBuilder.setLength
bbae82dfc Merge pull request #1183 from romainbrenguier/bugfix/character-digit#851
3ab7e8b97 Merge pull request #1153 from lucasccordeiro/fix-existing-coverage
4928ef657 Regression tests for Character.getNumericValue
cc01a047a ensured minimal requirements for a goal entry
c59e84670 Document convert_digit_char and make precondition more precise
e525d5b9f Adapt convert_digit_char for the case without radix argument
6e2ee6f0c Add regression test for issue test-gen/856
dacf8faf6 Better error message when too many dynamic objects
71d55ec3b Replace BV_ADDR_BITS by config setting
e59511c91 Factorize setting config from symbol table when reading goto binaries
2456011c4 Make configt::set_classpath private
5110f181a Merge pull request #1186 from jasigal/test/change-string-contains
c8dabe24b Merge pull request #1105 from romainbrenguier/feature/string-format
b1531d952 test.pl - go through all child directories
571a72012 Shortened the string contains test.
c172622db added warning message for incomplete/incorrect goals
ceb8ab71f Adding a test with multiple arguments
1d994138f Adding test for exception throwing in String.format
5138f7d04 Adding a test with an indexed argument in format
bf0c217f1 Adding test for String.format with non-constant argument
c7d972f4e Corrections in string refinement constraint generation
6fd1c329e Renaming utility function to utf16_constant_array_to_ascii
27be55555 Adding test for String.format function
2d6d6893d Adding String.format to Java String library preprocessing
162b45b14 Adding calls to add_axioms_for_format in add_axioms_for_function_application
c79baf87e Factorizing part of string_of_array in string_refiniment with code of the generator
9bcb2e7d6 Adding declaration of format functions and string_of_constant_array
f8d54e357 New file for String.format function
b4b0a6e02 Intermediary function for conversion to uppercase
760e6bd8e Adding intermediary function for empty strings
657ca6736 Merge pull request #1177 from LAJW/test-gen-adapt-perl-script
9552a29cd Merge pull request #1122 from LAJW/regression-test
e7259ad9b Merge pull request #1169 from owen-jones-diffblue/feature/rewrite-add-axioms-for-parse-int#702-again
4cfbfb555 Updated two unit tests
7aaf76191 Refactor big for loop into a function
448abb62a Refactor helper functions
527c28228 Rewrite parseint code to use modulo
a3db858b5 Merge pull request #1179 from smowton/smowton/feature/well_known_globals_non_null
89d679962 Mark well-known globals System.out and System.err non-null
71d8a14a0 Add zsh support to auto-complete
710f615a1 Adapt perl script to handle multiple .desc files
b295c0548 Enable working string regression tests
ca96a491b Refactor add_axioms_for_correct_number_format
3a13476d6 Fix formatting spotted by the linter
bb6693793 Merge pull request #1176 from smowton/smowton/fix/restore_object_factory_recursion_set
bcbb6fa0f Merge pull request #1162 from jasigal/fix/invalid-string-constraint-transformations#779
7121d4c76 Object factory: remove type from recursion set on leaving scope
f798feff6 Merge pull request #1178 from smowton/smowton/feature/string_literal_util
7f1d9f8f2 Merge pull request #1118 from jasigal/test/knownbug-for-string-printable
5cb4c9a95 Add a utility for spotting string literal identifiers
c306d56e7 Fixed some spelling errors
d43f9b50c Added `string_constraintt` invariant checking
9f4179fc8 Fixed checking of not contains axioms
7b5fb34c8 Fixed universal constraints that break invariants.
d4be55498 Don't lint text between #if 0...#endif
af36ed141 Added KNOWNBUG regression test for `--string-printable`
727f31658 Merge pull request #1149 from thk123/refactor/select-nondet-init-interface
366ee47ab Replaced shared pointers with references
20fb06816 Added overload with the identiy pointer_selector
96fdb9e5e Moved the logic of select_pointer_type into test-gen
3279e5649 Fixed documentation on object_factory
9af615d9b Merge pull request #1170 from LAJW/test-gen-support
5e02b0cad Disable bug-test-gen-095 string refinement test
39743abb7 Merge pull request #1156 from smowton/smowton/fix/global_variable_nondet_init
8738274bd Merge pull request #1168 from LAJW/test-gen-regexp-escape
7d92f4813 Merge pull request #1163 from romainbrenguier/feature/string-solver-debug-info
f0054270d Fix global variable initialisation
dca977524 Merge pull request #1114 from LAJW/test/regression-434
c163b5b46 Merge pull request #1164 from allredj/add-string-to-string
3b4b0d0c7 Escape square brackets in java_length test descriptor
e5b2cc7b7 Merge pull request #1157 from romainbrenguier/bugfix/char-array-if-correction
cc8c420f3 Making added axioms fit the new invariant checks on universal formulas
7b09ba3c3 Simplify expressions representing arrays that we get from the model
cea763be9 Adapting resolve_symbol map to contain if expressions
317baac16 Better indentation in string solver debug
d3234c80a Handle String.toString() in preprocess
65835c249 Object factory: support global allocation
bbee1b18c Remove field current model
857379db7 Better debugging information in string solver
bc2d47ea9 Passing if expressions representing arrays to the parent solver
e2ef2b279 Removing unused commented instruction
74cffe43b Getting rid of add_axioms_for_if_array
00040555d Take into account if_expression when generating new strings
476f48dcf Propagating index set of if_expression representing char arrays
9d08aa669 Merge pull request #1150 from jasigal/fix/universal-constraint-instantiation#780
ff6135c1e Corrected instantiation of universal string constraints.
7379da481 Merge pull request #1155 from smowton/smowton/fix/interpreter_alloc_size
3fcf2d852 Merge pull request #1110 from jasigal/refactor/update-refinement-solver-asserts
2acd0244f Fix interpreter allocation sizing
0d39c4aee extend the existing-coverage option to support bytecode_index
312a0aeaa Updated assertions and throws to be invariants in src/sovlers/refinement.
19ee8aab5 Added `string_refinement_invariantt` macro as a placeholder for future structured exceptions
ebe4914e6 Merge pull request #1151 from owen-jones-diffblue/revert/feature/rewrite-add-axioms-for-parse-int#702
aec7c1967 Revert "Merge pull request #1143 from owen-jones-diffblue/feature/rewrite-add-axioms-for-parse-int#702"
6bd2e302f Merge pull request #1143 from owen-jones-diffblue/feature/rewrite-add-axioms-for-parse-int#702
489cadb6a Merge pull request #1147 from jasigal/fix/lazy-methods-clinit#747
6f6a24e1b Update tests
d55669348 Speed up parseInt and parseLong
412becd69 Added `$assertionsDisabled` case in `java_bytecode_convert_methodt::convert_instructions` ("getstatic" branch).
e9e1dd7b7 Merge pull request #1141 from thk123/bugfix/invalid-parameters-to-gen-nondet-init
88dbfcd3a Added in parameter to correct call to gen_nondet_init
e8e20ea4f Merge pull request #1117 from mgudemann/fix/ignore_functions_not_in_symbol_table_remove_static_init
dba081fdd Merge pull request #1046 from smowton/smowton/fix/cleanup_array_errors
adfd9a452 Merge pull request #1024 from cristina-david/feature/switch-to-invariants-in-exception-handling
2e115f1f3 Merge pull request #1104 from romainbrenguier/feature/string-solver-if-expr#275
4da42f985 Skip functions not in the symbol table in remove <clinit> loops
2c29180fc Merge pull request #1096 from cristina-david/feature/consider-implicit-exceptions-when-building-cfg
85b2a6d82 Added two more tests for runtime exceptions
68f6ccd42 Adjust regression tests for exceptions: given that we now consider implicit exceptions when building the CFG, there is no need for the redundant explicit throws
728bbc383 Consider implicit exceptions when building the CFG from bytecode
db0b1f298 Merge pull request #1112 from smowton/smowton/feature/call_graph_improvements
d0d046aa5 Add call-graph inversion function
05ffc71c5 Setting bound in if_exprt for constant arrays
da1dc29d2 Merge pull request #1100 from thk123/feature/select-concrete-class-for-abstract-types
98488bf6b Merge pull request #1113 from mgudemann/fix/language_set_options_show_parse_tree
bb108a3d5 Call `get_language_options` on `--show-parse-tree`
40ac69104 Fix a "bug-test-gen-095" test description
a64e6ed9c Merge pull request #1097 from owen-jones-diffblue/feature/parseInt#410
1563e30e0 Enable strings test suite
e2e670efa Removing whitespace that causes an error on windows
a3f7eedfd Made jsonArrays test less strict
248ec8ea3 Don't require pointers point to classes
90286a86f Adding regression tests showing the modified gen code works
e4ac6e21f Modified definition of abstract to not fall over on void* types
2c79f51fb Removed extra code and just combined into gen_nondet_pointer_init
78a4e05ad Made the random selection alphabetical instead of random
d5513db13 Make class derived from object factory
a904f089c Add class for randomly selecting a concrete child of an abstract class
8dcff58e8 Code tidy changes
cc201f7a7 Test for char array expressions containing if_expr in VCC
b84d9d59b Handling of if_exprt in checking universal axioms of string solver
2e6d2ce68 Using warning() for warning messages in string solver
30306f1fe Handling of if_exprt in char array assignment
f06649bb6 Adding axioms for arrays of characters in the form of an if expression
735065ce9 Make Long.parseLong work
79c0aaaf0 Merge pull request #1106 from romainbrenguier/bugfix/append-long-warning#447
f8131c35e Merge pull request #1102 from romainbrenguier/pull-request/remove-unused-function-in-string-preprocessing
836be74b8 Merge pull request #1103 from romainbrenguier/bugfix/declare-pointer-before-use
e2dea9b4f Correcting type in add axiom for int
8082795f4 Add test checking that string content is declared before being allocated
280c45b13 Declare malloc-site symbol before use
c33306a9d Removing string_literal declaration
07ff02d22 Removing string literal function from string preprocess cpp
941945491 Merge pull request #1084 from thk123/feature/mark-abstract-classes
6c7d6d49e Merge pull request #1088 from smowton/smowton/fix/instrumentation_source_locations
4193022c8 Added unit tests to demonstrate the abstract flag
41bb0d443 Store in the class_typet whether the class is abstract
a3e75574a Merge pull request #1098 from smowton/smowton/fix/cast_null_pointer
5bca0b2a5 Merge pull request #1094 from smowton/merge_master_20170705
0e1b95c5d Merge remote-tracking branch 'upstream/master' into merge_master_20170705
eb3b64c93 Ensure source locations are assigned to all expressions
530a2dd62 Merge pull request #1078 from jasigal/fix/contains-mem-issue-511
73bd18d6a Don't throw ClassCastException when casting null pointer
ca3dbab05 check_class_cast: don't duplicate existing assertion
c242674b9 Merge pull request #1076 from jasigal/fix/lastIndexOf-issue-614
bb31bb547 Added regression test for lastIndexOf
f5f122e55 Added lower bound in lastIndexOf
45e0b9782 Switched from assertions to invariants/preconditions in exception handling
939fb8766 Added regression tests based on originating test-gen tests
8495451a9 For contains, added bounds for substring index in !contains case
9ab281b75 Merge pull request #1087 from owen-jones-diffblue/revert-3f4c9d1
7a0ef6cad Revert "Merge pull request #986 from owen-jones-diffblue/bugfix/goto-trace-contains-ssa-information-test-gen-support"
3f4c9d100 Merge pull request #986 from owen-jones-diffblue/bugfix/goto-trace-contains-ssa-information-test-gen-support
7c415e89f Merge pull request #1071 from jasigal/fix/indexOf-issue-612
8226c5b7e Merge pull request #1019 from cristina-david/feature/refactor-exception-instrumentation
05516bbf5 Added regresion test for indexOf
cd29f689d Extended check_axioms for not_contains and refactored
87ff9de34 Fixed function inversion.
3d418796b Merge pull request #1077 from owen-jones-diffblue/feature/parseInt#613
2a7e25c7d Merge pull request #1067 from cesaro/bugfix/groovy-lvt-handling
6a18c24aa Merge pull request #1079 from peterschrammel/bugfix/java-entry-point-modes
236e44231 Adjusted runtime exceptions regression tests
a6d1084e3 Move generate_class_stub out of java_bytecode_convert_classt and to java_utils.cpp and use it to generate stubs for exceptions
961c0a35f Refactoring the runtime exception instrumentation out of java_bytecode_convert
72677f2b6 Add regression test for runtime exceptions instrumentation
b63547fbc Merge pull request #1064 from Degiorgio/fix/inherited_methods
bdb1a3c5d Regression tests
238c02fa8 Add parseInt with radix to preprocessing
4e5d8cce4 add_axioms_for_parse_int can take optional radix
50732ee85 Create is_digit_with_radix()
af4edae93 Fixing inheritance issue for java programs.
56307d03c Merge pull request #1050 from mgudemann/fix/revert_assert_non_nil_decl_assign_json_trace
5409f5631 Add missing header guard endif comment
0e4176d23 Fix modes in java entry point code
a1af44f10 Regression tests: groovyc lvts
5330536f5 Documentation for java_bytecode_convert_methodt::variable
cf2600829 Discard LVT if bytecode > codet translation cannot make sense of it
d32543190 Merge pull request #1017 from romainbrenguier/pull-request/float-to-string-conversion
e1f2d77fa Adding tests for String.valueOf float
64558ca16 Update comments in string_constraint_generator_valueof.cpp
cae6d279b Style improvements in string_constraint_generator_float.cpp
4eacbd359 Renaming add_axioms_from_float to add_axioms_for_string_of_float
105925ac4 Comment corrections in string_constraint_generator_float
a8b1e8ec6 Changing assert for PRECONDITION and UNREACHABLE in float to string conversion
5c71733f9 Comment corrections in string_constraint_generator_concat
651836996 Adding test for the String.valueOf(F) function
8367ff522 Allocate array in String result of String.valueOf(F)
4ecec1ab1 Improve the documentation of the string preprocessing
685a105e2 Improving the float to string conversion in the preprocessing
518efa497 Conversion between string and float moved into a new file
5f28dc66d New file for conversion between floats and strings
d8af6b648 Adding id for scientific notation of floats
9c94cb30b Correcting initialization of floatbv_typecast_exprt
82642b959 Add regression test for nil assigns in JSON trace
d299ea29e Allow "unknown" value assignments in JSON trace
4a2876baf Merge pull request #1033 from romainbrenguier/feature/string-builder-appendJ#447
6c0fcda90 Merge pull request #1053 from cesaro/bugfix/581-incorrect-params
1e68ad273 Documentation: functionality around `setup_local_variables`
0968e9368 Regression tests: java method parameter detection
9bb474dc0 Fixes parameter detection on bytecode->goto translation
77bda4efc Merge pull request #990 from thk123/refactor/gen-nondet-init
fde9c7659 Correcting assertions.
90c8198fc Added missing comment to class_hieracrchyt
6770e74f8 Split up gen_nondet_init for structs
9ccdd3234 Split up gen_nondet_init function
a85737244 Merge pull request #1066 from diffblue/smowton/fix/json_trace_pointer_offset
edd7b0a5d Fix remove_pointer_offsets
f690a3c80 Merge pull request #910 from allredj/cmdline-feedback
71b3fd2d1 Merge pull request #772 from lucasccordeiro/fix-existing-coverage
a63f2bbd0 replaced assertion by invariant in cover.cpp
406a6c40e Merge pull request #1059 from smowton/smowton/fix/structured_trace_output
7583da2a0 Merge pull request #1056 from diffblue/smowton/cleanup/remove_skip_before_cover_annotation
913de981b check for java bytecode index in the existing coverage
20f395172 Correction of line numbers in valueOf(long) test
33fc907df Call remove-skip before coverage instrumentation
d68f1372e Merge pull request #1055 from diffblue/smowton/fix/set_block_source_locations
0e5b254cf Java frontend: Set source locations on instructions in code_blocks
6b6f6cb45 Add message for unknown cbmc option
4440343e1 Adding tests for String.valueOf(long)
eaad10007 Comment on the bound for overflow in int to string conversion
fb3ab81c0 Using PRECONDITION instead of assert
7fa229b3d Update comments in add_axioms_from_int to reflect changes in the code
15e88e736 Making tests for int to string conversion more precise
8a803100e Correcting when to do overflow check in add_axioms_from_int
70d0cb0e0 Forgotten premise in add_axioms_from_int
71ace4332 Merge pull request #1036 from romainbrenguier/feature/string-to-lower-case
20e4def6a Add preformatted message flag
0610b0d74 Merge pull request #992 from romainbrenguier/bugfix/string-builder-append-object#442
fdb6f2e5c Ordering functions in alphabetic order in initialize conversion table
a95e8dc33 Removing comments on non-supported functions in string preprocessing
b0b21bbb5 Remove functions that are destined to be modelled in Java
9ac5dff9d Merge pull request #1051 from smowton/smowton/fix/strings_debug_output
fbe8be8dd Merge pull request #1026 from romainbrenguier/bugfix/string-to-char-array#443
70a980660 Merge pull request #1021 from romainbrenguier/bugfix/object-get-class#272
05875e1d7 Merge pull request #922 from romainbrenguier/pull-request/arrays-in-trace
bc968b0f7 Always pass namespace to from_expr
0619f0587 Better test for String.toCharArray
c745aa79d Improvements in the code for String.toCharArray in preprocessing
50be5302d Removing overflow check in quantified formula
fbb5724db Declaring string expression symbol for each string_exprt
f950ffc74 Documentation for json_goto_trace in doxygen format
5cfa41309 Adding test to check that data field of strings are set in json
f4fa77802 Simplifying array access and expressions with pointer offsets
02b794290 Simplifying expressions of the form &array[0] in json
a9de8594a Merge pull request #1001 from allredj/pr/add-axioms-for-concat-substr
f84d96b11 Merge pull request #1048 from allredj/fix-for-platform-975
53237027b Fix bad return type of char pointer func
fc47fe31c flattening/arrays.cpp: replace throw and assert with invariants
cf0875a9e Merge pull request #1047 from smowton/smowton/fix/cleanup_array_errors_hotfix
610d78a68 Merge remote-tracking branch 'origin/test-gen-support' into smowton/fix/cleanup_array_errors_hotfix
ce8303968 Replace std::cout for errors with messaget::error()
cf39c2994 Replace asserts
ef5bd4dbf Modifications to doxygen
334ab00b9 Comment in description of test for String.replace()
1e567fbe4 Add an add_axioms_for_concat_substr function
695b3ce4a Add comments about characters transformed by toLowerCase
8cf48d329 Merge pull request #1045 from smowton/smowton/fix/restore_win32_compilation
e6e7e168f Merge pull request #1044 from smowton/smowton/fix/lazy_loading_clinit_on_static_call
eeac67231 Merge pull request #1018 from Degiorgio/test-gen-support
448f1ca33 Merge pull request #1037 from owen-jones-diffblue/owen/errors-to-warnings
2534b8000 Handling incomplete traces.
471254ce3 Fix win32 compilation
092f8e224 Lazy methods: fault in static initializer if a static method is called
4701c0b32 Change two errors to warnings
2d9739300 Merge pull request #1014 from smowton/smowton/cleanup/stray_include
5553652ef Improving the test for Java case functions
6a156a9f6 Making toLowerCase more precise
6fa72c839 Merge pull request #1000 from smowton/smowton/feature/class_access_flags
c50f3d595 Merge pull request #1004 from smowton/smowton/feature/time_limit_minisat
0ee493340 Add simple time limiting to prop_conv and propt
38907fce4 Merge pull request #1003 from smowton/smowton/cleanup/traces_to_status_out
7cf8d5f58 Add support for recording and propagating class access flags
f88f46177 Remove stray include accidentally merged from master
23e2c9b2c Merge pull request #1012 from smowton/smowton/merge/master_20170614
4324bbd96 Disable warnings that result from array-of with zero length
eed0afb9a Merge remote-tracking branch 'origin/master' into smowton/merge/master_20170614
823b32d3e Merge commit 'e9349f8' into smowton/merge/master_20170614
a320377c2 Merge commit 'aed3c25' into smowton/merge/master_20170614
1a3eb1ceb Merge pull request #945 from romainbrenguier/feature/object-get-class
db1cd5f34 Cleaning the initialization of string expressions from constants
e9e3989bf Providing code for Object.getClass() in bytecode conversion
3d80c6f8c Merge pull request #1006 from romainbrenguier/bugfix/memory-leak-in-json#294
2105ee9dc Merge pull request #994 from allredj/pr/string-preprocess-improve-lengths
01e9e6791 Using unique pointers to avoid memory leak in json for expressions
e1aadeb44 Write traces to status() not cout
a308fb5e2 Merge pull request #996 from cristina-david/bug/remove-assumptions-about-exception-handlers
161329004 Update smoke tests for String.length
72b611a1b Improvements on lengths
8f629b6a0 Addressed reviewers comments
bb9c28ac6 Added regression test capturing an exception handler that does not start with astore
770728742 Always push the current exceptional return variable on the stack before converting an exception handler
4b9f42ecf Merge pull request #995 from romainbrenguier/bugfix/add_string_type#480
07001e996 Merge pull request #993 from allredj/pr/improve-init-and-copy-of-strings
d475cf139 Merge pull request #889 from romainbrenguier/bugfix/char-input-type-in-trace
2c27b416b Assertion to forbid calling json() with nil values
b0b8bbccc Adding assertions to prevent the "data" field from not being set
fd80fe6be Adding assertion to make sure "type" field is always set
62d355cc7 Use the from_type function to get string for the type
9936ddbdb Improvements following review on PR#995
985baf18a Take care of cases where the symbol exists in table diffblue/test-gen#480
c61d0951a Improve constructor and copy of strings
d41448fb1 Call to lookup that does not throw when symbol is not found
7dc5efa6f Adding a mode option to json output diffblue/test-gen#294
2120a44b9 Merge pull request #978 from romainbrenguier/feature/index-of-precise
cf5b5d374 Update regressions tests for indexOf and lastIndexOf
ff81171bb Merge pull request #983 from romainbrenguier/pull-request/override-in-final-step
ac71afe93 Merge pull request #837 from allredj/string-solver-bugfix-symbol-map
65f2e3696 Overwrite String type
dcf7614d4 Correcting replace_string_methods to not overwrite the map we iterate on
94f99b5d5 Adding forgotten precondition in not_contains constraint
d4a9b2a5b More comments on the output of last_index_of functions
80dff96f9 Correcting lower bound in axiom added for last_index_of
af98378f8 Correcting misuse of univ variable qvar instead of qvar2
b06476c47 Correcting indentation in the comments
3e9668a71 Correcting a mistake, universal variable was used in non-quantified formula
7edfe0d2d Typo in comment
069da5161 Typo in comment
1eb7d748e Uniformising mathematical notations in comments
ca32a0a1d Removing string conversion from method conversion
0dcb77341 Change the step at which we replace String methods code
a4ab7db7b Updating comments for functions adding axioms for index_of
eb9a78974 Correcting addition of symbol to symbol map
f3f5a19b2 Replacing str and substring by haystack and needle in the comments
2d16c2cf9 Correct comments and axioms in lastIndexOf
68cdc6fd1 Renaming str and substring to haystack and needle
1eb3263f1 Making comments about the output more precise
666bec088 Removing comments about lastIndexOf being imprecise
bc3eedc52 Replacing str and substring by haystack and needle
9b11653a8 Updating comments for index_of and last_index_of on characters
4f4df8e1a Optimize last_index_of for constant argument
bc59d0c6a Making lastIndexOf precise diffblue/test-gen#77
f9199a097 Make index_of precise diffblue/test-gen#77
f4f4c44c7 Merge pull request #976 from allredj/test-gen-strings-update-regression
f05ea1748 Merge pull request #980 from romainbrenguier/feature/forbid-copies-of-string-preprocess
56800d52e Add strings-smoke-tests to regression Makefile
86de08fbc Update strings-smoke-test
0cc5ae662 Using delete to forbid copies of objects
12c5f2661 Merge pull request #828 from allredj/test-gen-string-fix-159
00bb9b1c2 Merge pull request #900 from romainbrenguier/pull-request/forbid-null-data-in-string
e3b44c700 Avoid copies of string preprocess objects
5b5a4d223 Merge pull request #906 from allredj/java-string-preprocess
0bbfffd96 Merge pull request #943 from romainbrenguier/bugfix/test-gen#118
7653a764b Removing and deactivating the old preprocessing
45a026040 Merging string and character preprocess as one argument of bytecode conversion
af2fd46c7 Replacement of string preprocessing for Java
8f120bd7a Declaring auxiliary function for allocation of dynamic objects
a9d96f661 Remove SSA ids from goto trace
b2dd3a21b Disallow null pointer in data field of String
671193c2f Merge pull request #960 from pkesseli/bugfix/main-and-args-not-internal
c07cdf953 Merge pull request #940 from cristina-david/feature/uncaught-exceptions
f42cc33e4 Addressed reviewers comments
d0ec24270 Merge pull request #975 from thk123/feature/access-methods-on-code-type
b6e193ea3 Adding accessors for the access properties
229817d23 Remove duplicate version of class_hierarchyt::get_children_trans_rec
37c0a366a Avoid marking main function call / arguments as internal
927e48c8e Merge pull request #958 from thk123/bugfix/trace-missing-class-info
47cd9273e Ignore AssertionError This is ignored when we comoute the set of escaped exceptions as well as when replacing throws.
f59ec9a74 Modified the expected goto-program for cbmc-java/virtual7
ca693b4de Make sure that both the caller and callee have exceptional return vars before instrumenting function calls
047671b09 add the uncaught exceptions analysis to the Makefile
d4378331e Added an uncaught exceptions analysis
a54d806fb Merge pull request #941 from thk123/update-to-master-19-05-17
575b34331 Adding simple test for trace correctness
851037459 Revert "Remove variable that is always false"
06837c8bf Use the member functions to make code more robust
eff658a97 Add hanlded for constant strings
f9748b1b1 Merge commit 'c4412e9' into merge-master-20170522
be3f76179 Merge pull request #942 from pkesseli/java-switch-instruction
befb6e261 Fix a mistake in java_identifier_start
013f442fc Add missing swap instruction
f791fef65 Merge pull request #939 from reuk/str-refine-use-after-free
05d1ec641 Merge pull request #938 from reuk/pedantic-fix-test-gen-support
f4ba652cc Fix signed/unsigned comparison warning
539db2549 Fix use-after-free bugs
72da3fb3c Give pragma files a '.def' suffix
76dda349c Remove unnecessary asserts
c21e64c93 Remove unnecessary flags from travis.yml
44c96ebda Build cleanly without globally disabling warnings
f22a696f9 Merge pull request #901 from dcattaruzza/ml-test-gen-integration
c5033663f Merge pull request #856 from cristina-david/bugfix/uninitialised-exceptional-value
116237769 Specification for contains in the case of a constant argument diffblue/test-gen#159
2dc8cf3c3 Merge pull request #848 from cristina-david/bugfix/set-bytecode-index
34a847c76 Merge pull request #829 from allredj/test-gen-string-fix-201
fe03a6e9e Merge pull request #844 from allredj/test-gen-string-fix-199
0e5a54e97 Avoid initializing the index set if not needed diffblue/test-gen#199
f8f761092 Merge pull request #819 from allredj/test-gen-string-fix-158-2
072ed0f8b Overhaul of string concretization
aa78fc1f8 Merge pull request #841 from allredj/test-gen-string-fix-244
0bc3416d3 Merge pull request #840 from allredj/test-gen-string-fix-241
6c626c7c1 Merge pull request #843 from allredj/test-gen-string-fix-245
64c8bdf70 Merge pull request #822 from allredj/test-gen-string-fix-170
43e324f39 Added new friend to bmc to handle refactoring
2c78d4648 Correcting constraints for conversion from int diffblue/test-gen#241
6b24ec76d Implement StringBuffer methods
7cf1c92d4 Fixes in pre-processing for issue #170
95844654f Correction in add_axioms_for_set_length
21eeb2979 Enable working smoke tests
67961355a Added the bytecode index to the expected result of the regression tests
6d1feea66 Set the bytecode index for the instrumentation in goto_check.cpp
1e9123f0a Always initialise the exceptional return variable of the entry function
30b5c726f Merge pull request #857 from smowton/refactor/move_coverage_arg_parsing
468ad17b6 Merge pull request #854 from cristina-david/bugfix/handle-typecast-in-interpreter
d11747558 Merge pull request #860 from reuk/nondet-memory-fix
f5aa61270 Merge pull request #866 from reuk/linter-complaint-fix
d15d84238 Fix indentation in convert_nondet
6deaa3b89 Remove skip in replace_java_nondet.cpp
8ad72a70d Fix linter complaint
c195e63c3 Remove 'erase' in replace_java_nondet.cpp
b8586a6e3 Move coverage arg-parsing into cover.cpp
466f6292b Merge pull request #852 from smowton/smowton/merge/master_2017_04_20
520cf38ce Handle typecast when evaluating addresses in the interpreter
9dea22a93 Merge remote-tracking branch 'upstream/master' into smowton/merge/master_2017_04_20
7cbe566dc Merge pull request #827 from owen-jones-diffblue/bugfix/java-parameter-declarations
3fddf20d3 Merge pull request #691 from reuk/java-nondet-new-pass
ff72ddc8c Ensure assume only throws upon predicate failure
f4a47f9e1 Split java nondet pass in two
58f3c446c Merge pull request #824 from smowton/smowton/fix/object_factory_recursion
e81b1d9fe Merge pull request #821 from smowton/smowton/fix/checkcast_against_null
b5e06ba86 Merge pull request #817 from forejtv/bugfix/ccache-on-mac-clang-testgen
2f5a39156 Merge pull request #814 from cristina-david/bugfix/report-entry-point-exceptional-value
df1caca1e Adding namespace to arguments of from_expr in debug diffblue/test-gen#201
17db86df0 Refactor java object factory
dc94557d8 Rearrange loop in remove_java_nondet
19c8d8d7c Suppress loading methods with nondet signatures
f85494b07 Add remove_java_nondet
7ed66a1a0 Add tests
241dbee16 Add org.cprover package and makefile
77ac3a243 Fix Java object factory recursion set
3c5ae1a56 Allow checkcast of null pointer
935825efc Merge pull request #820 from smowton/smowton/fix/init_zero_length_arrays
035ae9211 Restore array-set for nondet arrays
a1b6ea374 Travis fix: ccache limit was in the wrong section
827519db9 Merge pull request #815 from smowton/smowton/fix/c_bool_is_zero
fcafa4178 Merge pull request #813 from smowton/smowton/cleanup/remove_trace_stackt
083d8a65f Always report exceptinal output in __CPROVER_start
5c289b18c Support ID_C_bool in exprt::is_zero
3a87f5cae Merge pull request #811 from peterschrammel/bugfix/expr2java-boolean-tgs
718683f6f Remove trace_stackt
396a53091 Remove unused nullptr case in expr2java
7755820ab Fix boolean to string conversion in expr2java
8fd111868 Merge pull request #803 from owen-jones-diffblue/bugfix/java-parameter-declarations
11402daee Assign variables for all parameters
57f592745 Merge pull request #806 from allredj/string-axioms-corrections
cc3e3cc61 Merge pull request #805 from allredj/string-fix-172
72e3e350d Merge pull request #802 from allredj/string-fix-119
94e9c647e Various improvements in string refinement
f0004a5d2 Corrections on generated axioms
02f86978d Adding overflow checks in the parsing of integer (#172)
e05353e49 Merge pull request #800 from allredj/string-functions-alphabetical
621f366ff Correct a mistake in the signature for String.valueOf
aaa56bb21 Adding tests for issue diffblue/test-gen#119
03667afea Make add_axioms_from_bool add concret constraints
b04878720 Merge pull request #796 from smowton/smowton/feature/clinit_on_demand
75337a21e Merge pull request #788 from smowton/smowton/fix/preserve_new_array_type
c63141902 Add tests for static initialization order
85b1e4f4f Invoke static initializers on demand
668f30f0e Always convert methods in two phases, even in eager mode
318ab8612 Improve `class_typet`'s base description
5851f6374 Order string functions in alphabetical order
4bebee959 Merge pull request #790 from romainbrenguier/string-solver-refine-array-option
cb065bfbf Merge pull request #799 from peterschrammel/fix-style-java-entry
2fc6f099d Preserve true array type in Java -> GOTO conversion. Fixes #184.
788a60e45 Merge pull request #794 from cristina-david/missing-function-name
051a245b3 Merge pull request #789 from smowton/smowton/fix/restore_array_skip_init
e5293e50b Merge pull request #785 from forejtv/cherrypick-osx-travis-to-test-gen
3cb035e4d Fix style to silence cpplint
7e1b38208 Set function member for class identifier assignment
44041aeff Allowing some options for string refinement
46151843e Restore array skip-initialize flag
158d95022 Speed up OSX builds on Travis.
531ef7e62 Merge pull request #782 from forejtv/cherrypick-appveyor-fixes-to-testgen
a2f4ab3bf Coverage (branch mode): add missing is-current-function test (#781)
b4658eb76 Allow long long int instead of just long int in regexp of some tests.
ebaad56b7 Remove blank lines from regression test specs
e610c081e Implement Java array.clone (#774)
ee5d7fc79 Run static initializers for enumeration types before all others (#773)
512d6efa3 Initialise array clsid fields (#770)
48b942733 Merge pull request #762 from smowton/smowton/merge/master_2017_04_05
f2bfd675a Merge remote-tracking branch 'origin/master' into smowton/merge/master_2017_04_05
372bafbd1 Merge pull request #758 from smowton/feature/cover-function-only
8081a9a29 Merge pull request #738 from allredj/test-gen-support-string-additional-options-2
03891c93a Merge pull request #699 from romainbrenguier/test-gen-java-character-library
161aeee31 Apply review comments to coverage code
91d07b1e1 Bug corrections in string refinement
dead0224b Corrected type problem for the function Character.forDigit:(II)C
da849ee28 Adding conversion for functions of the Java Character library
4c4d85ca6 Implement function-only coverage
6b5d9b70a Merge pull request #742 from allredj/test-gen-fix-build-issue-with-sparse-vector
d5c6ac636 Added option to the string solver for string length and printability
6c1f70074 Adding options to cbmc for parameters of the string solver
9ddfb302a Add includes to sparse_vector.h
932d7df71 Merge pull request #709 from lucasccordeiro/fixing-issue-20
2499213a3 Merge pull request #717 from peterschrammel/bugfix/port-json-pointer-fix
508131009 added internal field to json output
a5f773923 set internal for specific variables in the counterexample trace for test-gen-support
28fb701b5 Merge pull request #689 from romainbrenguier/interpreter-sparse-memory
1b97f3dbc Add support for unbounded-size objects
5d2919b36 Interpreter: switch to sparse vector memory map
2e62c6638 New class for sparse vectors in util
072e37412 Display dynamic object names as 'data' in JSON traces
fd96accc0 Merge pull request #705 from peterschrammel/pull-from-master
58d68436d Merge branch 'master' of github.com:diffblue/cbmc into pull-from-master
c3cc87261 Merge pull request #678 from allredj/testgen-string-solver-dev-1-regression
c7691a4ff Restructuration of tests on strings
3eeb73d60 Merge pull request #676 from allredj/testgen-string-refine-option
9d2a1158d Change option name to --refine-strings
c7328e225 Adding the string refinement option to the CBMC solvers
055829123 Adding string solver cpp files to Makefile
402f8e180 Adding string preprocessing of goto-programs to Makefile
6cc1266de Adding refined_string_type to util Makefile
a11a70b53 Merge pull request #688 from allredj/testgen-corrections-for-675
df36fecde const refs and clean up
e4e26d861 Merge pull request #675 from allredj/testgen-string-refine-corrections-on-preprocess
29d67d39e Merge pull request #679 from diffblue/master
6958a561d Need to assign length before calls since it can be overwritten by functions with side-effect
bdbeaf586 Many corrections in string refinement
a04dc21fc Many corrections in preprocessing of strings
c9ff379f1 new identifier for converting char pointer to array
72ad6ad81 Making add_string_type more generic
e81a5e04e Merge pull request #669 from romainbrenguier/string-refine-preprocessing
c362a2605 Merge pull request #660 from peterschrammel/pull-from-master
aa8c91ee6 Update test-gen-support from master
5cb0e5e09 Removed mention of c string type
2929d7f04 Removed distinction between c string type and refined string type
70af9ce61 Moving refined_string_type to util
3a2e210d4 Moving is_java_string_type functions to string_preprocess
1aede785e Preprocessing of goto programs for string refinement
c33736331 Merge pull request #631 from peterschrammel/update-from-master
dcd0c52df Add test for Alpine linux (musl-libc).
0381aab5e Support for Linux based on musl-libc.
712f94ff8 Remove the top variable from the cfg_dominator analysis.
5baa807a6 Add space after comma globally within the line
f1a99f78f Replace tabs globally within the line
0f69c9341 Fix missing space after , errors
32f91b828 Fix ; after } errors
db2858718 Explore matching nested bracketed stuff
039ac4d8c change from vector indices to map
aec47b700 take comments into account
52952bb68 add regression test
898ba0c1e add jars from JSON config to classpath
6de183b7d support class load configuration via JSON file
15fd106b1 allow regex to limit class files loaded from JAR
28d00ebd1 + regression test for Java exception handling
8d2a26b86 Modified the expected goto-program for cbmc-java/virtual7 as exception handling instrumentation introduces new labels and GOTOs
0a11374e7 Add jump to the end of the current function if a function call throws an exception for which there is no handler
18fa65d50 Restructuring such that the exceptions instrumentation is added in one pass over the goto-program
d0d20360e Forced try-catch to start a new basic block
6f5d6409f Recompute live ranges for local variables and add corresponding DEAD instructions
50dfffb70 Fixed test description for cbmc-java/virtual7
58a076309 Escaping brackets in test descriptions
05f223359 Moved Java exceptions regression tests
33c8e3714 Remove throw/try-catch and add the required instrumentation
a07691896 Recreate the try-catch structure from the exception table
ebf9002e3 Regression tests for exception handling
206f7f4d6 Added a side effect expr that pushes/pops Java try-catch handlers + irep ids for Java exception handling
4d316064c Use remove_instanceof in driver programs
6861a5826 remove `<regex>` from unapproved headers in cpplint
f430ec5a4 Fixed compilation issues on MinGW
7d73d66f1 libzip/zlib download no longer needed
c384ff74e auto-fix cpplint errors with generated sed script
85889e9bd disable unaligned load/store for g++
8e3f68125 regression test with multiple JARs/classpath
1dd43f634 update Makefiles / remove all references to libzip/zlib
c2a8fb248 type cleanup in miniz
7d2536db6 use amalgamated files from release tarball
4854c9a35 initial support for miniz
bbe06ad69 Java checkcast: fix stack when check disabled
4cb8705b2 set EXIT to 10 to all failing string-solver test cases
2f06442f9 Add json->irep deserialization routine
2cc423e5f added json to cegis makefile
6cc36c156 added CPROVER_initialize
7e71a71c8 do not produce test goals for constructor and destructor methods
2440baf68 add the --no-trivial-tests option to CBMC
51ecf5166 add consider_goals method
6bf5c14f0 use json file suggested at github issue #187
a91860a6e method to construct a coverage_goalst object
eff4b7149 a goal should be identified by a source_locationt
f70eadf6c implement get_coverage method
143b53e77 a goal should be identified by a source_locationt
b128a597e default variant of instrument_cover_goals that uses an empty set of existing goals
ead4b237a add more test cases to check existing coverage
ae5282bdf generate goals only if they do not exist in the json file
055f515bd extend java_bytecode for test-gen-support
8236166af Changes to get java compiling
8dd297e5a Call the generate_opqaue_stubs from final
fa73b8bcb Use the symbol in expr2c
e2614efa4 Adding simple regression for struct function
4e6b2a290 Added comment explaining the type of symbols we aren't stubbing
a1014a13f Use the system_library_symbols when generating stubs
e11fd6384 Added a flag for enabling opaque method stubs
dddb5522f Refactored method for generating return symbol name to languaget
18b1445a9 Pass the whole parameter in when generating the symbol
53f4a9905 Create stub argument identifiers for functions with parameters
35d847be9 Don't create stub for CPROVER_ functions
c09db527d Generate stub method for opaque functions
5a33d9142 Merge pull request #582 from peterschrammel/update-from-master
1cbd032f7 Merge branch 'master' of github.com:diffblue/cbmc into update-from-master
60744ee17 Merge pull request #580 from mgudemann/update_interpreter
fef1fed6b update interpreter
8ae50cd8c Merge pull request #579 from peterschrammel/test-gen-support
b7d828bc1 Updated dump-C to use the new class
02d2b9d0c fix problem with missing comma / range fix for reaching end
f5f47a704 add regression test for coverage lines
2ae1f47f3 compress list of lines into line ranges
e55f20b6f output covered lines as CSV in show_properties
5c309076a Remove assume as coverage target
1436e3960 Regression tests for Java assume
0cf34af4d Support for Java assume
7ac505d22 loop unwinding in static init of Java enum
99eb1a0b3 Discover lexical scopes for anonymous variables
d485c88a2 Factor class identifier extraction out of remove virtuals
2f5b86689 Autocomplete script for bash
fc756f336 Adding more symbols that should be excluded
fb616c542 Added a new class for handling the internals
7fb817448 Fix arithmetic shift operators
d81dd759c Auxiliary function to retrieve tail of trace and added dead command to trace
298740647 Bitwise operators for mpinteger
27153d142 Auxiliary function to check if the ssa has enough data to build an identifier
d47d503b6 Get symbol of member expression
6c0ff3217 Don't allowing functions called from _Start to be inlined
8809a4c56 Remove aa-symex from DIRS variable in Makefile
a30720b39 Improve failed test printer
ffef5d715 Add lazy conversion documentation
86bef2317 Use safe pointers for optional arguments
5c5bd7a43 Improve code style
9474d563d Add lazy loading tests
49105209d Style fixes
311806ecb Document lazy methods
2f47cba73 Add CBMC lazy-methods parameter
21decbb64 Make lazy method loading optional
93af0389f Don't try to call an abstract function
d20bdc644 Always assume String, Class and Object are callable
e12448b0d Lazy method conversion: load callee parent classes
49bfea4d8 Add this-parameter before determining needed classes
6e1133da8 Mark all classes in root jar reachable if it doesn't declare a main function
caf804e47 Restrict virtual method targets to known-created types
b7a7bfb17 Remove dead global variables
777d52e35 Convert Java methods only when they have a caller
895f8a695 Skip already-loaded Java classes
fdd81210c Fix failing travis tests after removal of aa-symex.
4fc57801c cleanup aa-path-symex and aa-symex
02df7f1c8 added test cases related to validate data from user using the ValidateInput class
b8f2f5a65 added test cases related to StringTokenizer object used to tokenize strings
47dbc2ed9 added test case…
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.
Replaces #950, adding cases for modulus-of-zero (e.g.
10 % 0) and excluding FP types from the exception, since div-by-zero yields infinity or NaN for such types.