a brief overview of the huge commit
Radu Grigore
I changed. I'm a bit concerned that I'll give unsolicited advice in
the process, but I hope it is better to say what's on my mind than not
to. Be warned: this is purely about engineering, not about science, so
you may find it boring.
Many changes are simply code rewritings I've done while reading it. A
few changes are more pervasive.
I'll start with the pervasive changes. In src/utils/debug.ml [1]
there's a bit of infrastructure that should help with debugging. The
flag "safe" is supposed to guard expensive sanity checks (aka
assertions). Non-expensive assertions can use OCaml's assert.
Roughly, sanity checks that take Omega(n) time are probably
"expensive". The log_* flags are supposed to turn on/off various
categories of *debugging* output (as opposed to user output). The
reason they are implemented with bitmasks is that in this case the
compiler is smart enough to completely remove the code that does some
debugging printing when that printing is turned off. Note that none of
these things is supposed to be used in any way to control output
intended for the user. (IOW, they are *not* verbosity controls.)
The other change is that I migrated to Format from Printf. OCaml's
docs suggest that they may be unexpected behavior if you use both [2].
It's possible that new Printfs were introduced after I did the
modifications, since I didn't merge them in time. :P While making the
changes I notice some formats that seemed strange (although I can't
remember now what exactly was the problem), so I wrote some 'applied
summary' of what I learned by reading [2], also in debug.ml [1]. Oh, I
opened Format everywhere, since it seems a standard convention in
OCaml to open Printf/Format (but not other standard libs like List
because of name conflicts with other standard libs).
Related to Format, I think I added some pretty-printing functions for
data structures, and perhaps changed a few to start with "pp_", as
they do in the standard library [2]. Another change is that I tried to
use Format's tags facility for the non-printable output that switches
colors. That's what they are for.
OK, now smaller changes. I renamed stmt_core to cfg_node because I
found it impossible to remember which is which out of stmt_core and
core_statement. The building of the CFG of core statements now uses
some hashes instead of association lists.
There's probably other stuff that I don't remember. There's also some
stuff in my non-master branches that I need to look at...
regards,
radu
[1] http://github.com/septract/jstar/blob/master/src/utils/debug.ml
[2] see the "Warning" at
http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html
Matthew Parkinson
code and also setting up the error messages to be localisable to
modules. We should add
Engineering jStar
To the agenda. As you might have gathered lots of jStar was somewhat
rushed. Part of our hope with this grant is to get some good research
done while making jStar a better engineered tool.
One thing we should perhaps have a regular Skype chat between Cam and
QM to stop any duplication of effort. Also perhaps more regular
commits, so we can all see what is happening?
Matt
Sent from my iPhone
Radu Grigore
> Also perhaps more regular commits, so we can all see what is happening?
You can follow my fork on github to see the commits. The problem was I
wasn't merging them.
Anyway, I set github earlier to send commit emails to the developers
list for my fork (septract needs to do it for the main fork). Whoever
will turn out to be the source of those emails (github?) needs to be
allowed to post by a moderator.
regards,
radu
Radu Grigore
> stop any duplication of effort.
Either that or more emails, I'd say.
Matthew Parkinson
Matt
Sent from my iPhone
Mike Dodds
>> stop any duplication of effort.
>
> Either that or more emails, I'd say.
Yes, this.
> One thing I noticed is that Mike added some command line flags that
> look like they conflict (semantically) with some older changes from my
> fork that I didn't merge. I'll look into this by tomorrow.
Yes, could you look into this?
Things I'm currently working on:
1. A more generic test-harness framework for symbexe etc. [easy]
2. Abduction. [hard]
M.
Dino Distefano
an idea.
It looks to me that using git is somehow hiding what people is
actually doing. So more
information should go around between people in different means. Skype
can be good.