Software installation guide for Lecture 9
Please install the software listed below.
If any issues contact avais _at_ cse . iitb . ac . in
We will be in the class room at 13:00 (one hour before the class) to
helpout students if the have any issues in installation.
Installing emacs25 IDE
Execute following commands:
- $ sudo apt-get update
- $ sudo apt-get install emacs
- $ emacs --version
You should be able to see current installed version of emacs
- $ emacs
Emacs window should be open
Installing gdb
Execute following commands:
- $ sudo apt-get update
- $ sudo apt-get install gdb
- $ gdb --version
You should be able to see current installed version of gdb
Using gdb
- Try writing a simple hello world program and save it with name src.c.
- Compile it using `-g` flag:
$gcc -g src.c -o a.out
-g flag will compile src.c in debug mode
Now `a.out` has bytecode annotated with debug info, which can be used by GDB.
- Now run following commands to start debugger
$ gdb a.out
- Add breakpoints at some lines
Example:- b 4 (breakpoint at line 4)
b main (breakpoint at function main)
- Now type in debugger :-
run
and analyse the output
- Enter
n
for next
- Enter
q
for quitting debugger
Links to good tutorials in GDB (highly recommended to do before class):
- Short and simple http://www.gdbtutorial.com/
- A bit more detail
https://www.cs.umd.edu/~srhuang/teaching/cmsc212/gdb-tutorial-handout.pdf
- https://people.cs.uchicago.edu/~bomb154/154/maclabs/gdblab.html
- Short and dry https://www.cprogramming.com/gdb.html
GDB References
https://www.gnu.org/software/gdb/documentation/
Compiling Z3 and using it
- Install cmake
$ sudo apt-get install cmake
- Download test.smt2 file
- Even if you have build z3 previously we still need to follow these steps to build it again in debug mode
- Making a environment variable for z3 path, you can change path according to your convenience
$ export BUILDDIR=~/z3build
- Creating the directory
$ mkdir -p $BUILDDIR
- Changing current directory
$ cd $BUILDDIR
- Cloning z3Prover form github in current directory
$ git clone https://github.com/Z3Prover/z3.git
- Remove builddebug directry if it already exist
$ rm -rf $BUILDDIR/z3/builddebug
- Creating builddebug folder
$ mkdir -p $BUILDDIR/z3/builddebug
- Change directory to builddebug
$ cd $BUILDDIR/z3/builddebug
- Now type:-
$ cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Debug ../
$ make
It will build in debug mode, it might take a while
- Running the test.smt2 file, change the path according to test.smt2 location
$ ./z3 -smt2 ~/Downloads/test.smt2
Running gdb in emacs
The GDB mode for emacs is an excellent way to interact with GDB. It comes pre-installed in emacs.
Note:
`C-x` stands for the keypress "Control with x"
`M-x` stands for the keypress "Alt with x"
`C-x o` stands for the keypress "Control with x, then o"
- Change current directory of terminal to builddebug folder
- Start emacs by typing:-
$ emacs
On the terminal
- Press on emacs
M-x (Alt+x)
And type:-
gdb
- Type following in Run gdb (like this) , set path of test.smt2 accordingly
gdb -i=mi --args z3 -smt2 ~/Downloads/test.smt2
--args parameter is used because we will be passing them as argumen