Open dddejan opened 7 years ago
Here is an example how to run the code
dejan@hilbert:~/workspace/sally/build$ ./src/sally -v 1 --debug crab --no-lets --ai crab ../test/regress/ic3/example0.mcmt
[2017-03-06.11:45:03] Processing ../test/regress/ic3/example0.mcmt
[2017-03-06.11:45:03] Crab: starting
crab: I = (= |state_type::state.x| 0)
crab: T = (= |state_type::next.x| (+ |state_type::state.x| 1))
[2017-03-06.11:45:03] Crab: done
Engine needed to do a query.
-v 1
is the general message verbosity (to be used with MSG() macro)--debug crab
is the trace option (to be used with the TRACE() macro)--no-lets
is for printout without the let
construct--ai
selects crab as the abstract interpretation engine
I've added some boilerplate to the "ai" branch.
Notes:
src/ai/crab/crab.{h.cpp}
.src/ai/crab/crab_info.h
and they will automatically be available from command line.crab.cpp
so that they don't leak out to the rest of the project.