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

set multiple error labels 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5001 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2015-01-05 12:43:10 +00:00
parent d95d36ed76
commit 47f6881aad
4 changed files with 38 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
regression/cbmc/Error_Label3/main.c Normal file
View File

@ -0,0 +1,10 @@
int main()
{
int i;
goto ERROR2;
return 0;
ERROR1:;
ERROR2:;
}

8
regression/cbmc/Error_Label3/test.desc Normal file
View File

@ -0,0 +1,8 @@
CORE
main.c
--error-label ERROR1 --error-label ERROR2
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^warning: ignoring

17
src/analyses/goto_check.cpp
View File

@ -47,7 +47,7 @@ public:
enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
enable_assertions=_options.get_bool_option("assertions");
enable_assumptions=_options.get_bool_option("assumptions");
error_label=_options.get_option("error-label");
error_labels=_options.get_list_option("error-label");
}
typedef goto_functionst::goto_functiont goto_functiont;
@ -115,7 +115,9 @@ protected:
bool enable_assert_to_assume;
bool enable_assertions;
bool enable_assumptions;
irep_idt error_label;
typedef optionst::value_listt error_labelst;
error_labelst error_labels;
};
/*******************************************************************\
@ -1454,8 +1456,12 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
check(i.guard);
// magic ERROR label?
if(error_label!=irep_idt() &&
std::find(i.labels.begin(), i.labels.end(), error_label)!=i.labels.end())
for(optionst::value_listt::const_iterator
l_it=error_labels.begin();
l_it!=error_labels.end();
l_it++)
{
if(std::find(i.labels.begin(), i.labels.end(), *l_it)!=i.labels.end())
{
goto_program_instruction_typet type=
enable_assert_to_assume?ASSUME:ASSERT;
@ -1465,9 +1471,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
t->guard=false_exprt();
t->source_location=i.source_location;
t->source_location.set_property_class("error label");
t->source_location.set_comment("error label");
t->source_location.set_comment("error label "+*l_it);
t->source_location.set("user-provided", true);
}
}
if(i.is_other())
{

2
src/cbmc/cbmc_parseoptions.cpp
View File

@ -240,7 +240,7 @@ void cbmc_parseoptionst::get_command_line_options(optionst &options)
// magic error label
if(cmdline.isset("error-label"))
options.set_option("error-label", cmdline.get_value("error-label"));
options.set_option("error-label", cmdline.get_values("error-label"));
// generate unwinding assertions
if(cmdline.isset("cover-assertions"))