Skip to content

Updates to compiling instructions for GCC 6 #682

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.

Sign up for GitHub

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

Merged
merged 1 commit into from
Mar 24, 2017
Merged

Updates to compiling instructions for GCC 6 #682

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions COMPILING
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.

On Red Hat/Fedora or derivates, do

yum install gcc gcc-c++ flex bison perl-libwww-perl patch
yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
Copy link

Choose a reason for hiding this comment

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

I think that when you use devtoolset-6 you can remove some of dependencies. YUM should be fine with

yum install flex bison perl-libwww-perl patch devtoolset-6

Copy link
Author

Choose a reason for hiding this comment

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

Removing gcc and gcc-c++ makes the regression tests fail without the devtoolset-6 enabled. I cannot immediately see if this is a problem with the tests or with the cbmc binary. @kroening please let me know if you would like me to investigate further or you are happy with the instructions as is.


Note that you need g++ version 5.2 or newer.

Expand All @@ -48,13 +48,14 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.

cd cbmc-git/src
make minisat2-download
make
make CXX=g++-6

On Redhat/Fedora etc., do

cd cbmc-git/src
make minisat2-download
make CXX=g++-6
scl enable devtoolset-6 bash
Copy link

Choose a reason for hiding this comment

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

and then you probably need to run this before first make

Copy link
Author

Choose a reason for hiding this comment

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

agreed this is required, if the above requested change is made.

Copy link
Member

Choose a reason for hiding this comment

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

Yes, let's go for the "scl enable devtoolset-6 bash" change; it's better that the regressions work out-of-the box

Copy link
Author

Choose a reason for hiding this comment

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

In which case I am happy with the state of this PR. The version here will ensure that the regression tests run under most scenarios.

Please let me know if you need anything else.

make


COMPILATION ON SOLARIS 11
Expand Down