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