Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove unused files #1321

Merged
merged 1 commit into from
Sep 8, 2017
Merged

Conversation

reuk
Copy link
Contributor

@reuk reuk commented Sep 1, 2017

Several files are never mentioned in any makefiles, and therefore are not built. This patch removes these unused files.

@tautschnig tautschnig requested a review from kroening September 1, 2017 10:08
@tautschnig
Copy link
Collaborator

@reuk Thanks a lot for this cleanup work. I believe the unit tests ought to be converted to Catch-based ones and it may thus be worth holding off on their removal. See #921. For various other files @kroening's opinion is essential.

@reuk reuk force-pushed the reuk/remove-unused-files branch from f52b833 to 0ad63b7 Compare September 1, 2017 10:52
@reuk
Copy link
Contributor Author

reuk commented Sep 1, 2017

Modified to keep unit tests.

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems like a zero-risk change since the files are always in source control. Suggest merge now then when @kroening has time to review can reinstate any if necessary (preferably by adding them to the Makefiles!)

@kroening
Copy link
Member

kroening commented Sep 7, 2017

We'll want to keep
src/solvers/floatbv/float_approximation.cpp/.h
and the satcheck_limmat.h/.cpp
files for now; the rest can go away.

@kroening kroening assigned reuk and unassigned kroening Sep 7, 2017
@tautschnig
Copy link
Collaborator

@reuk could you please add the files indicated by @kroening to the Makefiles to make intent explicit? Thank you!

@reuk
Copy link
Contributor Author

reuk commented Sep 7, 2017

I will if they build. If they don't I'll create an issue to fix them, but I'll leave them out of the makefiles for the time being.

@reuk reuk force-pushed the reuk/remove-unused-files branch 2 times, most recently from b69ed43 to b61e76f Compare September 7, 2017 14:14
@reuk
Copy link
Contributor Author

reuk commented Sep 7, 2017

I can get floatbv_approximation to build, but not satcheck_limmat.cpp, which depends on a header "limmat.h" which I can't find anywhere.

Ready for re-review.

@tautschnig
Copy link
Collaborator

Thank you!

Would you mind adding

ifneq ($(LIMMAT),)
  LIMMAT_SRC=sat/satcheck_limmat.cpp
  LIMMAT_INCLUDE=-I $(LIMMAT)
  LIMMAT_LIB=$(LIMMAT)/liblimmat$(LIBEXT)
  CP_CXXFLAGS += -DHAVE_LIMMAT
endif

and add $(LIMMAT_SRC) to SRC = ... in solvers/Makefile?

