replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Add option not to transform self-loops into assumes 

This allows disabling an optimisation in goto-symex
which is not compatible with termination checking.
This commit is contained in:
Peter Schrammel 2017-11-25 16:44:09 +00:00 committed by Michael Tautschnig
parent 5e6a3afeac
commit 25339d5e61
8 changed files with 44 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
jbmc/src/jbmc/jbmc_parse_options.cpp
View File

@ -152,6 +152,11 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
else
options.set_option("propagation", true);
// transform self loops to assumptions
options.set_option(
"self-loops-to-assumptions",
!cmdline.isset("no-self-loops-to-assumptions"));
// all checks supported by goto_check
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);

7
regression/cbmc/self_loops_to_assumptions1/default.desc Normal file
View File

@ -0,0 +1,7 @@
CORE
main.c
--unwind 1 --unwinding-assertions
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--

8
regression/cbmc/self_loops_to_assumptions1/main.c Normal file
View File

@ -0,0 +1,8 @@
int main()
{
while(1)
{
}
return 0;
}

7
regression/cbmc/self_loops_to_assumptions1/no-assume.desc Normal file
View File

@ -0,0 +1,7 @@
CORE
main.c
--unwind 1 --unwinding-assertions --no-self-loops-to-assumptions
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--

5
src/cbmc/bmc.h
View File

@ -84,6 +84,8 @@ public:
symex.constant_propagation=options.get_bool_option("propagation");
symex.record_coverage=
!options.get_option("symex-coverage-report").empty();
symex.self_loops_to_assumptions =
options.get_bool_option("self-loops-to-assumptions");
}
virtual resultt run(const goto_functionst &goto_functions)
@ -292,6 +294,7 @@ private:
"(unwinding-assertions)" \
"(no-unwinding-assertions)" \
"(no-pretty-names)" \
"(no-self-loops-to-assumptions)" \
"(partial-loops)" \
"(paths):" \
"(show-symex-strategies)" \
@ -315,6 +318,8 @@ private:
" --unwinding-assertions generate unwinding assertions (cannot be\n" \
" used with --cover or --partial-loops)\n" \
" --partial-loops permit paths with partial loops\n" \
" --no-self-loops-to-assumptions\n" \
" do not simplify while(1){} to assume(0)\n" \
" --no-pretty-names do not simplify identifiers\n" \
" --graphml-witness filename write the witness in GraphML format to " \
"filename\n" // NOLINT(*)

5
src/cbmc/cbmc_parse_options.cpp
View File

@ -227,6 +227,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
if(cmdline.isset("no-propagation"))
options.set_option("propagation", false);
// transform self loops to assumptions
options.set_option(
"self-loops-to-assumptions",
!cmdline.isset("no-self-loops-to-assumptions"));
// all checks supported by goto_check
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);

2
src/goto-symex/goto_symex.h
View File

@ -57,6 +57,7 @@ public:
total_vccs(0),
remaining_vccs(0),
constant_propagation(true),
self_loops_to_assumptions(true),
language_mode(),
outer_symbol_table(outer_symbol_table),
ns(outer_symbol_table),
@ -202,6 +203,7 @@ public:
unsigned total_vccs, remaining_vccs;
bool constant_propagation;
bool self_loops_to_assumptions;
optionst options;

8
src/goto-symex/symex_goto.cpp
View File

@ -58,9 +58,11 @@ void goto_symext::symex_goto(statet &state)
if(!forward) // backwards?
{
// is it label: goto label; or while(cond); - popular in SV-COMP
if(goto_target==state.source.pc ||
(instruction.incoming_edges.size()==1 &&
*instruction.incoming_edges.begin()==goto_target))
if(
self_loops_to_assumptions &&
(goto_target == state.source.pc ||
(instruction.incoming_edges.size() == 1 &&
*instruction.incoming_edges.begin() == goto_target)))
{
// generate assume(false) or a suitable negation if this
// instruction is a conditional goto