static_verifier.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: goto-analyzer
 
Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
\*******************************************************************/
 
#ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
#define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 
#include <goto-checker/properties.h>
 
#include <iosfwd>
 
#include <analyses/ai_history.h>
 
class abstract_goto_modelt;
class ai_baset;
class goto_modelt;
class message_handlert;
class optionst;
 
bool static_verifier(
  const goto_modelt &,
  const ai_baset &,
  const optionst &,
  message_handlert &,
  std::ostream &);
 
void static_verifier(
  const abstract_goto_modelt &abstract_goto_model,
  const ai_baset &ai,
  propertiest &properties);
 
enum class ai_verifier_statust
{
  TRUE,               // true : 1+, unknown :  0, false :  0
  FALSE_IF_REACHABLE, // true : 0+, unknown :  0, false : 1+
  NOT_REACHABLE,      // true :  0, unknown :  0, false :  0
  UNKNOWN             // true : 0+, unknown : 1+, false : 0+
};
 
std::string as_string(const ai_verifier_statust &);
 
class static_verifier_resultt
{
public:
  ai_verifier_statust status;
  source_locationt source_location;
  irep_idt function_id;
  ai_history_baset::trace_sett unknown_histories;
  ai_history_baset::trace_sett false_histories;
 
  static_verifier_resultt(
    const ai_baset &ai,
    goto_programt::const_targett assert_location,
    irep_idt func_id,
    const namespacet &ns);
 
  jsont output_json(void) const;
  xmlt output_xml(void) const;
};
 
#endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H