Updated README.md and Makefile

Author: aadityanaik

clang-fe/Makefile

@@ -56,14 +56,14 @@ tests: bin/clang-fe
 @echo "The tests need to be manually verified. The json files are written into the same directory as the test cases."
 @echo "For information about the rewritten code, CFG and the Dominator Tree, run make test-debug."
 @cp tests/assert.h .
-./bin/clang-fe $(shell ls tests/*.c) 2>/dev/null
+./bin/clang-fe -ssa $(shell ls tests/*.c) 2>/dev/null
 @rm assert.h
 
 test-debug: bin/clang-fe
 @echo "The tests need to be manually verified. The json files are written into the same directory as the test cases."
 @echo "For information about the rewritten code, CFG and the Dominator Tree, run make test-debug."
 @cp tests/assert.h .
-./bin/clang-fe $(shell ls tests/*.c)
+./bin/clang-fe -ssa $(shell ls tests/*.c)
 @rm assert.h
 
 clean:

clang-fe/README.md

@@ -1,19 +1,21 @@
 # clang-fe
 
-A front end to code2inv responsible for transforming code into its SSA form using Clang.
+A front end to code2inv responsible for transforming code into its SSA form and also generating Verification Conditions using Clang.
 
 ## Installation
 
-Refer [INSTALL.md](INSTALL.md)
+Refer [INSTALL.md](INSTALL.md).
 
 ## Run the executable
 
-To run any of the test codes inside the tests directory, cd into tests/ and run `../bin/ssa-transform filename.c`. This will produce a json file of the same name with the ssa graph in it. To run all tests, run `make tests` (for no debug output) or `make test-debug` for debug output (which includes the CFG, Dominator Tree and the SSA Graph).
+To run any of the test codes inside the tests directory, cd into tests/ and run `../bin/clang-fe -ssa filename.c`. This will produce a json file of the same name with the ssa graph in it. To run all tests, run `make tests` (for no debug output) or `make test-debug` for debug output (which includes the CFG, Dominator Tree and the SSA Graph).
+
+To generate Verification Conditions, run `./bin/clang-fe -smt ../benchmarks/c/<filename>`. Only the files under benchmarks have been tested with VC Generation. To only store the SMT graph, run `./bin/clang-fe -smt ../benchmarks/c/<filename> > smtfile.smt 2>/dev/null`.
 
 ## Notes
-The renaming and phi function placement algorithms are taken from http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.6361&rep=rep1&type=pdf
+The renaming and phi function placement algorithms are taken from http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.6361&rep=rep1&type=pdf.
 
-Clang-fe has only been tested on the programs under the tests directory, taken from https://github.com/sosy-lab/sv-benchmarks/tree/master/c/loop-invgen
+Clang-fe has only been tested on the programs under the tests directory taken from https://github.com/sosy-lab/sv-benchmarks/tree/master/c/loop-invgen and the benchmarks directory.
 
 ## Known Issues
 <ul>