Remove incomplete type constructors by kroening · Pull Request #2201 · diffblue/cbmc

kroening · 2018-05-18T14:57:43Z

This continues the campaign to remove "half-way" constructors that yield objects that violate obvious class invariants.

martin-cs

Seems like a good thing to have.

tautschnig · 2018-05-18T17:38:04Z

src/solvers/smt2/smt2_parser.cpp

  }

-  mathematical_function_typet result;
+  mathematical_function_typet result({}, nil_typet());


I'm not sure this is an improvement? Maybe the arguments should be collected first and the type be constructed once that's done?

tautschnig · 2018-05-18T17:38:41Z

src/java_bytecode/java_bytecode_convert_method.cpp

      if(cur_pc==it->handler_pc)
      {
-        if(catch_type!=typet() || it->catch_type==symbol_typet())
+        if(catch_type!=typet() || it->catch_type==symbol_typet(irep_idt()))


Nit pick: Please add spacing around !=, == while at it.

tautschnig · 2018-05-18T20:09:53Z

src/java_bytecode/java_bytecode_parse_tree.h

    public:
+      exceptiont():
+        start_pc(0), end_pc(0), handler_pc(0),
+        catch_type(irep_idt())


Nit-pick: clang-format will suggest a different formatting

tautschnig · 2018-05-18T20:10:13Z

src/java_bytecode/java_string_library_preprocess.cpp

  else
    UNREACHABLE;

+  assert(object_type.has_value());


Use INVARIANT

tautschnig · 2018-05-18T20:10:29Z

src/java_bytecode/java_string_library_preprocess.cpp

  // Check that the type of the object is in the symbol table,
  // otherwise there is no safe way of finding its value.
-  if(const auto maybe_symbol=symbol_table.lookup(object_type.get_identifier()))
+  if(const auto maybe_symbol=symbol_table.lookup(object_type->get_identifier()))


Nit pick: adjust spacing

kroening · 2018-05-19T08:40:06Z

All done

thk123 · 2018-05-21T08:46:17Z

Needs a TG bump before merging - will create.

thk123 · 2018-05-21T09:52:39Z

diffblue/test-gen#1831 - awaiting CI

thk123

This appears to have broken lambda beautification on TG. I can investigate this on Wednesday if you've not already looked at this before then.

thk123 · 2018-05-22T11:56:17Z

I'm not realistically going to get to this on Wednesday any more due to other priorities - let me know if this is going to be a problem.

peterschrammel

This is good to go. TG bump is passing.

reviewer on holiday

tautschnig · 2018-05-29T10:35:23Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

      if(cur_pc==it->handler_pc)
      {
-        if(catch_type!=typet() || it->catch_type==symbol_typet())
+        if(catch_type!=typet() || it->catch_type==symbol_typet(irep_idt()))


Nit-picking: add clang-format style spacing

tautschnig · 2018-05-29T10:35:53Z

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

  else
    UNREACHABLE;

+  assert(object_type.has_value());


INVARIANT

tautschnig · 2018-05-29T10:38:07Z

src/solvers/smt2/smt2_parser.cpp

  next_token(); // eat the ')'

-  result.codomain()=sort();
+  typet codomain=sort();


Nit-picking: add clang-format style spacing

tautschnig · 2018-05-29T10:38:15Z

src/solvers/smt2/smt2_parser.cpp

  next_token(); // eat the ')'

-  result.codomain()=sort();
+  typet codomain=sort();


Nit-picking: add clang-format style spacing

… object

kroening · 2018-05-29T16:34:10Z

All done

8de6a33 Merge pull request diffblue#2006 from tautschnig/opt-no-self-loops 6605699 Merge pull request diffblue#2217 from diffblue/c-preprocessing-cleanout f1d787b Merge pull request diffblue#2166 from tautschnig/out-of-bounds 25339d5 Add option not to transform self-loops into assumes 5e6a3af Merge pull request diffblue#2249 from tautschnig/attribute-used d3d888b Bounds check for flexible array members 41003e8 Handle negative byte_extract offsets efea5c4 Fix flattening of access beyond type-specified bounds 0ec87c8 Merge pull request diffblue#2271 from diffblue/letification 090790a Interpret GCC's attribute __used__ 7985716 Merge pull request diffblue#2252 from tautschnig/fresh-symbol-cleanup 022846a letify: use irep_hash_mapt when hashing is expensive 15dff7d Merge pull request diffblue#2260 from antlechner/antonia/annotation-class-value 9a0ffae added irep_hash_mapt da0adfe bugfix: irep_hash_containert now keeps a copy of the contained ireps 45436ce use std::size_t for container sizes 0c26a53 let_count_idt is now a struct e0a5142 Merge pull request diffblue#2206 from diffblue/use-get_identifier e0ad069 Add support for Java annotations with Class value 3817341 Merge pull request diffblue#2237 from smowton/smowton/feature/initialize-class-literals 25c097e use get_identifier() instead of get(ID_identifier) on symbols 4eda8ad Java class literals: init using a library hook when possible 70f13f3 Merge pull request diffblue#1906 from tautschnig/missing-return-semantics 57885a5 Merge pull request diffblue#1868 from tautschnig/fix-1867 b49822e Merge pull request diffblue#2028 from tautschnig/regression-fix 2815e84 Merge pull request diffblue#2259 from smowton/smowton/feature/note-abstract-methods 09b8cf7 Merge pull request diffblue#2014 from tautschnig/cadical-experiment f50237b Merge pull request diffblue#1967 from romainbrenguier/refactor/drop-constraint-inheritance2 3f951dd Merge pull request diffblue#2234 from nmanthey/upstream-fpr c6c2928 Drop inheritance from constraint on exprt 0ffd0ae Replace negation of constraint by a method f653dec use compiler defaults for gcc defines a31f530 remove need to do preprocessing on 16-bit test 24210e9 enable AWS Codebuild to do -m32 bfae4e3 enable Travis to do -m32 34a3d85 Merge pull request diffblue#2247 from antlechner/antonia/annotation-conversion 15ed961 Note when symbol-table entries are abstract methods 3a7135a Add module_dependencies.txt in test folder 1fa0b97 Generalize and rename does_annotation_exist 1db0af4 Define inverse function of convert_annotations ff25b2c get_max: do not parse every symbol name in the symbol table b603703 Add missing override 70da606 Merge pull request diffblue#2251 from tautschnig/rename-cleanup 49429cf Merge pull request diffblue#2257 from owen-jones-diffblue/owen-jones-diffblue/fix-cmake-macro 4b7a195 Improve naming of annotation variables 57d96e5 Fix CMake macro f9058e7 Merge pull request diffblue#2246 from diffblue/z3-fpa 6b0f265 Merge pull request diffblue#2248 from thk123/bugfix/doxygen-including-jbmc 72e99a0 Merge pull request diffblue#2201 from diffblue/remove-incomplete-type-constructors d4abbea smt2 implementation for popcount_exprt e8fa1c9 bswap_exprt now knows how many bits a byte has a6652d2 Merge pull request diffblue#2255 from tautschnig/speedup-no-pointer-check 4b0a2d6 goto_check: do not unnecessarily build size-of expressions 1fe7cd7 remove mathematical_typet() constructor, which produces an incomplete object 25d393b remove vector_typet() constructor, which produces an incomplete object e7c52e4 remove range_typet() constructor, which produces an incomplete object f92083d remove array_typet() constructor, which produces an incomplete object 72f63f3 remove tag_typet() constructor, which produces an incomplete object 516ed14 remove symbol_typet() constructor, which produces an incomplete object 4215f21 Consistently use get_fresh_aux_symbol instead of local implementations e6cd488 Remove unused goto_symext::new_name c24b820 Remove goto_convertt::lookup a816b26 Do not include rename.h when not using its functions 52ab088 called_functions: use unordered_set 157a12c Fix doxyfile to include JBMC documentation 026e93f function-pointer-removal: drop unused set b75fcbc smt2 implementation for bswap_exprt e276b27 Avoid extern/parameter name collisions in show-goto-functions/dump-c output 87c5948 C front-end: Record extern declarations in current scope a47941d perf-test: add -W/--witness-check to validate SV-COMP witness checking 5b0395f perf-test: Update Ubuntu AMI ids for latest version 1288ec7 perf-test: speed up builds just like e7bb127 did afccaec Provide goto-cc in performance tests f802d87 Support CaDiCaL in performance tests, remove redundant script 7872f7c Replace a missing return value by nondet 829068f Don't require the simplifier to solve this regression test git-subtree-dir: cbmc git-subtree-split: 8de6a33

kroening requested review from peterschrammel and tautschnig May 18, 2018 14:57

kroening requested review from cesaro, mgudemann, smowton and thk123 as code owners May 18, 2018 14:57

kroening force-pushed the remove-incomplete-type-constructors branch from e43efb2 to 75a7857 Compare May 18, 2018 15:16

kroening requested a review from martin-cs as a code owner May 18, 2018 15:16

kroening force-pushed the remove-incomplete-type-constructors branch 2 times, most recently from 911b14a to 93864a3 Compare May 18, 2018 17:00

martin-cs approved these changes May 18, 2018

View reviewed changes

tautschnig reviewed May 18, 2018

View reviewed changes

kroening force-pushed the remove-incomplete-type-constructors branch from 93864a3 to 73564b7 Compare May 19, 2018 08:39

kroening added the cleanup label May 20, 2018

thk123 added the do not merge label May 21, 2018

thk123 previously requested changes May 21, 2018

View reviewed changes

kroening force-pushed the remove-incomplete-type-constructors branch from 73564b7 to 2b66046 Compare May 22, 2018 10:18

kroening assigned thk123 May 26, 2018

peterschrammel force-pushed the remove-incomplete-type-constructors branch from 2b66046 to 154d288 Compare May 27, 2018 12:25

peterschrammel approved these changes May 27, 2018

View reviewed changes

peterschrammel removed the do not merge label May 27, 2018

peterschrammel assigned kroening and tautschnig and unassigned thk123 May 27, 2018

tautschnig reviewed May 29, 2018

View reviewed changes

tautschnig removed their assignment May 29, 2018

kroening added 6 commits May 29, 2018 17:34

remove symbol_typet() constructor, which produces an incomplete object

516ed14

remove tag_typet() constructor, which produces an incomplete object

72f63f3

remove array_typet() constructor, which produces an incomplete object

f92083d

remove range_typet() constructor, which produces an incomplete object

e7c52e4

remove vector_typet() constructor, which produces an incomplete object

25d393b

remove mathematical_typet() constructor, which produces an incomplete…

1fe7cd7

… object

kroening force-pushed the remove-incomplete-type-constructors branch from 154d288 to 1fe7cd7 Compare May 29, 2018 16:34

tautschnig approved these changes May 29, 2018

View reviewed changes

kroening merged commit 72e99a0 into develop May 30, 2018

kroening deleted the remove-incomplete-type-constructors branch May 30, 2018 11:52

Conversation

kroening commented May 18, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented May 19, 2018

Uh oh!

thk123 commented May 21, 2018

Uh oh!

thk123 commented May 21, 2018

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 commented May 22, 2018

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented May 29, 2018

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

kroening commented May 18, 2018 •

edited

Loading