(You've already got my approval anyway.)

@reuk reuk force-pushed the reuk/remove-unused-files branch from b61e76f to 2217501 Compare September 7, 2017 15:35
@reuk
Copy link
Contributor Author

reuk commented Sep 8, 2017

I've made the requested change

@tautschnig tautschnig merged commit 435c0bf into diffblue:develop Sep 8, 2017
reuk added a commit to reuk/cbmc that referenced this pull request Sep 11, 2017
@reuk reuk deleted the reuk/remove-unused-files branch September 14, 2017 16:58
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
08f269c Merge pull request diffblue#1388 from smowton/merge-develop-20170914
e3f3abd Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914
4df244c Merge pull request diffblue#1383 from reuk/reuk/sync-projects
f25db0a Merge pull request diffblue#189 from diffblue/smowton/fix/remove_debug_code
1fae64c Remove stray use of overlay_map
1264b4d Re-enable old function signatures for test-gen compat
e54c0e9 Merge pull request diffblue#338 from thk123/bug/function-flag-on-goto-program
63c9a1e Merge pull request diffblue#1374 from reuk/reuk/maintain-pointer-invariants
00e4555 Fix up CMake build (unrelated)
81f1300 Use PRECONDITION in std_types.h
a9806c0 Ensure pointer invariants are maintained
a46ad62 Regenerate malformed binary blobs
f77822b Merge pull request diffblue#1380 from diffblue/remove-musketeer
22f06fd Correcting windows build
3ede81b Merge pull request diffblue#1293 from reuk/cmake-develop
92a52a5 Corrected doxygen errors
c6f1430 Ensure symex and goto-analyzer regenerate functions
e37d3d5 Disable failing test in the symex directory
15b89fc Weaked the tests for pointer-function-parameters
dee89b0 Fixing the method to work with java_bytecode
1ccd1a2 Add support for using the --function flag to goto-analyze and symex
0732580 Adding missing overrides
71dec3d Use ID_main as the default name for entry function
2aea88d Made generate_start_function abstract
f0d6d72 Refactored the regenerate function into goto-programs
71e6800 Added regression test for using --function on a GOTO program
94b7185 Implemented generate_start_function for Java
cd416bc Call generate_start_function only when regenerating the start function
ee5fb93 Protect against invalid function label
2a3d876 Adding explanatory comment
f347a22 Cause a regeneration of the entry method if a --function is provided
69d05a9 Merge pull request diffblue#1382 from pkesseli/bugfix/language-opaque-stubs
d45325c Merge pull request diffblue#1378 from thk123/bugfix/fix-symex-appveyor
444f256 Add initial value to languaget::generate_opaque_stubs
91e733d Manually disable some failing tests
41bafc0 Merge pull request diffblue#1375 from pkesseli/bugfix/uncaught-exceptions-invariant
a31f1d9 remove musketeer
af8d46f Reverting manually commited fixes
e73a884 Attempt to fix the symex appveyor build
0496142 Account for replaced functions in exceptions_map
2816b80 revert symex regression until Appvoyer works
6a2fd50 added symex to Appveyor build
a2834d0 Map wrappers: forward more of the std::map interface
0a668ae Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2
8cd4490 Merge pull request diffblue#1373 from diffblue/symex-trace-fix
5d2d07b enable symex regression testing
5195d24 avoid confusion between SSA lhs and full lhs during assignment
430218f option is now --trace
746bff5 remove_returns missing in symex
211355d comments on test
3896110 output statements
8fc714d use __CPROVER_assert
728ac5b Merge pull request diffblue#1367 from reuk/reuk/disable-alpine-in-travis
73b4357 Merge pull request diffblue#1339 from diffblue/initialize_goto_model
4febd10 Merge pull request diffblue#1364 from diffblue/phread-create-fix
0cfd7b0 Remove PRE_COMMAND scaffolding
04b4f63 Merge pull request diffblue#186 from diffblue/cleanup/misc
577fa6c Tightened up usage of maps
8782103 Merge pull request diffblue#1365 from smowton/smowton/feature/more_map_forwarding
4dde3c5 Disable glucose in Travis
91684da Clean up CMake files after diffblue#1321
7d4e9b5 Make CMake release flags similar to Makefile build
5ee349f Control SAT library from makefiles
ad486f8 Set up glucose externalproject
5afa929 Quote paths in flex/bison commands
9afbced Disable 32-bit builds in Travis
d953327 Enable caching for CMake builds (hopefully)
6251055 Fix and refactor library_check target
3c36aa5 Enable CMake in Travis
f6e4968 Enable running tests from CMake
e609bbb Add CMake howto to COMPILING file
22c2ab9 Add CMakeLists
6facf74 Map wrappers: forward more of the std::map interface
b846858 Merge pull request diffblue#1291 from LAJW/optional
3ddd377 clean-out ill-modeled optimization in string comparisons
95c5e63 Disable Alpine in Travis
fe60e60 pthread_create arguments null/nonnull fix
7d30cde missing copyright header
8c4ff7b remove spurious references to langapi/language_ui.h
e4498ca brief list of symbols, from language_uit
fc4d44a use goto_modelt
9469552 use initialize_goto_model in CBMC/goto-analyse/etc
40fe0f8 simplify API of goto_convert
40557df Used range iterators
d4e89fd Tidy up symbol_tablet::move
c125146 Merge pull request diffblue#1245 from tautschnig/run-diagnostic
435c0bf Merge pull request diffblue#1321 from reuk/reuk/remove-unused-files
08a4077 Make the child process that failed to execvp exit
4928f69 Diagnostic output if run/execve fails
5863a75 Merge pull request diffblue#1333 from tautschnig/remove-c_sizeof
498718f Code readability
2217501 Remove unused files
1c8d81a Merge pull request diffblue#1356 from smowton/smowton/feature/test_pl_add_dry_run
56b5e25 Merge pull request diffblue#1358 from thk123/feature/decrease-message-spam
359a3e3 Modified verbosity for loaded message
296349c Add dry-run mode to test.pl
f6d94cf clean out an unused method
3613ebc When possible, update array types before typechecking initializer
3273bf5 Fix type casts from initializer lists to arrays of unspecified size
1fa569f sizeof(*(void*)) is sizeof(char)
d79067e Remove long-deprecated c_sizeof in favour of size_of_expr et al.
254f133 Merge pull request diffblue#1323 from janmroczkowski/janmroczkowski/goto_modelt-output-const
388a25e Make uncaught_exceptions_analysis.output const
211fcc2 Make path_nodet.output const
9be84ea Make automatont.output const
567eaa7 Make basic_blockst.output const
ebbbf5f Make goto_modelt.output const
ae584df Move optional unit tests into util directory
4dbf939 Manually fix optional
43d0602 Add unit tests for nonstd::optional
8584bb0 Add nonstd/optional.hpp library
281e384 Workaround for travis performing shallow clones with wrong branch

git-subtree-dir: cbmc
git-subtree-split: 08f269c
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants