Thank you for the comments, I'll take them into account and form a new
patch.
On Friday, October 28, 2011 16:55:56 you wrote:
> Why does --no-convert-field-offsets imply --no-split-structs?
> Shouldn't the user be to enable them separately?
>
> > @@ -89,6 +89,12 @@ let simplAddrOf = ref true
> >
> > * has been taken somewhere. *)
> >
> > let convertDirectCalls = ref true
> >
> > +(* Whether to convert field offsets to offsets by integer.
> > + * Static source code verifiers do not need such a conversion *)
> > +let convertFieldOffsets = ref true
> > +(* WARN: splitStructs should be set to false, as it won't find
> > the usage of *) +
> > +
> >
> > let onlyVariableBasics = ref false
> > let noStringConstantsBasics = ref false
>
> This looks like an explanation, but I'm afraid I don't understand it
> ("the usage of"... what?).
It turns out that I started to write an explanation, and switched to
something else forgetting to complete it. I'll figure it out.
Anyway, splitting structures in function calls isn't very useful for a
static verification tool that supports C structures, which is the
"target audience" for this patch.
> > @@ -224,8 +234,13 @@ and simplifyLval
> >
> > in
> > let a' = if !simpleMem then makeBasic setTemp a'
> > else a' in
> > Mem (mkCast a' (typeForCast restoff)), restoff
> >
> > + | Mem a, off when not !convertFieldOffsets ->
>
> I'd rather remove the "when" here, since it's the complement of the
> previous case and could confuse exhaustiveness analysis (did not try
> to compile it in fact) --- and maybe put this case before the
> previous one, in fact.
Yeah, you're probably right.
> > (* We are taking this variable's address; but suppress
> > simplification if it's a simple function>
> > * call in no-convert mode*)
> >
> > + | Var v, off when v.vaddrof && (not !convertFieldOffsets) &&
> > (!convertDirectCalls || not (isFunctionType (typeOfLval lv) ))
> > -> + (Var v, off)
>
> The "when" part is very complex, why not make your change an "if" in
the next case:
Okay, but it may fail to make the code less complex.
> Will try to look at it in more depth next week. Since your patch is
> not very invasive, I guess the issue is its interaction with other
> simplification steps.
Thanks.
> > 2) could this patch be added to upstream nevertheless? I think
> > that the benefits to the verification tools, for which the
> > options is useful, are much greater than the very rarely
> > encountered issue with "very volatile" structs with array fields.
> > Besides, the behavior without this command- line option is
> > retained.
>
> I do not like the idea of adding bugs on purpose, but I see your
> point. Need to think a bit more about it.
I do not approach this as "adding a bug on purpose". Rather, I think
it's adding a feature that is useful but doesn't work in all cases.
Moreover, problematic cases may be inserted into the test system as
"should fail at compilation" tests; does the test system employed
support that?
--
Pavel Shved
website: http://coldattic.info/
e-mail: [email protected]
------------------------------------------------------------------------------
Get your Android app more play: Bring it to the BlackBerry PlayBook
in minutes. BlackBerry App World™ now supports Android™ Apps
for the BlackBerry® PlayBook™. Discover just how easy and simple
it is! http://p.sf.net/sfu/android-dev2dev
_______________________________________________
CIL-users mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/cil-users
