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

Issue 160, 161, 153, 164, 165, 167: Proof properties for applications #173

Merged
merged 40 commits into from
May 19, 2020
Merged

Issue 160, 161, 153, 164, 165, 167: Proof properties for applications #173

merged 40 commits into from
May 19, 2020

Conversation

jklmnn
Copy link
Member

@jklmnn jklmnn commented May 13, 2020

  • Allow proving applications including global state and all generic code
  • Enable proofs in cement
  • Improve proof coverage of broker
  • Add custom parameters for callbacks to model global application state within interfaces

jklmnn and others added 30 commits April 24, 2020 19:57
@jklmnn
proof of log proxy (WIP)
90ada30 
ref #160
@jklmnn
prove message tests
9680145 
ref #160
@jklmnn
prove Rom test
c5ef73d 
ref #160
@jklmnn
prove Memory tests
4636623 
ref #160
@jklmnn
fix log proxy proof
1d70759 
ref #160
@jklmnn
allow editing and proving with subcommands
6abcfe7 
ref #163
@jklmnn
prove broker packages (WIP)
262de0a 
ref #161
- Main
- Gneiss.Main
- Gneiss.Broker
- Gneiss.Broker.Main
- Gneiss.Broker.Startup
@jklmnn
fix test script
1e81735 
ref #163
@jklmnn
prove broker with only low checks missing
1867325 
ref #161
@jklmnn
fix broken loop condition
f780796 
ref #161
@jklmnn
custom parameter for memory client callback
3e97b53 
ref #165
@jklmnn
split up event procedures
b78fdd1 
ref #165
@jklmnn
improve error messages
8e9b2b9
@jklmnn
custom parameter for rom client callback
45e8750 
ref #165
@jklmnn
custom parameters for log server
9ed538f 
ref #165
@jklmnn
custom parameter and proof for memory server
f4c409e 
ref #165
@jklmnn
custom parameter and proof for message server
cfd24cd 
ref #165
@jklmnn
make log session generic
39da7ad 
ref #165
@jklmnn
prove main properties of log dispatcher
d720fa4 
ref #165
@jklmnn
implement custom parameters on Genode
7987012 
ref #165
@jklmnn
improve proof state of test components
71ef6fc 
ref #160
@jklmnn
Restructure internal Linux implementation to allow hidden platform state
a4190b7 
ref #164
@jklmnn
prove global state of hello world example
1be59d1 
ref #164
@jklmnn
prove global state of log proxy
de32987 
ref #164
@jklmnn
prove global state of memory client
6d21dfa 
ref #164
@jklmnn
prove global state of memory server
1f13eed 
ref #164
@jklmnn
prove global state of message client
0b56cc1 
ref #164
@jklmnn
prove global state of message server
53b38ad 
ref #164
@jklmnn
prove global state of rom client
a9c15d9 
ref #164
@jklmnn
prove global state of timer client
a8cd42f 
ref #164
@jklmnn jklmnn requested a review from senier May 13, 2020 12:55
senier
senier suggested changes May 18, 2020
View reviewed changes
src/core/linux/gneiss-broker-main.adb Outdated Show resolved Hide resolved
src/log/genode/gneiss-log.adb Outdated Show resolved Hide resolved
src/log/server/linux/gneiss-log-dispatcher.adb Show resolved Hide resolved
src/memory/server/gneiss-memory-server.ads Show resolved Hide resolved
src/rom/client/linux/gneiss-rom-client.adb Outdated Show resolved Hide resolved
test/log_proxy/component.adb Outdated Show resolved Hide resolved
test/message_client/component.adb Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Outdated Show resolved Hide resolved
README.md Show resolved Hide resolved
@jklmnn jklmnn merged commit 55bf740 into project_4 May 19, 2020
jklmnn added a commit that referenced this pull request May 19, 2020
@jklmnn
Unify duplicated helper functions
9918912 
ref #173
jklmnn added a commit that referenced this pull request May 19, 2020
@jklmnn
Add clarifications, fix indentation
bb9ad50 
ref #173
This was referenced May 19, 2020
Closed
Closed
Closed
Closed
Closed
Closed
Closed
jklmnn added a commit that referenced this pull request May 20, 2020
@jklmnn
Unify duplicated helper functions
b56cdb1 
ref #173
jklmnn added a commit that referenced this pull request May 20, 2020
@jklmnn
Add clarifications, fix indentation
9e2394d 
ref #173
jklmnn added a commit that referenced this pull request May 20, 2020
@jklmnn
Clarifications in Readme
7e629d8 
ref #173
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@senier senier senier approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@jklmnn @senier