ctest.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_SYMEX_CTEST_H
#define CPROVER_GOTO_SYMEX_CTEST_H
 
#include <goto-symex/equation/symex_target_equation.h>
#include <util/symtab/namespace.h>
#include <string>
#include <vector>
#include <mutex>
 
class smt_convt;

class ctest_generator
{
private:
  struct test_variable
  {
    std::string verifier_type; // "int", "uint", "char", "uchar", "float", etc.
                               // for __VERIFIER_nondet_TYPE
    std::string c_type;        // C type: "int", "unsigned int", "float", etc.
    std::string value;         // The concrete value
  };
 
  std::vector<std::vector<test_variable>> test_cases;
  std::string function_name;
  std::vector<std::string> source_files;
  mutable std::mutex data_mutex;

  static std::string fingerprint(const std::vector<test_variable> &tc);

  std::string clean_variable_name(const std::string &name) const;

  std::string extract_function_name(
    const symex_target_equationt &target,
    smt_convt &smt_conv) const;

  std::string type_to_c_string(const type2tc &type) const;
  std::string type_to_verifier_string(const type2tc &type) const;

  std::string format_c_value(const expr2tc &value) const;
 
public:
  ctest_generator() = default;

  static constexpr const char *default_output_dir = "esbmc-ctest";

  void clear();

  void collect(
    const symex_target_equationt &target,
    smt_convt &smt_conv,
    const namespacet &ns);

  void generate(const std::string &output_dir) const;

  void generate_single(
    const std::string &output_dir,
    const symex_target_equationt &target,
    smt_convt &smt_conv,
    const namespacet &ns);

  bool has_tests() const;
};
 
#endif