pytest.h

Go to the documentation of this file.

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

class pytest_generator
{
private:
  std::vector<std::vector<std::string>> test_cases;
  std::vector<std::string> param_names;
  std::string function_name;
  mutable std::mutex data_mutex;

  bool values_only = false;

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

  void write_test_body(
    std::ofstream &file,
    const std::string &module_name,
    const std::string &func_name,
    const std::vector<std::string> &param_names,
    const std::vector<std::vector<std::string>> &test_data) const;

  void write_witness(
    std::ofstream &file,
    const std::vector<std::string> &param_names,
    const std::vector<std::vector<std::string>> &test_data) const;

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

  std::string convert_float_to_python(const std::string &c_float) const;

  std::string escape_python_string(const std::string &str) const;

  std::string convert_array_to_python_list(const expr2tc &array_expr) const;

  std::string convert_struct_to_python_dict(const expr2tc &struct_expr) const;

  bool is_char_array(const expr2tc &array_expr) const;

  std::string convert_char_array_to_string(const expr2tc &array_expr) const;

  void write_file_header(std::ofstream &file, const std::string &original_file)
    const;

  void write_imports(std::ofstream &file, const std::string &module_name) const;

  static std::string build_param_list(const std::vector<std::string> &params);

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

  void write_test_data(
    std::ofstream &file,
    const std::vector<std::string> &param_names,
    const std::vector<std::vector<std::string>> &test_data) const;

  void write_test_function(
    std::ofstream &file,
    const std::string &func_name,
    const std::vector<std::string> &param_names) const;
 
public:
  pytest_generator() = default;

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

  static std::string extract_module_name(const std::string &input_file);

  static std::string generate_pytest_filename(const std::string &module_name);

  void clear();

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

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

  void set_values_only(bool enabled)
  {
    values_only = enabled;
  }
 
  void generate_single(
    const std::string &output_dir,
    const std::string &file_name,
    const symex_target_equationt &target,
    smt_convt &smt_conv,
    const namespacet &ns);

  bool has_tests() const;
};
 
#endif