test_gen_guard.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_SYMEX_TEST_GEN_GUARD_H
#define CPROVER_GOTO_SYMEX_TEST_GEN_GUARD_H
 
#include <util/message/message.h>
 
#include <filesystem>
#include <fstream>
#include <string>
#include <vector>

inline constexpr char ESBMC_GENERATED_MARKER[] = "Auto-generated by ESBMC";
 
enum class overwrite_verdict
{
  safe,
  foreign,
  unreadable
};

inline overwrite_verdict classify_existing(const std::filesystem::path &path)
{
  std::ifstream in(path);
  if (!in)
    return overwrite_verdict::unreadable;
  std::string first_line;
  if (!std::getline(in, first_line))
    return overwrite_verdict::safe;
  return first_line.find(ESBMC_GENERATED_MARKER) != std::string::npos
           ? overwrite_verdict::safe
           : overwrite_verdict::foreign;
}

inline bool can_write_all(
  const std::vector<std::filesystem::path> &paths,
  const std::string &option_name)
{
  for (const auto &path : paths)
  {
    std::error_code ec;
    if (!std::filesystem::exists(path, ec))
      continue;
 
    switch (classify_existing(path))
    {
    case overwrite_verdict::safe:
      break;
    case overwrite_verdict::foreign:
      log_error(
        "{} was not generated by ESBMC; refusing to overwrite it. Pass "
        "{} <dir> to generate elsewhere.",
        path.string(),
        option_name);
      return false;
    case overwrite_verdict::unreadable:
      log_error(
        "cannot read {} to check whether it is safe to overwrite; refusing. "
        "Pass {} <dir> to generate elsewhere.",
        path.string(),
        option_name);
      return false;
    }
  }
  return true;
}
 
#endif