Prove tests about gneiss HOT 9 CLOSED

@senier How should we handle warnings for missing global contracts? From the perspective of the application this isn't directly an error but I think we should model it at some point. I would propose an extra issue for that but I'm not sure if it should reside in 0.2.

from gneiss.

@senier How should we handle warnings for missing global contracts? From the perspective of the application this isn't directly an error but I think we should model it at some point. I would propose an extra issue for that but I'm not sure if it should reside in 0.2.

What messages are you referring to? Missing internal state? If so, wouldn't that prevent even flow analysis?

from gneiss.

I'm referring to

warning: no global contract available for ...
warning: assuming ... has no effect on global items

This happens when the aspect Global => is not defined but the package has global items or states. I think we should discuss in general how we want to handle global state, especially in regards to procedures that are passed to generic packages. In this case the procedure inside the package that calls the procedure that has been passed into the package somehow needs to define the same global state as the passed procedure.

from gneiss.

Offline discussion: We will handle this in a separate issue #164. Idea: Make generic subprograms Global => null and add a parameter (with a generic type) to pass in global state. For generic subprograms called by the platform we need to find a different solution.

from gneiss.

Currently I cannot prove the block test since we do not have this interface on Linux and proving components only works there. Should we postpone these three tests (client, server, proxy)?

from gneiss.

Yes, we should skip it for now. What would be necessary to enable proof for non-Linux platforms?

from gneiss.

We would have to set up an environment that allows to compile gneiss as a library. For Genode adding the correct source directories could be enough since we dont need to resolve all linker symbols. For Muen for example we would have to provide the whole source/library tree. For the sole purpose of proving applications we could provide an empty proof platform that only has empty implementations (and is not SPARK in its body). But to validate our assumptions (see aliasing) we should at least be able to proof on one real world platform (as far as it is possible).

from gneiss.

OK, so this is related to #86. Beyond that, we should focus on Linux for proof (i.e. sessions not available there cannot be validated right now).

from gneiss.

Fixed by #173.

from gneiss.