output of state

[jonathan heusser]

Hi Nathan,

I'm posting here in case other users have similar questions.
Is there a way to output the abstract variable state after the
analysis ? E.g. when using the interval domain it would output { l =
[0 20], h = [1 19], ... } or something.

thanks
Jonathan

[Nathan Cooprider]

This is a feature that I am in the middle of adding at various people's
request. There are two partial solutions:

--cxp_global_states

Prints the state at the start of each function, plus the return value,
to a file with .states added to the end. Each function is identified,
and then the output is of the form:

name : type : value

--cxp_peek_globals

Peek at all the information about globals (and why they don't compress).
This is output to standard out and does NOT include the actual values in
the globals. The main focus is the amount of information known about the
variable, not what that information is.

In a upcoming version (maybe even today) I will include global values in
the --cxp_global_states output. I will post to this list when a version
with that feature is available for download.

Getting global information for locals is problematic because of the way
CIL handles local initializations. It is not impossible, I just haven't
been pushed hard enough to figure out how to tease the information out.

Nathan

[Nathan Cooprider]

I just posted a version of cXprop which adds global state to the
information printed by using the --cxp_global_states flag. Sorry this
was not in the version posted earlier this week.

http://www.cs.utah.edu/~coop/research/ccomp/cil-cXprop.tgz

Let me know if you have any questions or problems.

Nathan