Skip to content

Commit

Permalink
WIP, create PRs
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Dec 19, 2023
1 parent 65e1cc9 commit 93a6b22
Show file tree
Hide file tree
Showing 6 changed files with 4 additions and 14 deletions.
4 changes: 2 additions & 2 deletions src/analyses/ai.h
Original file line number Diff line number Diff line change
Expand Up @@ -589,7 +589,7 @@ class ait : public ai_recursive_interproceduralt
// Not recommended as it will throw an exception if a location has not
// been reached in an analysis and there is no (other) way of telling
// if a location has been reached.
DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
// DEPRECATED(SINCE(2019, 08, 01, "use abstract_state_{before,after} instead"))
const domainT &operator[](locationt l) const
{
auto p = storage->abstract_state_before(l, *domain_factory);
Expand All @@ -607,7 +607,7 @@ class ait : public ai_recursive_interproceduralt
// Support the legacy get_state interface which is needed for a few domains
// This is one of the few users of the legacy get_state(locationt) method
// in location_sensitive_storaget.
DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
// DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
virtual statet &get_state(locationt l)
{
auto &s = dynamic_cast<location_sensitive_storaget &>(*storage);
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/ai_storage.h
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,7 @@ class location_sensitive_storaget : public trace_map_storaget
// Care should be exercised in using this. It is possible to create domains
// without any corresponding history object(s). This can lead to somewhat
// unexpected behaviour depending on which APIs you use.
DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
// DEPRECATED(SINCE(2019, 08, 01, "use get_state(trace_ptrt p) instead"))
statet &get_state(locationt l, const ai_domain_factory_baset &fac)
{
typename state_mapt::const_iterator it = state_map.find(l);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,6 @@ class dfcc_is_freeablet
protected:
dfcc_libraryt &library;
message_handlert &message_handler;
messaget log;
};

#endif
5 changes: 0 additions & 5 deletions src/goto-programs/safety_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,6 @@ Author: Daniel Kroening, [email protected]

#include "safety_checker.h"

safety_checkert::safety_checkert(const namespacet &_ns):
ns(_ns)
{
}

safety_checkert::safety_checkert(
const namespacet &_ns,
message_handlert &_message_handler):
Expand Down
3 changes: 0 additions & 3 deletions src/goto-programs/safety_checker.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,9 +24,6 @@ class goto_functionst;
class safety_checkert:public messaget
{
public:
explicit safety_checkert(
const namespacet &_ns);

explicit safety_checkert(
const namespacet &_ns,
message_handlert &_message_handler);
Expand Down
3 changes: 1 addition & 2 deletions src/jsil/jsil_entry_point.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -154,8 +154,7 @@ bool jsil_entry_point(

if(!symbol_table.insert(std::move(new_symbol)).second)
{
messaget message;
message.set_message_handler(message_handler);
messaget message{message_handler};
message.error() << "failed to move main symbol" << messaget::eom;
return true;
}
Expand Down

0 comments on commit 93a6b22

Please sign in to comment.