Comments (9)
@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.
Related Issues (20)
- Timer session on Linux HOT 1
- Consolidation HOT 1
- Prove broker HOT 1
- Fix file descriptor leaks
- Allow proving, editing and compiling as different commands in cement HOT 1
- Prove globals HOT 4
- Custom parameters for generic operations HOT 3
- GPIO Debug HOT 1
- Update ada-runtime, rename init to core/linux HOT 1
- Add support for different platforms to cement HOT 1
- Matrix Demo
- ICMP Demo HOT 4
- Update README HOT 1
- Global platform state for volatile inputs
- Update to CE 2020 HOT 5
- Update to RecordFlux 0.4.0 HOT 1
- Stream interface HOT 1
- Run checkers on cement
- SPI driver
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from gneiss.