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

AV: Options to ignore CPP file and allocate within stubs for nested pointers #47

Open
shuvendu-lahiri opened this issue Jun 19, 2017 · 3 comments
Assignees

Comments

@shuvendu-lahiri
Copy link
Collaborator

shuvendu-lahiri commented Jun 19, 2017

Is there an option to not analyze CPP and header files.

If you see an stub with an argument A **x, then we allocate *x. Related to #35

Also mod is not handled precisely (e.g. 0%2 == 0). Are there missing axioms or options?

@akashlal
Copy link
Contributor

Both these options exist and used by default, but for some reason they did not fire. Can you please share a module name on email and I'll investigate?

Mod is translated to an uninterpreted function (INTMOD). It does not have any supporting axioms. I will add 0 % x == 0.

@akashlal
Copy link
Contributor

akashlal commented Jul 1, 2017

Nevermind. I see the module names in SMV OneNote document. I will investigate.

@zvonimir
Copy link
Collaborator

I am guessing nobody will work on this any time soon, if ever.
@shuvendu-lahiri and @akashlal : are you ok if I mark this as "won't fix" and close the issue?

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

No branches or pull requests

3 participants