File tree Expand file tree Collapse file tree 4 files changed +17
-10
lines changed
Expand file tree Collapse file tree 4 files changed +17
-10
lines changed Original file line number Diff line number Diff line change 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+ --
Original file line number Diff line number Diff line change 1+ module main ;
2+
3+ p0 : assert final (0 );
4+
5+ endmodule
Original file line number Diff line number Diff 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
140133ebmc_propertiest ebmc_propertiest::from_command_line (
Original file line number Diff line number Diff 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
You can’t perform that action at this time.
0 commit comments