Different struct sizes

[Chasm]

Why does an empty struct have a size of 4 and not 1 like in C#?

[Charles]

For contract support. Cobra adds this to structs and classes:

Code: Select all

   int _ih_invariantGuard;


You can remove it with the -contracts:none option.

You can research issues like this with the -keep-intermediate-files option. The various *.cs files will be left around:

"""
cobra -c -keep-intermediate-files empty-struct.cobra
cobra -c -keep-intermediate-files -contracts:none empty-struct.cobra
"""

struct S

    pass


class P

    def main
        pass

[hopscc]

Unfortunately it adds it regardless of whether its needed or not (i.e if there are no contracts/invariants given).

Also it may be possible/preferable to only have it on the lowest accessible baseclass rather than each class
see notes and patch on ticket:243

[Chasm]

What is that integer for? What function does it serve? I mean does it store data or just serve as a key?

[hopscc]

Its a guard value to make invariant checks run only once per method
(for suppressing invariant checks inside methods called (possibly by by invariant checks).
Its bumped prior to checking and any re-entrant checks are not run if guard value non zero.

See SharpGenerator.cobra (codegen) or can see the mechanism by making a class with invariants and compiling with
-kif/keep-intermediate-files and looking at C# code generated.

Theres a fair bit of unnecessary inserted boiler plate inserted that could be optimised away.
(I see another ticket coming up)

Charles:
Slightly related:
with -contracts:methods is it intentional that both calls to the synthesized require/ensure contract methods and (possibly empty) contracts methods themselves are always generated (even if no contracts are given)?
The default inline version at least has some optimising out for non-existant contracts calls.

[Chasm]

And couldn't you make it "DependencyProperty"-esque? Basically a static dictionary of <int, int>? The object's address would be the key and the value would be the check int?

[Charles]

Charles:
Slightly related:
with -contracts:methods is it intentional that both calls to the synthesized require/ensure contract methods and (possibly empty) contracts methods themselves are always generated (even if no contracts are given)?
The default inline version at least has some optimising out for non-existant contracts calls.

It's been awhile since I worked on that code, so I don't have a ready answer for you. Potential motivations that come to mind include:

-- subclassing

-- the library boundary

So if we optimize it out, we'll need to be sure some test cases are in place around those circumstances.

[Charles]

And couldn't you make it "DependencyProperty"-esque? Basically a static dictionary of <int, int>? The object's address would be the key and the value would be the check int?

For classes/objects, that seems workable. For structs/values, I don't think it would work.