Go to the documentation of this file.
60 std::string description,
62 : pc(pc), description(std::move(description)), status(status)
78 for(
const auto &function_pair : goto_functions.function_map)
80 const goto_programt &goto_program = function_pair.second.body;
85 if(!i_it->is_assert())
88 std::string description =
id2string(i_it->source_location.get_comment());
89 if(description.empty())
90 description =
"assertion";
92 i_it->source_location.get_property_id(),
107 xmlt xml_result(
"result");
113 template <
class json_
objectT>
115 json_objectT &result,
128 json<json_objectt>(result, property_id, property_info);
137 json<json_stream_objectt>(result, property_id, property_info);
159 std::size_t count = 0;
160 for(
const auto &property_pair : properties)
162 if(property_pair.second.status == status)
176 for(
const auto &property_pair : properties)
261 for(
const auto &property_pair : properties)
263 status &= property_pair.second.status;
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
@ FAIL
The property was violated.
property_statust
The status of a property.
#define CPROVER_EXIT_VERIFICATION_UNSAFE
Verification successful indicates the analysis has been performed without error AND the software is n...
resultt determine_result(const propertiest &properties)
Determines the overall result corresponding from the given properties That is PASS if all properties ...
@ ERROR
An error occurred during goto checking.
resultt
The result of goto verifying.
property_statust & operator|=(property_statust &a, property_statust const &b)
Update with the preference order.
#define CPROVER_EXIT_VERIFICATION_SAFE
Verification successful indicates the analysis has been performed without error AND the software is s...
@ PASS
No properties were violated.
@ UNKNOWN
No property was violated, neither was there an error.
@ NOT_REACHABLE
The property was proven to be unreachable.
void update_properties_from_goto_model(propertiest &properties, const abstract_goto_modelt &goto_model)
Updates properties with the assertions in goto_model.
std::string description
A description (usually derived from the assertion's comment)
@ FAIL
Some properties were violated.
propertiest initialize_properties(const abstract_goto_modelt &goto_model)
Returns the properties in the goto model.
property_statust status
The status of the property.
const std::string & id2string(const irep_idt &d)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
property_statust & operator&=(property_statust &a, property_statust const &b)
Update with the preference order.
#define PRECONDITION(CONDITION)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
@ NOT_CHECKED
The property was not checked (also used for initialization)
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
@ ERROR
An error occurred during goto checking.
@ UNKNOWN
The checker was unable to determine the status of the property.
Provides methods for streaming JSON objects.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
int result_to_exit_code(resultt result)
#define CPROVER_EXIT_VERIFICATION_INCONCLUSIVE
Verification inconclusive indicates the analysis has been performed without error AND the software is...
void set_attribute(const std::string &attribute, unsigned value)
Document and give macros for the exit codes of CPROVER binaries.
std::string as_string(resultt result)
A generic container class for the GOTO intermediate representation of one function.
@ PASS
The property was not violated.
instructionst::const_iterator const_targett
Abstract interface to eager or lazy GOTO models.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
#define forall_goto_program_instructions(it, program)
property_infot(goto_programt::const_targett pc, std::string description, property_statust status)