Go to the documentation of this file.
43 case property_statust::NOT_CHECKED:
47 case property_statust::NOT_REACHABLE:
49 case property_statust::PASS:
51 case property_statust::FAIL:
62 std::string description,
64 : pc(pc), description(std::move(description)), status(status)
80 for(
const auto &function_pair : goto_functions.function_map)
82 const goto_programt &goto_program = function_pair.second.body;
87 if(!i_it->is_assert())
90 std::string description =
id2string(i_it->source_location.get_comment());
91 if(description.empty())
92 description =
"assertion";
94 i_it->source_location.get_property_id(),
109 xmlt xml_result(
"result");
115 template <
class json_
objectT>
117 json_objectT &result,
130 json<json_objectt>(result, property_id, property_info);
139 json<json_stream_objectt>(result, property_id, property_info);
161 std::size_t count = 0;
162 for(
const auto &property_pair : properties)
164 if(property_pair.second.status == status)
172 return status == property_statust::NOT_CHECKED ||
178 for(
const auto &property_pair : properties)
198 a == property_statust::NOT_CHECKED ||
205 case property_statust::NOT_CHECKED:
210 case property_statust::PASS:
211 case property_statust::NOT_REACHABLE:
212 case property_statust::FAIL:
232 case property_statust::FAIL:
238 case property_statust::NOT_CHECKED:
240 (b != property_statust::PASS && b != property_statust::NOT_REACHABLE ? b
243 case property_statust::NOT_REACHABLE:
244 a = (b != property_statust::PASS ? b : a);
246 case property_statust::PASS:
247 a = (b == property_statust::PASS ? a : b);
262 for(
const auto &property_pair : properties)
264 status &= property_pair.second.status;
268 case property_statust::NOT_CHECKED:
273 case property_statust::NOT_REACHABLE:
275 return resultt::PASS;
276 case property_statust::PASS:
277 return resultt::PASS;
278 case property_statust::FAIL:
279 return resultt::FAIL;
#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.
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...
@ UNKNOWN
No property was violated, neither was there an error.
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)
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)
Abstract interface to eager or lazy GOTO models.
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.
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.
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)