diff --git a/.travis.yml b/.travis.yml index ffbfb288b96..2957786e6cd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -99,6 +99,7 @@ jobs: - libubsan0 - parallel - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-5 bin/gcc @@ -115,7 +116,7 @@ jobs: compiler: clang cache: ccache before_install: - - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel + - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel gdb - export PATH=$PATH:/usr/local/opt/ccache/libexec env: COMPILER="ccache clang++" @@ -134,6 +135,7 @@ jobs: - g++-5 - libubsan0 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-5 bin/gcc @@ -162,6 +164,7 @@ jobs: - libstdc++-5-dev - libubsan0 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-5 bin/gcc @@ -189,6 +192,7 @@ jobs: packages: - g++-7 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-7 bin/gcc @@ -216,6 +220,7 @@ jobs: packages: - g++-7 - jq + - gdb before_install: - mkdir bin - ln -s /usr/bin/gcc-7 bin/gcc @@ -249,6 +254,7 @@ jobs: - libubsan0 - parallel - jq + - gdb before_install: - mkdir bin # Use gcc/g++ 5 for tests, as Clang doesn't work yet @@ -270,7 +276,7 @@ jobs: compiler: clang cache: ccache before_install: - - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache + - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache gdb - export PATH=$PATH:/usr/local/opt/ccache/libexec env: - BUILD_SYSTEM=cmake diff --git a/buildspec.yml b/buildspec.yml index 975e3eea7a7..6394753b0e7 100644 --- a/buildspec.yml +++ b/buildspec.yml @@ -8,7 +8,7 @@ phases: - apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F - add-apt-repository ppa:openjdk-r/ppa -y - apt-get update -y - - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache libc6-dev-i386 jq + - apt-get install -y g++-5 flex bison make git libwww-perl patch ccache libc6-dev-i386 jq gdb - apt-get install -y openjdk-8-jdk - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1 - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1 diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp new file mode 100644 index 00000000000..4a1e452f2df --- /dev/null +++ b/src/memory-analyzer/gdb_api.cpp @@ -0,0 +1,503 @@ +/*******************************************************************\ + +Module: GDB Machine Interface API + +Author: Malte Mues + Daniel Poetzl + +\*******************************************************************/ + +/// \file +/// Low-level interface to gdb + +// clang-format off +#if defined(__linux__) || \ + defined(__FreeBSD_kernel__) || \ + defined(__GNU__) || \ + defined(__unix__) || \ + defined(__CYGWIN__) || \ + defined(__MACH__) +// clang-format on + +#include +#include +#include +#include +#include + +#include "gdb_api.h" + +#include + +#include +#include + +#include + +/// Create a gdb_apit object +/// +/// \param binary the binary to run with gdb +/// \param log boolean indicating whether gdb input and output should be logged +gdb_apit::gdb_apit(const char *binary, const bool log) + : binary(binary), log(log), gdb_state(gdb_statet::NOT_CREATED) +{ +} + +/// Terminate the gdb process and close open streams (for reading from and +/// writing to gdb) +gdb_apit::~gdb_apit() +{ + PRECONDITION( + gdb_state == gdb_statet::CREATED || gdb_state == gdb_statet::STOPPED || + gdb_state == gdb_statet::NOT_CREATED); + + if(gdb_state == gdb_statet::NOT_CREATED) + return; + + write_to_gdb("-gdb-exit"); + // we cannot use most_recent_line_has_tag() here as it checks the last line + // before the next `(gdb) \n` prompt in the output; however when gdb exits no + // next prompt is printed + CHECK_RETURN(has_prefix(read_next_line(), "^exit")); + + gdb_state = gdb_statet::NOT_CREATED; + + fclose(command_stream); + fclose(response_stream); + + wait(NULL); +} + +/// Create a new gdb process for analysing the binary indicated by the member +/// variable `binary` +void gdb_apit::create_gdb_process() +{ + PRECONDITION(gdb_state == gdb_statet::NOT_CREATED); + + command_log.clear(); + + pid_t gdb_process; + + int pipe_input[2]; + int pipe_output[2]; + + if(pipe(pipe_input) == -1) + { + throw gdb_interaction_exceptiont("could not create pipe for stdin"); + } + + if(pipe(pipe_output) == -1) + { + throw gdb_interaction_exceptiont("could not create pipe for stdout"); + } + + gdb_process = fork(); + + if(gdb_process == -1) + { + throw gdb_interaction_exceptiont("could not create gdb process"); + } + + if(gdb_process == 0) + { + // child process + close(pipe_input[1]); + close(pipe_output[0]); + + dup2(pipe_input[0], STDIN_FILENO); + dup2(pipe_output[1], STDOUT_FILENO); + dup2(pipe_output[1], STDERR_FILENO); + + dprintf(pipe_output[1], "binary name: %s\n", binary); + + char *const arg[] = {const_cast("gdb"), + const_cast("--interpreter=mi"), + const_cast(binary), + NULL}; + + dprintf(pipe_output[1], "Loading gdb...\n"); + execvp("gdb", arg); + + // Only reachable, if execvp failed + int errno_value = errno; + dprintf(pipe_output[1], "errno in child: %s\n", strerror(errno_value)); + } + else + { + // parent process + gdb_state = gdb_statet::CREATED; + + close(pipe_input[0]); + close(pipe_output[1]); + + // get stream for reading the gdb output + response_stream = fdopen(pipe_output[0], "r"); + + // get stream for writing to gdb + command_stream = fdopen(pipe_input[1], "w"); + + bool has_done_tag = most_recent_line_has_tag(R"(~"done)"); + CHECK_RETURN(has_done_tag); + + if(log) + { + // logs output to `gdb.txt` in the current directory, input is not logged + // hence we log it to `command_log` + write_to_gdb("-gdb-set logging on"); + check_command_accepted(); + } + + write_to_gdb("-gdb-set max-value-size unlimited"); + check_command_accepted(); + } +} + +void gdb_apit::write_to_gdb(const std::string &command) +{ + PRECONDITION(!command.empty()); + PRECONDITION(command.find('\n') == std::string::npos); + + std::string line(command); + line += '\n'; + + if(log) + { + command_log.push_front(command); + } + + if(fputs(line.c_str(), command_stream) == EOF) + { + throw gdb_interaction_exceptiont("could not write a command to gdb"); + } + + fflush(command_stream); +} + +/// Return the vector of commands that have been written to gdb so far +const gdb_apit::commandst &gdb_apit::get_command_log() +{ + PRECONDITION(log); + return command_log; +} + +std::string gdb_apit::read_next_line() +{ + std::string result; + + do + { + const size_t buf_size = 1024; + char buf[buf_size]; // NOLINT(runtime/arrays) + + const char *c = fgets(buf, buf_size, response_stream); + + if(c == NULL) + { + if(ferror(response_stream)) + { + throw gdb_interaction_exceptiont("error reading from gdb"); + } + + INVARIANT( + feof(response_stream), + "EOF must have been reached when the error indicator on the stream " + "is not set and fgets returned NULL"); + INVARIANT( + result.empty() || result.back() != '\n', + "when EOF is reached then either no characters were read or the string" + " read does not end in a newline"); + + return result; + } + + std::string chunk(buf); + INVARIANT(!chunk.empty(), "chunk cannot be empty when EOF was not reached"); + + result += chunk; + } while(result.back() != '\n'); + + return result; +} + +std::string gdb_apit::read_most_recent_line() +{ + std::string line; + std::string output; + + do + { + output = line; + line = read_next_line(); + } while(line != "(gdb) \n"); + + return output; +} + +gdb_apit::gdb_output_recordt +gdb_apit::get_most_recent_record(const std::string &tag, const bool must_exist) +{ + std::string line = read_most_recent_line(); + const bool b = has_prefix(line, tag); + + if(must_exist) + { + CHECK_RETURN(b); + } + else if(!b) + { + throw gdb_interaction_exceptiont("record does not exist"); + } + + std::string record = strip_string(line.substr(line.find(',') + 1)); + + return parse_gdb_output_record(record); +} + +bool gdb_apit::most_recent_line_has_tag(const std::string &tag) +{ + const std::string line = read_most_recent_line(); + return has_prefix(line, tag); +} + +/// Run gdb with the given core file +/// +/// \param corefile core dump +void gdb_apit::run_gdb_from_core(const std::string &corefile) +{ + PRECONDITION(gdb_state == gdb_statet::CREATED); + + // there does not seem to be a gdb mi command to run from a core file + const std::string command = "core " + corefile; + + write_to_gdb(command); + check_command_accepted(); + + gdb_state = gdb_statet::STOPPED; +} + +/// Run gdb to the given breakpoint +/// +/// \param breakpoint the breakpoint to set (can be e.g. a line number or a +/// function name) +bool gdb_apit::run_gdb_to_breakpoint(const std::string &breakpoint) +{ + PRECONDITION(gdb_state == gdb_statet::CREATED); + + std::string command("-break-insert"); + command += " " + breakpoint; + + write_to_gdb(command); + if(!was_command_accepted()) + { + throw gdb_interaction_exceptiont("could not set breakpoint"); + } + + write_to_gdb("-exec-run"); + + if(!most_recent_line_has_tag("*running")) + { + throw gdb_interaction_exceptiont("could not run program"); + } + + gdb_output_recordt record = get_most_recent_record("*stopped"); + const auto it = record.find("reason"); + CHECK_RETURN(it != record.end()); + + const std::string &reason = it->second; + + if(reason == "breakpoint-hit") + { + gdb_state = gdb_statet::STOPPED; + return true; + } + else if(reason == "exited-normally") + { + return false; + } + else + { + throw gdb_interaction_exceptiont( + "gdb stopped for unhandled reason `" + reason + "`"); + } + + UNREACHABLE; +} + +std::string gdb_apit::eval_expr(const std::string &expr) +{ + write_to_gdb("-var-create tmp * " + expr); + + if(!was_command_accepted()) + { + throw gdb_interaction_exceptiont( + "could not create variable for expression `" + expr + "`"); + } + + write_to_gdb("-var-evaluate-expression tmp"); + gdb_output_recordt record = get_most_recent_record("^done", true); + + write_to_gdb("-var-delete tmp"); + check_command_accepted(); + + const auto it = record.find("value"); + CHECK_RETURN(it != record.end()); + + const std::string value = it->second; + + INVARIANT( + value.back() != '"' || + (value.length() >= 2 && value[value.length() - 2] == '\\'), + "quotes should have been stripped off from value"); + INVARIANT(value.back() != '\n', "value should not end in a newline"); + + return value; +} + +/// Get the memory address pointed to by the given pointer expression +/// +/// \param expr an expression of pointer type (e.g., `&x` with `x` being of type +/// `int` or `p` with `p` being of type `int *`) +/// \return memory address in hex format +std::string gdb_apit::get_memory(const std::string &expr) +{ + PRECONDITION(gdb_state == gdb_statet::STOPPED); + + std::string mem; + + // regex matching a hex memory address followed by an optional identifier in + // angle brackets (e.g., `0x601060 `) + std::regex regex(R"(^(0x[1-9a-f][0-9a-f]*)( <.*>)?)"); + + const std::string value = eval_expr(expr); + + std::smatch result; + if(regex_match(value, result, regex)) + { + // return hex address only + return result[1]; + } + else + { + throw gdb_interaction_exceptiont( + "value `" + value + + "` is not a memory address or has unrecognised format"); + } + + UNREACHABLE; +} + +/// Get value of the given value expression +/// +/// \param expr an expression of non-pointer type or pointer to char +/// \return value of the expression; if the expression is of type pointer to +/// char and represents a string, the string value is returned; otherwise the +/// value is returned just as it is printed by gdb +std::string gdb_apit::get_value(const std::string &expr) +{ + PRECONDITION(gdb_state == gdb_statet::STOPPED); + + const std::string value = eval_expr(expr); + + { + // get string from char pointer + const std::regex regex(R"(0x[1-9a-f][0-9a-f]* \\"(.*)\\")"); + + std::smatch result; + if(regex_match(value, result, regex)) + { + return result[1]; + } + } + + // this case will go away eventually, once client code has been refactored to + // use get_memory() instead + { + // get void pointer address + const std::regex regex(R"(0x[1-9a-f][0-9a-f]*)"); + + std::smatch result; + if(regex_match(value, result, regex)) + { + return result[1]; + } + } + + // return raw value + return value; +} + +gdb_apit::gdb_output_recordt +gdb_apit::parse_gdb_output_record(const std::string &s) +{ + PRECONDITION(s.back() != '\n'); + + gdb_output_recordt result; + + std::size_t depth = 0; + std::string::size_type start = 0; + + const std::string::size_type n = s.length(); + + for(std::string::size_type i = 0; i < n; i++) + { + const char c = s[i]; + + if(c == '{' || c == '[') + { + depth++; + } + else if(c == '}' || c == ']') + { + depth--; + } + + if(depth == 0 && (c == ',' || i == n - 1)) + { + const std::string item = + i == n - 1 ? s.substr(start) : s.substr(start, i - start); + + // Split on first `=` + std::string::size_type j = item.find('='); + CHECK_RETURN(j != std::string::npos); + CHECK_RETURN(j > 0); + CHECK_RETURN(j < s.length()); + + const std::string key = strip_string(item.substr(0, j)); + std::string value = strip_string(item.substr(j + 1)); + + const char first = value.front(); + const char last = value.back(); + + INVARIANT(first == '"' || first == '{' || first == '[', ""); + INVARIANT(first != '"' || last == '"', ""); + INVARIANT(first != '{' || last == '}', ""); + INVARIANT(first != '[' || last == ']', ""); + + // Remove enclosing `"` for primitive values + if(first == '"') + { + value = value.substr(1, value.length() - 2); + } + + auto r = result.insert(std::make_pair(key, value)); + CHECK_RETURN(r.second); + + start = i + 1; + } + } + + return result; +} + +bool gdb_apit::was_command_accepted() +{ + return most_recent_line_has_tag("^done"); +} + +void gdb_apit::check_command_accepted() +{ + bool was_accepted = was_command_accepted(); + CHECK_RETURN(was_accepted); +} + +#endif diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h new file mode 100644 index 00000000000..92c73df2234 --- /dev/null +++ b/src/memory-analyzer/gdb_api.h @@ -0,0 +1,107 @@ +/*******************************************************************\ + +Module: GDB Machine Interface API + +Author: Malte Mues + Daniel Poetzl + +\*******************************************************************/ + +/// \file +/// Low-level interface to gdb +/// +/// This provides an API to run a program under gdb up to some +/// breakpoint, and then query the values of expressions. It uses the +/// gdb machine interface (see section "The GDB/MI Interface" in the +/// gdb manual to communicate with gdb. + +// clang-format off +#if defined(__linux__) || \ + defined(__FreeBSD_kernel__) || \ + defined(__GNU__) || \ + defined(__unix__) || \ + defined(__CYGWIN__) || \ + defined(__MACH__) +// clang-format on + +#ifndef CPROVER_MEMORY_ANALYZER_GDB_API_H +#define CPROVER_MEMORY_ANALYZER_GDB_API_H +#include + +#include +#include + +#include + +class gdb_apit +{ +public: + using commandst = std::forward_list; + + explicit gdb_apit(const char *binary, const bool log = false); + ~gdb_apit(); + + void create_gdb_process(); + void terminate_gdb_process(); + + bool run_gdb_to_breakpoint(const std::string &breakpoint); + void run_gdb_from_core(const std::string &corefile); + + std::string get_value(const std::string &expr); + std::string get_memory(const std::string &expr); + + const commandst &get_command_log(); + +protected: + const char *binary; + + FILE *response_stream; + FILE *command_stream; + + const bool log; + commandst command_log; + + enum class gdb_statet + { + NOT_CREATED, + CREATED, + STOPPED // valid state, reached e.g. after breakpoint was hit + }; + + gdb_statet gdb_state; + + typedef std::map gdb_output_recordt; + static gdb_output_recordt parse_gdb_output_record(const std::string &s); + + void write_to_gdb(const std::string &command); + + std::string read_next_line(); + std::string read_most_recent_line(); + + std::string eval_expr(const std::string &expr); + + gdb_output_recordt + get_most_recent_record(const std::string &tag, const bool must_exist = false); + + bool most_recent_line_has_tag(const std::string &tag); + bool was_command_accepted(); + void check_command_accepted(); +}; + +class gdb_interaction_exceptiont : public cprover_exception_baset +{ +public: + explicit gdb_interaction_exceptiont(std::string reason) : reason(reason) + { + } + std::string what() const override + { + return reason; + } + +private: + std::string reason; +}; + +#endif // CPROVER_MEMORY_ANALYZER_GDB_API_H +#endif diff --git a/src/memory-analyzer/module_dependencies.txt b/src/memory-analyzer/module_dependencies.txt new file mode 100644 index 00000000000..5e3f81fdcc7 --- /dev/null +++ b/src/memory-analyzer/module_dependencies.txt @@ -0,0 +1,3 @@ +goto-programs +util +sys diff --git a/unit/Makefile b/unit/Makefile index 8b3f5343b1d..c93aa6fc932 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -32,6 +32,7 @@ SRC += analyses/ai/ai.cpp \ interpreter/interpreter.cpp \ json/json_parser.cpp \ json_symbol_table.cpp \ + memory-analyzer/gdb_api.cpp \ path_strategies.cpp \ pointer-analysis/value_set.cpp \ solvers/bdd/miniBDD/miniBDD.cpp \ diff --git a/unit/memory-analyzer/gdb_api.cpp b/unit/memory-analyzer/gdb_api.cpp new file mode 100644 index 00000000000..fb4ef130549 --- /dev/null +++ b/unit/memory-analyzer/gdb_api.cpp @@ -0,0 +1,197 @@ +/*******************************************************************\ + +Module: GDB Machine Interface API unit tests + +Author: Malte Mues + Daniel Poetzl + +\*******************************************************************/ + +#include + +// clang-format off +#if defined(__linux__) || \ + defined(__FreeBSD_kernel__) || \ + defined(__GNU__) || \ + defined(__unix__) || \ + defined(__CYGWIN__) || \ + defined(__MACH__) +#define RUN_GDB_API_TESTS +#endif +// clang-format on + +#ifdef RUN_GDB_API_TESTS + +#include +#include +#include +#include + +#include +#include + +#include + +void compile_test_file() +{ + std::string test_file("memory-analyzer/test.c"); + + std::string cmd("gcc -g -o test "); + cmd += test_file; + + const int r = system(cmd.c_str()); + REQUIRE(!r); +} + +class gdb_api_testt : public gdb_apit +{ + explicit gdb_api_testt(const char *binary) : gdb_apit(binary) + { + } + + friend void gdb_api_internals_test(); +}; + +void gdb_api_internals_test() +{ + compile_test_file(); + + SECTION("parse gdb output record") + { + gdb_api_testt gdb_api("test"); + + gdb_api_testt::gdb_output_recordt gor = gdb_api.parse_gdb_output_record( + "a = \"1\", b = \"2\", c = {1, 2}, d = [3, 4], e=\"0x0\""); + + REQUIRE(gor["a"] == "1"); + REQUIRE(gor["b"] == "2"); + REQUIRE(gor["c"] == "{1, 2}"); + REQUIRE(gor["d"] == "[3, 4]"); + REQUIRE(gor["e"] == "0x0"); + } + + SECTION("read a line from an input stream") + { + gdb_api_testt gdb_api("test"); + + FILE *f = fopen("memory-analyzer/input.txt", "r"); + gdb_api.response_stream = f; + + std::string line = gdb_api.read_next_line(); + REQUIRE(line == "abc\n"); + + line = gdb_api.read_next_line(); + REQUIRE(line == std::string(1120, 'a') + "\n"); + + line = gdb_api.read_next_line(); + REQUIRE(line == "xyz"); + } + + SECTION("start and exit gdb") + { + gdb_api_testt gdb_api("test"); + + gdb_api.create_gdb_process(); + + // check input and output streams + REQUIRE(!ferror(gdb_api.response_stream)); + REQUIRE(!ferror(gdb_api.command_stream)); + } +} + +#endif + +TEST_CASE("gdb api internals test", "[core][memory-analyzer]") +{ +#ifdef RUN_GDB_API_TESTS + gdb_api_internals_test(); +#endif +} + +TEST_CASE("gdb api test", "[core][memory-analyzer]") +{ +#ifdef RUN_GDB_API_TESTS + compile_test_file(); + + { + gdb_apit gdb_api("test", true); + gdb_api.create_gdb_process(); + + try + { + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); + REQUIRE(r); + } + catch(const gdb_interaction_exceptiont &e) + { + std::cerr << "warning: cannot fully unit test GDB API as program cannot " + << "be run with gdb\n"; + std::cerr << "warning: this may be due to not having the required " + << "permissions (e.g., to invoke ptrace() or to disable ASLR)" + << "\n"; + std::cerr << "gdb_interaction_exceptiont:" << '\n'; + std::cerr << e.what() << '\n'; + + std::ifstream file("gdb.txt"); + CHECK_RETURN(file.is_open()); + std::string line; + + std::cerr << "=== gdb log begin ===\n"; + + while(getline(file, line)) + { + std::cerr << line << '\n'; + } + + file.close(); + + std::cerr << "=== gdb log end ===\n"; + + return; + } + } + + gdb_apit gdb_api("test"); + gdb_api.create_gdb_process(); + + SECTION("breakpoint is hit") + { + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); + REQUIRE(r); + } + + SECTION("breakpoint is not hit") + { + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint2"); + REQUIRE(!r); + } + + SECTION("breakpoint does not exist") + { + REQUIRE_THROWS_AS( + gdb_api.run_gdb_to_breakpoint("checkpoint3"), gdb_interaction_exceptiont); + } + + SECTION("query memory") + { + const bool r = gdb_api.run_gdb_to_breakpoint("checkpoint"); + REQUIRE(r); + + REQUIRE(gdb_api.get_value("x") == "8"); + REQUIRE(gdb_api.get_value("s") == "abc"); + + const std::regex regex(R"(0x[1-9a-f][0-9a-f]*)"); + + { + std::string address = gdb_api.get_memory("p"); + REQUIRE(std::regex_match(address, regex)); + } + + { + std::string address = gdb_api.get_memory("vp"); + REQUIRE(std::regex_match(address, regex)); + } + } + +#endif +} diff --git a/unit/memory-analyzer/input.txt b/unit/memory-analyzer/input.txt new file mode 100644 index 00000000000..5d3bfc24a58 --- /dev/null +++ b/unit/memory-analyzer/input.txt @@ -0,0 +1,3 @@ +abc +aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa +xyz \ No newline at end of file diff --git a/unit/memory-analyzer/module_dependencies.txt b/unit/memory-analyzer/module_dependencies.txt new file mode 100644 index 00000000000..aa1bc7f84f8 --- /dev/null +++ b/unit/memory-analyzer/module_dependencies.txt @@ -0,0 +1,2 @@ +memory-analyzer +testing-utils diff --git a/unit/memory-analyzer/test.c b/unit/memory-analyzer/test.c new file mode 100644 index 00000000000..8c23338cddb --- /dev/null +++ b/unit/memory-analyzer/test.c @@ -0,0 +1,27 @@ +int x; +char *s = "abc"; +int *p; +void *vp; + +void checkpoint() +{ +} +void checkpoint2() +{ +} + +void func() +{ + checkpoint2(); +} + +int main() +{ + x = 8; + p = &x; + vp = (void *)&x; + + checkpoint(); + + return 0; +} diff --git a/unit/module_dependencies.txt b/unit/module_dependencies.txt index 65410cabc47..ffb35402365 100644 --- a/unit/module_dependencies.txt +++ b/unit/module_dependencies.txt @@ -7,6 +7,7 @@ goto-programs goto-symex json langapi # should go away +memory-analyzer solvers/flattening solvers/floatbv solvers/miniBDD