Skip to content

Replace get_mutable by goto_programt API function #362

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

Merged
merged 3 commits into from
Jan 3, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
39 changes: 17 additions & 22 deletions .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -5,44 +5,39 @@ sudo: required
matrix:
include:
- os: linux
dist: trusty
compiler: clang
compiler: gcc
addons:
apt:
sources:
- ubuntu-toolchain-r-test
packages:
# newer g++ version (also pulls libstdc++)
- g++-4.9
- libwww-perl
- g++-5
before_install:
- sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 90
env: COMPILER=g++-5
- os: linux
dist: trusty
compiler: gcc
compiler: clang
addons:
apt:
sources:
- ubuntu-toolchain-r-test
- llvm-toolchain-precise-3.7
packages:
# newer g++ version (also pulls libstdc++)
- g++-4.9
- libwww-perl
- clang-3.7
before_install:
- sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-4.9 90
- os: osx
compiler: clang
- sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/clang-3.7 90
env: COMPILER=clang++-3.7
- os: osx
compiler: gcc

addons:
apt:
packages:
- libwww-perl
env: COMPILER=g++
- os: osx
compiler: clang
env: COMPILER=clang++
- env: NAME="CPP-LINT"
script: DIFF=`git diff --name-only master HEAD` && if [ "$DIFF" != "" ]; then python scripts/cpplint.py $DIFF; fi

script:
- make -C src minisat2-download
- make -C src CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 && make -C regression test

matrix:
include:
- env: NAME="CPP-LINT"
script: DIFF=`git diff --name-only master HEAD` && if [ "$DIFF" != "" ]; then python scripts/cpplint.py $DIFF; fi
- make -C src CXX=$COMPILER CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 && make -C regression test
5 changes: 3 additions & 2 deletions src/goto-instrument/unwind.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ void goto_unwindt::unwind(
goto_programt::targett t_goto=goto_program.insert_before(loop_exit);
unwind_log.insert(t_goto, loop_exit->location_number);

t_goto->make_goto(get_mutable(goto_program, loop_exit));
t_goto->make_goto(goto_program.const_cast_target(loop_exit));
t_goto->source_location=loop_exit->source_location;
t_goto->function=loop_exit->function;
t_goto->guard=true_exprt();
Expand All @@ -269,7 +269,8 @@ void goto_unwindt::unwind(

// re-direct any branches that go to loop_head to loop_iter

for(goto_programt::targett t=get_mutable(goto_program, loop_head);
for(goto_programt::targett
t=goto_program.const_cast_target(loop_head);
t!=loop_iter; t++)
{
if(!t->is_goto())
Expand Down
7 changes: 0 additions & 7 deletions src/goto-instrument/unwind.h
Original file line number Diff line number Diff line change
Expand Up @@ -117,13 +117,6 @@ class goto_unwindt
const goto_programt::const_targett start,
const goto_programt::const_targett end, // exclusive
goto_programt &goto_program); // result

goto_programt::targett get_mutable(
goto_programt &goto_program,
const goto_programt::const_targett t) const
{
return goto_program.instructions.erase(t, t);
}
};

#endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H
13 changes: 13 additions & 0 deletions src/goto-programs/goto_program_template.h
Original file line number Diff line number Diff line change
Expand Up @@ -248,6 +248,19 @@ class goto_program_templatet
//! The list of instructions in the goto program
instructionst instructions;

// Convert a const_targett to a targett - use with care and avoid
// whenever possible
targett const_cast_target(const_targett t)
{
return instructions.erase(t, t);
}

// Dummy for templates with possible const contexts
const_targett const_cast_target(const_targett t) const
{
return t;
}

void get_successors(
targett target,
targetst &successors);
Expand Down