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.

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

Integrate crab into Sally #42

Open
dddejan opened this issue Mar 6, 2017 · 1 comment
Open

Integrate crab into Sally #42

dddejan opened this issue Mar 6, 2017 · 1 comment
Assignees

Comments

@dddejan
Copy link
Member

dddejan commented Mar 6, 2017

I've added some boilerplate to the "ai" branch.

Notes:

  • The code for crab integration should be added to src/ai/crab/crab.{h.cpp}.
  • Any options for the module should be added to src/ai/crab/crab_info.h and they will automatically be available from command line.
  • We try to use regular c++ features, if crab is using new c++ features they should only be used within crab.cpp so that they don't leak out to the rest of the project.
@dddejan
Copy link
Member Author

dddejan commented Mar 6, 2017

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants