Skip to content
This repository has been archived by the owner on May 22, 2023. It is now read-only.

Proof of tests and platform code #80

Open
6 of 37 tasks
jklmnn opened this issue Aug 7, 2019 · 2 comments
Open
6 of 37 tasks

Proof of tests and platform code #80

jklmnn opened this issue Aug 7, 2019 · 2 comments
Assignees
@jklmnn

Comments

@jklmnn
Copy link
Member

jklmnn commented Aug 7, 2019 •
edited
Loading

To consolidate the current implementation all tests and the platform code written in SPARK should be proven for the absence of runtime errors.

  • test/hello_world
  • test/rom
  • test/timer
  • test/block_client
  • test/block_server
  • test/block_proxy
  • src/common/*strings
  • src/common/*strings_generic
  • src/log/client/genode/*log-client
  • src/log/client/linux/*log-client
  • src/log/client/muen/*log-client
  • src/rom/client/genode/*rom-client
  • src/rom/client/linux/*rom-client
  • src/rom/client/muen/*rom-client
  • src/timer/timer*
  • src/timer/client/genode/*timer-client
  • src/timer/client/linux/*timer-client
  • src/timer/client/muen/*timer-client
  • src/block/*block
  • src/block/client/genode/*block-client
  • src/block/client/linux/*block-client
  • src/block/client/muen/*block-client
  • src/block/server/genode/*block-server
  • src/block/server/genode/*block-dispatcher
  • src/block/server/genode/cxx-block-server
  • src/block/server/genode/cxx-block-dispatcher
  • src/block/server/muen/*block-server
  • src/block/server/muen/*block-dispatcher
  • src/platform/genode/*component
  • src/platform/linux/*component
  • src/platform/muen/*component
  • src/platform/muen/*main
  • src/platform/muen/*muen
  • src/platform/muen/*muen
  • src/platform/muen/*muen_registry
  • src/platform/muen/*muchannel_reader
  • src/platform/muen/*muchannel_writer

This list lists all units that should be proven. The * is only used to shorten componolit-interfaces-. The units are selected by all packages that have bodies or that implement expression functions if they don't have a body. Also all generic packages should be proven via the tests that use them.
@jklmnn
Copy link
Member Author

jklmnn commented Aug 7, 2019

Also the CI should run the proofs for all of these tests. This is currently only true for Linux.

jklmnn added a commit that referenced this issue Aug 7, 2019
@jklmnn
prove block client test
06eb7a8 
ref #80
jklmnn added a commit that referenced this issue Aug 7, 2019
@jklmnn
prove block server test
06972a0 
ref #80
jklmnn added a commit that referenced this issue Aug 8, 2019
@jklmnn
update block proxy test architecture
011813a 
ref #80
jklmnn added a commit that referenced this issue Aug 8, 2019
@jklmnn
improve contracts of block client and server
dca8713 
ref #80
senier pushed a commit that referenced this issue Aug 8, 2019
@jklmnn @senier
prove block client test
19d9313 
ref #80
senier pushed a commit that referenced this issue Aug 8, 2019
@jklmnn @senier
prove block server test
16e0993 
ref #80
senier pushed a commit that referenced this issue Aug 8, 2019
@jklmnn @senier
update block proxy test architecture
8f9fb29 
ref #80
senier pushed a commit that referenced this issue Aug 8, 2019
@jklmnn @senier
improve contracts of block client and server
ea8dd30 
ref #80
jklmnn added a commit that referenced this issue Aug 20, 2019
@jklmnn
prove rom test parse procedure
0b05cfe 
ref #80
jklmnn added a commit that referenced this issue Aug 20, 2019
@jklmnn
add proof annotation
8bcd451 
ref #80
jklmnn added a commit that referenced this issue Aug 26, 2019
@jklmnn
prove rom test
5e6b72d 
ref #80
jklmnn added a commit that referenced this issue Aug 26, 2019
@jklmnn
prove timer test
82f9d06 
ref #80
jklmnn added a commit that referenced this issue Aug 26, 2019
@jklmnn
fix muen block server test proof
292e592 
ref #80
@jklmnn
Copy link
Member Author

jklmnn commented Aug 26, 2019

There are two checks in the block proxy that are not yet proved due to the incorrect preconditions on the types operators.

jklmnn added a commit that referenced this issue Aug 27, 2019
@jklmnn
prove rom test
aad2620 
ref #80
jklmnn added a commit that referenced this issue Aug 27, 2019
@jklmnn
prove timer test
a8cf491 
ref #80
jklmnn added a commit that referenced this issue Aug 27, 2019
@jklmnn
fix muen block server test proof
5cce2ea 
ref #80
senier pushed a commit that referenced this issue Aug 27, 2019
@jklmnn @senier
prove rom test
d96e8fc 
ref #80
senier pushed a commit that referenced this issue Aug 27, 2019
@jklmnn @senier
prove timer test
3271b67 
ref #80
senier pushed a commit that referenced this issue Aug 27, 2019
@jklmnn @senier
fix muen block server test proof
0afcd4f 
ref #80
senier pushed a commit that referenced this issue Sep 24, 2019
@jklmnn @senier
prove block client test
8539f06 
ref #80
senier pushed a commit that referenced this issue Sep 24, 2019
@jklmnn @senier
prove block server test
791fe08 
ref #80
senier pushed a commit that referenced this issue Sep 24, 2019
@jklmnn @senier
update block proxy test architecture
cbec83d 
ref #80
senier pushed a commit that referenced this issue Sep 24, 2019
@jklmnn @senier
improve contracts of block client and server
8063a72 
ref #80
senier pushed a commit that referenced this issue Sep 24, 2019
@jklmnn @senier
prove rom test
6eb3610 
ref #80
senier pushed a commit that referenced this issue Sep 24, 2019
@jklmnn @senier
prove timer test
3c9713b 
ref #80
senier pushed a commit that referenced this issue Sep 24, 2019
@jklmnn @senier
fix muen block server test proof
4a7a342 
ref #80
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@jklmnn jklmnn

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@jklmnn