Skip to content

Property reporting utilities [blocks: 3584] #3583

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Jan 14, 2019
Merged

Property reporting utilities [blocks: 3584] #3583

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
cc1a90e
Add count_properties with given result
peterschrammel Dec 16, 2018
4da669d
Add property output functions
peterschrammel Dec 16, 2018
519fb98
Add report_util for outputting verification results
peterschrammel Dec 16, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions src/goto-checker/properties.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
#include "properties.h"

#include <util/invariant.h>
#include <util/json.h>
#include <util/xml.h>

std::string as_string(resultt result)
{
Expand Down Expand Up @@ -89,6 +91,31 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model)
return properties;
}

std::string
as_string(const irep_idt &property_id, const property_infot &property_info)
{
return "[" + id2string(property_id) + "] " + property_info.description +
": " + as_string(property_info.status);
}

xmlt xml(const irep_idt &property_id, const property_infot &property_info)
{
xmlt xml_result("result");
xml_result.set_attribute("property", id2string(property_id));
xml_result.set_attribute("status", as_string(property_info.status));
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing description

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's what we are doing at the moment: https://github.com/diffblue/cbmc/blob/develop/src/cbmc/all_properties.cpp#L258

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It still seems wrong.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Filed as #3798.

return xml_result;
}

json_objectt
json(const irep_idt &property_id, const property_infot &property_info)
{
json_objectt result;
result["property"] = json_stringt(property_id);
result["description"] = json_stringt(property_info.description);
result["status"] = json_stringt(as_string(property_info.status));
return result;
}

std::size_t
count_properties(const propertiest &properties, property_statust status)
{
Expand Down
11 changes: 11 additions & 0 deletions src/goto-checker/properties.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,9 @@ Author: Daniel Kroening, Peter Schrammel

#include <goto-programs/goto_model.h>

class json_objectt;
class xmlt;

/// The status of a property
enum class property_statust
{
Expand Down Expand Up @@ -73,6 +76,14 @@ typedef std::unordered_map<irep_idt, property_infot> propertiest;
/// Returns the properties in the goto model
propertiest initialize_properties(const abstract_goto_modelt &);

std::string
as_string(const irep_idt &property_id, const property_infot &property_info);

xmlt xml(const irep_idt &property_id, const property_infot &property_info);

json_objectt
json(const irep_idt &property_id, const property_infot &property_info);

/// Return the number of properties with given \p status
std::size_t count_properties(const propertiest &, property_statust);

Expand Down