Skip to content

Commit

Permalink
ebmc: hard error when giving an unknown property ID
Browse files Browse the repository at this point in the history
When giving an unknown property ID to --property, abort, as opposed to
continuing with an empty set of properties.
  • Loading branch information
kroening committed Oct 21, 2024
1 parent cdcc95f commit b3bb952
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 10 deletions.
7 changes: 7 additions & 0 deletions regression/ebmc/CLI/property-not-found1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
property-not-found1.sv
--property main.something
^error: Property main\.something not found$
^EXIT=6$
^SIGNAL=0$
--
5 changes: 5 additions & 0 deletions regression/ebmc/CLI/property-not-found1.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module main;

p0: assert final (0);

endmodule
11 changes: 2 additions & 9 deletions src/ebmc/ebmc_properties.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ ebmc_propertiest ebmc_propertiest::from_transition_system(
return properties;
}

bool ebmc_propertiest::select_property(
void ebmc_propertiest::select_property(
const cmdlinet &cmdline,
message_handlert &message_handler)
{
Expand All @@ -126,15 +126,8 @@ bool ebmc_propertiest::select_property(
}

if(!found)
{
messaget message(message_handler);
message.error() << "Property " << property << " not found"
<< messaget::eom;
return true;
}
throw ebmc_errort() << "Property " << property << " not found";
}

return false;
}

ebmc_propertiest ebmc_propertiest::from_command_line(
Expand Down
4 changes: 3 additions & 1 deletion src/ebmc/ebmc_properties.h
Original file line number Diff line number Diff line change
Expand Up @@ -195,7 +195,9 @@ class ebmc_propertiest
static ebmc_propertiest
from_transition_system(const transition_systemt &, message_handlert &);

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

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

0 comments on commit b3bb952

Please sign in to comment.