Comments (9)
Efforts to port the Ada conformance tests to Genode are done in Componolit/componolit#125. Maybe we should pursue platform independence here, too. @jklmnn, what do you think?
from ada-runtime.
I'm not sure if the Ada conformance tests are what helps us here since they rather test what the runtime supports instead of its correct functioning (well this is tested of course but probably not as targeted as we need it).
Generally I think that we're not heading into the right direction with tests. Originally I implemented the secondary stack in a separate library and put it into a separate space to compile and prove it independently of the rest of the runtime. This, especially the SPARK part, is what would have prevented #8 in the first place (in my eyes). But this is also what I miss with the current structure of the runtme (runtime files and their implementation are mangled together).
So I propose that we take the effort and refactor the runtime to consequently separate the interface providing parts of the runtime (e.g. s-secsta.ad*
) and the actual implementation (e.g. ss-utils.ad*
) again and prove the implementation. We still should test the runtime in a manner as done now, even more thoroughly.
EDIT: I'd volunteer to do that ;)
from ada-runtime.
I agree that we should better test the runtime. Ideally, we should do test-driven development as done for the secondary stack allocator package. Also, using SPARK at least for dataflow analysis would be great.
I wonder whether we only want to test in the common runtime or also create specific tests for the system-specific parts of the runtime. Having tests in a central place seems useful. Opinions?
We also should decide how to build tests. I'd suggest AUnit (but without gnattest which I found very inconvenient as tests could not be disabled and I was forced to implement many stupid tests for trivial functions. Also, I found no way to add tests for private subprograms.)
Thanks for volunteering!
from ada-runtime.
I'd also do some sort of integration test for the platform dependent parts of the runtime. This would have helped e.g. to recognize that allocate_secondary_stack
returned the wrong side of the stack. Also we could check explicitly for the behaviour we defined in the spec.
While writing trivial tests for some functions isn't really a problem for me not having tests available for private ones is indeed a one (so it seems AUnit only does blackbox tests on packages).
from ada-runtime.
Testing private subprograms is possible in AUnit. I just found no way to use gnattest
for that. So "manual" AUnit should be OK (I use that in JWX).
For the integration test you suggest, the question still remains whether generic integration tests (in the generic runtime) suffice or we need specific tests in the platform repositories.
from ada-runtime.
Oh I failed to make the distinction between AUnit and gnattest.
As far as I understand it we have to run the integration test on the specific platform itself (how could we otherwise test the memory allocation for example?). So the test functions also need to be somewhat platform specific. I would separate them into two parts (like it is done in Acats). One that checks the functional requirements (e.g. if the mapping is correct) and one that takes the same role as the Report package.
from ada-runtime.
I looked into the Aunit Cookbook and the tests autogenerated by gnatmake. Since gnattest does not support private we have to use Aunit without it what means that we have to create all tests manually. This is time consuming but the tests created by gnattest are hardly usable since they depend on some gnattest libraries. Also I doubt that refining them manually requires significantly less time.
from ada-runtime.
IMHO you overestimate the effort required to create tests manually. Once you have the basic setup, this mainly boils down to copying a test case or test suite. I never felt this to be overly complicated. Have a look at the jwx tests.
from ada-runtime.
Closing in favor of #32
from ada-runtime.
Related Issues (20)
- Run Genode depot autopilot tests in CI HOT 1
- Heap allocator
- Tagged types with dynamic dispatching
- Test tagged types on Genode and Muen
- Add weak symbols for memcmp, memcpy in Genode
- nRF52832 support HOT 1
- Reduce log procedures to a single one HOT 2
- STM32F0 support HOT 1
- Support for executing function contracts
- Ada.Numerics.Big_Numbers.Big_Integers HOT 3
- Prove embedded drivers HOT 1
- Annotate global state HOT 1
- Update to GNAT Community 2020 HOT 8
- nRF52 memcpy behaviour HOT 1
- Project always completely rebuilt when runtime is used
- Serial debug support for nRF52832
- Compatibility to GNAT Community 2021 HOT 1
- Compatibility to FSF GNAT 11
- Compatibility to FSF GNAT 12
- Cleanup/deprecation HOT 1
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 ada-runtime.