ansi-c: introduce typedef type #2641
Merged
Conversation
This file contains hidden or 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
kroening
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
martin-cs,
mgudemann,
NathanJPhillips,
peterschrammel,
pkesseli,
romainbrenguier,
smowton and
thk123
as code owners
|
Is this the third PR that includes the introduction of |
allredj
reviewed
Jul 31, 2018
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: a69575d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80490465
|
No, it simply depends on it -- i.e., look at the final commit only. |
kroening
force-pushed
the
typedef-type
branch
2 times, most recently
from
f65f3fb to
3329421
Compare
|
I've rebased onto develop, since #2205 is delayed. |
tautschnig
approved these changes
Aug 3, 2018
thk123
approved these changes
Aug 3, 2018
| template <> | ||
| inline bool can_cast_type<typedef_typet>(const typet &type) | ||
| { | ||
| return type.id() == ID_typedef_type; |
There was a problem hiding this comment.
If we introduce the method above the to_typedef_type methods we can de-duplicate the check (id() == ID_typedef_type) by replacing the preconditions with:
PRECONDITION(can_cast_type<typedef_typet>(type));Which will make it easier to add more robust checks in future.
| if(symbol.is_macro) | ||
| { | ||
| // overwrite, but preserve (add) any qualifiers and other flags | ||
| void c_typecheck_baset::typecheck_typedef_type(typet &type) |
There was a problem hiding this comment.
Why not take a typedef_typet to avoid the immediate cast (makes more consistent with typecheck_symbol_type as well).
There was a problem hiding this comment.
The typedef_type is replaced by whatever the typedef points to; i.e., you would violate the type invariant upon returning from this method.
| @@ -89,7 +90,9 @@ void c_typecheck_baset::typecheck_type(typet &type) | |||
| else if(type.id()==ID_typeof) | |||
| typecheck_typeof_type(type); | |||
| else if(type.id()==ID_symbol) | |||
| typecheck_symbol_type(type); | |||
| typecheck_symbol_type(to_symbol_type(type)); | |||
| else if(type.id() == ID_typedef_type) | |||
There was a problem hiding this comment.
Per coding standards use can_cast_typet<typedef_typet>(type) to hide direct id access.
| while(true) | ||
| { | ||
| typet &t=*p; | ||
|
|
||
| if(t.id()==ID_symbol) | ||
| if(t.id() == ID_typedef_type || t.id() == ID_symbol) |
There was a problem hiding this comment.
Per coding standards prefer using can_cast_typet<typedef_typet>
allredj
reviewed
Aug 3, 2018
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: b391c9e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80875063
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Aug 22, 2018
5d3ea03 Merge pull request diffblue#2693 from zhixing-xu/fix_rw_range_upper 2b40338 Update test.desc c6d0427 Merge pull request diffblue#2674 from diffblue/msvc-link 318474f Merge pull request diffblue#2678 from romainbrenguier/feature/extend-builtin-functions-part3 c63030f Regression test for goto-link personality 64fedd0 Microsoft LINK personality d9f9dd9 Merge pull request diffblue#2688 from tautschnig/concat-dir-file 99946fc Merge pull request diffblue#2675 from diffblue/goto-cl-echo-file 252d857 Merge pull request diffblue#2687 from tautschnig/fo-directory 0d7ebd5 Fixed a problem where the rw_set range's upper bound not set correctly 29eab32 goto-cl: Fail invocation of trying to compile multiple files to non-directory 7f587c4 Fix concat_dir_file for Windows and unit-test it a44468b Document string_builtin_function::eval ecc0e43 Document eval_is_upper_case a345d30 Document eval_string 58307a0 Tests for String.toUpperCase 71de2e3 Tests for String.toLowerCase 579d00c Remove redundant function application ID check e2961b5 Add builtin class for string_to_upper_case fe9071b Make to_upper_case work for Latin-1 supplement 53ccd3f Refactor string_to_upper_case be477c9 Remove assumptions that input char are < 0x100 836cbad Extract an is_upper_case function 1137ffd Improve documentation of add_axioms_for_to_lower_case a71f2c0 Implement builtin string_to_lower_case function fae6a48 Merge pull request diffblue#2467 from tautschnig/vs-except 24de513 Merge pull request diffblue#2474 from tautschnig/vs-identifier e14f2f2 Merge pull request diffblue#2685 from diffblue/clcache-again 08698cc Merge pull request diffblue#2681 from diffblue/remove-aig d42020b remove --aig option cd4a163 AWS codebuild windows: set clcache base directory 1ba928c cleanup unnecessary path from configuration file 8c4801b Refactor add_axioms_for_to_lower_case 4291232 Merge pull request diffblue#2686 from diffblue/buildspec-apt-cache 3adb717 AWS codebuild: cache apt lists and packages 0efb169 remove AIGs 3a9c825 Merge pull request diffblue#2682 from diffblue/fix-clcache b9b5660 Merge pull request diffblue#2483 from tautschnig/vs-java-parameters a66ab1e CL prints the name of the file that's compiled onto stdout 0698a5f Merge pull request diffblue#2673 from diffblue/goto-cl-Fo 75855bf Java front-end: remove unused parameters 4df2187 debugging output to resolve seg fault 5bc7456 goto-cl: /Fo can set an output directory a43e4fa add is_directory to file_util.h 4ad91fb Codebuild for windows: set up cache path properly effb01b Merge pull request diffblue#2641 from diffblue/typedef-type 5ef2802 Merge pull request diffblue#2679 from tautschnig/version-string 2efea52 Refine test patterns to avoid spurious matches aa7ebbc Merge pull request diffblue#2672 from diffblue/goto-cc-multiple-source-files aaea781 Merge pull request diffblue#2671 from diffblue/fix_get_base_name 8b51faf fix get_base_name 694daaf gcc mode: error in case multiple files are given with -c and -o 09fdca3 Merge pull request diffblue#2643 from svorenova/fixup-nondet-static d42054a Merge pull request diffblue#2669 from diffblue/spurious-cover-test b391c9e introduce typedef_type in the C frontend 114030b Merge pull request diffblue#2664 from romainbrenguier/feature/extend-builtin-functions-part2 46f6231 cbmc test no longer uses --cover daff1d1 Make nondet-static replace lines in CPROVER_init 1bca129 Merge pull request diffblue#2665 from tautschnig/gcc-conditional-stmt 31366ad Tests for StringBuilder.setCharAt f4285e7 Add builtin support for string_set_char 2a8ea0f Better specify out-of-bounds case for set_char 9415a24 Refactor add_axioms_for_set_char 9762886 Refactor string_concat_char builtin function b62bf01 Make nondet-static check for ID_C_no_nondet_initialization a50562e Mark java.lang.String.Literals with ID_C_constant b3c08d3 Mark internal Java variables with ID_C_no_nondet_initialization f2dc978 Add a new comment to mark variables that should not be nondet initialized da7966c Merge pull request diffblue#2645 from mmuesly/feature_test_posix_memalign cb4a340 Merge pull request diffblue#2647 from diffblue/cleanout-jar-filet 2b27a2d Merge pull request diffblue#2622 from martin-cs/feature/context-sensitive-ait-merge-2 00b26a8 Adds a test for posix_memalign in stdlib.c 0f5a057 Merge pull request diffblue#2667 from tautschnig/slicer-cleanup 16e6462 Remove no-longer-used ifdef 96d345b Clean GCC conditional expressions in right-hand sides of declarations 086c266 Merge pull request diffblue#2651 from smowton/smowton/feature/unroll-enum-clone-loops f69b244 Merge pull request diffblue#2625 from smowton/smowton/feature/value-set-accuracy 730b3e2 Merge pull request diffblue#2655 from romainbrenguier/feature/extend-builtin-functions c4569dd remove java_class_loader_limitt from jar_filet e0f954d Merge pull request diffblue#2659 from smowton/smowton/fix/cmake-third-time-is-charm 7f547b1 Merge pull request diffblue#2656 from smowton/smowton/fix/testsuite-name 3a1593b Tests for String.valueOf(int) 7414d76 Add builtin support for string_of_int 0b44c89 Add version of make_string accepting iterators f81f082 Rename function to add_axioms_for_string_of_int 9a2a7c2 Switch version.cpp from a rule product to a byproduct 943d60c Value set: handle with, array and struct expressions more accurately 4f158a3 Mark regression tests as expecting failure for symex driven loading c9a53f9 Add regression tests for changes to JBMC enumeration support a985eae Interpreter: deal with member-of-constant-struct expressions 361469b Change source location of jump target in {table|lookup}switch 6270968 java-unwind-enum-static: also unwind clone loop in Enum.values() 714de0d Symex: expose call stack to unwinding decision making fb239ef Fix jbmc-generic-symex-driven-lazy-loading test name 28ba192 Strengthen the invariant on what are acceptable function calls. 773bc86 Convert various comments, asserts and throws into invariants. e65f027 Add comments to the abstract interpreter interface. 1fe0796 Convert various older domains to use the more recent ait API. afe32b7 Refactor the methods that access "the abstract domain at a location". aa743b3 Remove unused exception name from catch statement 5703504 Remove unused parameter identifier git-subtree-dir: cbmc git-subtree-split: 5d3ea03
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.
Note that this change is invisible outside of the frontend.
The key benefit is to remove the ambiguity with struct/union/enum tags.