Skip to content

Commit 01c39cf

Browse files
authored
Merge pull request #782 from diffblue/property-not-found1
ebmc: hard error when giving an unknown property ID
2 parents 6d19481 + b3bb952 commit 01c39cf

File tree

4 files changed

+17
-10
lines changed

4 files changed

+17
-10
lines changed
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
property-not-found1.sv
3+
--property main.something
4+
^error: Property main\.something not found$
5+
^EXIT=6$
6+
^SIGNAL=0$
7+
--
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module main;
2+
3+
p0: assert final (0);
4+
5+
endmodule

src/ebmc/ebmc_properties.cpp

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
102102
return properties;
103103
}
104104

105-
bool ebmc_propertiest::select_property(
105+
void ebmc_propertiest::select_property(
106106
const cmdlinet &cmdline,
107107
message_handlert &message_handler)
108108
{
@@ -126,15 +126,8 @@ bool ebmc_propertiest::select_property(
126126
}
127127

128128
if(!found)
129-
{
130-
messaget message(message_handler);
131-
message.error() << "Property " << property << " not found"
132-
<< messaget::eom;
133-
return true;
134-
}
129+
throw ebmc_errort() << "Property " << property << " not found";
135130
}
136-
137-
return false;
138131
}
139132

140133
ebmc_propertiest ebmc_propertiest::from_command_line(

src/ebmc/ebmc_properties.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -195,7 +195,9 @@ class ebmc_propertiest
195195
static ebmc_propertiest
196196
from_transition_system(const transition_systemt &, message_handlert &);
197197

198-
bool select_property(const cmdlinet &, message_handlert &);
198+
/// Implements --property ID.
199+
/// Throws when given an unknown identifier.
200+
void select_property(const cmdlinet &, message_handlert &);
199201

200202
/// a map from property identifier to normalized expression
201203
std::map<irep_idt, exprt> make_property_map() const

0 commit comments

Comments
 (0)