Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[GDB] Create script and tests for GDB to run in CI #840

Open
Robertorosmaninho opened this issue Sep 28, 2023 · 2 comments
Open

[GDB] Create script and tests for GDB to run in CI #840

Robertorosmaninho opened this issue Sep 28, 2023 · 2 comments
Assignees
@Robertorosmaninho
Labels
debugger

Comments

@Robertorosmaninho
Copy link
Collaborator

No description provided.

@Robertorosmaninho Robertorosmaninho self-assigned this Sep 28, 2023
@Robertorosmaninho
Copy link
Collaborator Author

Robertorosmaninho commented Sep 28, 2023 •
edited
Loading

  • Check if it is possible to automatize GDB/LLDB executions to run then in CI

Yes, it is. Both tools have a batch mode, and we can pass a list of commands on a file to be executed by GDB/LLDB.
#851 and runtimeverification/k#3687 introduce the interface to enable GDB/LLDB executions in CI

  • What do we want to test? Which programs and commands do we want to verify?
  • k start, k step, k step n, quit
  • Breakpoints
  • k match rule (success and fail)
  • print data types
  • How to create a standard output between systems that don't contain any source directory or platform-specific info? We need to pipe all outputs to this standard format.
  • Create the Debugger Test directory containing each test in a subfolder. Each test should contain:
    • The test file
    • A possible input
    • The debugger commands in a file
    • The expected output
  • Integrate the test-suite with lit

@Robertorosmaninho Robertorosmaninho mentioned this issue Oct 3, 2023
Merged
@radumereuta radumereuta mentioned this issue Oct 4, 2023
Merged
rv-jenkins pushed a commit that referenced this issue Oct 4, 2023
@Robertorosmaninho
Creating debug-command flag on llvm-krun (#851)
11ced91 
This PR introduces the `--debug-command` to the `llvm-krun` flag that
enables the use of GDB and LLDB in a non-iterative mode by passing a
file with the debugger commands appropriate for the OS.

This PR is part of #840 and will enable testing the debugger on the CI.

---------

Co-authored-by: rv-jenkins <devops@runtimeverification.com>
@Robertorosmaninho
Copy link
Collaborator Author

Blocked on: #858

@Robertorosmaninho Robertorosmaninho mentioned this issue Oct 15, 2023
Closed
@Baltoli Baltoli mentioned this issue Dec 5, 2023
Open
6 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Robertorosmaninho Robertorosmaninho

Labels
debugger
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Introducing GDB tests on CI runtimeverification/llvm-backend
1 participant
@Robertorosmaninho