Johannes Kanig
4981cd565d
Remove invalid successors invariant from context predicate
...
Ref. eng/recordflux/RecordFlux#1802
2024-10-29 17:27:24 +09:00
Andres Toom
5c667469c5
Use shorthand unsigned type definitions in examples and tests
...
Ref. eng/recordflux/RecordFlux#1398
2024-10-28 19:46:09 +00:00
Johannes Kanig
abc1dc6077
Remove Buffer argument when possible in helper functions
...
Ref. eng/recordflux/RecordFlux#1802
2024-10-21 23:47:45 +00:00
Tobias Reiher
24fdb9de8e
Rename Session to State Machine
...
Ref. eng/recordflux/RecordFlux#1772
2024-09-11 08:50:18 +00:00
Tobias Reiher
6c0c94d688
Enable SPARK proofs for SPDM responder example
...
Ref. eng/recordflux/RecordFlux#1704
2024-09-06 17:43:00 +02:00
Tobias Reiher
1677c46a85
Fix unused variables in SPDM responder example
...
Ref. eng/recordflux/RecordFlux#1704
2024-09-06 17:43:00 +02:00
Tobias Reiher
26d8c3759b
Fix missing checks in state machine
...
Ref. eng/recordflux/RecordFlux#1704
2024-09-06 17:43:00 +02:00
Tobias Reiher
63738d1074
Fix initialization of SPDM responder
...
Ref. eng/recordflux/RecordFlux!1663
2024-09-04 09:26:56 +00:00
Tobias Reiher
97d97a9fc8
Fix description in SPDM responder example
...
Ref. eng/recordflux/RecordFlux!1663
2024-09-04 09:26:56 +00:00
Tobias Reiher
81b56d5c38
Rename *_Functions.Context to *_Environment.State
...
Ref. eng/recordflux/RecordFlux#1769
2024-09-04 09:26:56 +00:00
Tobias Reiher
802c6baa46
Remove Initialize and Finalize functions for functions context
...
Ref. eng/recordflux/RecordFlux#1768
2024-09-04 09:26:56 +00:00
Tobias Reiher
bca2e60adc
Refactor SPDM responder specification and docstrings
...
Ref. eng/recordflux/RecordFlux!1645
2024-08-08 08:55:36 +00:00
Tobias Reiher
7c29a5af02
Fix separation of externally defined functions from state machine
...
Ref. eng/recordflux/RecordFlux#1032
2024-08-08 08:55:36 +00:00
Tobias Reiher
63d3a475b7
Fix GNATprove caching for SPDM responder example
...
Ref. None
2024-07-19 09:09:39 +00:00
Tobias Reiher
90f25f325f
Reduce timeout for SPDM verification
...
Ref. eng/recordflux/RecordFlux#1670
2024-07-03 12:45:41 +03:00
Tobias Reiher
cc68068e71
Fix GNAT Studio errors in example apps
...
Ref. eng/recordflux/RecordFlux#1492
2024-04-17 12:02:00 +00:00
Johannes Kanig
9ab5b4f937
remove cvc4 from project files
2023-11-28 09:49:49 +09:00
Andres Toom
70928e8f36
Refine the spdm_responder's build directories
...
All the files produced in the build process go to a common build
directory and the subfolders for the different target platforms
follow a similar hierarchy.
2023-11-19 19:33:07 +00:00
Tobias Reiher
2139ff0dfe
Fix duplicate code generation for SPDM example
...
Ref. eng/recordflux/RecordFlux#1449
2023-11-10 10:15:06 +00:00
Tobias Reiher
3edb6da430
Remove unused type in SPDM specification
2023-11-08 13:44:03 +00:00
Alexander Senier
046f55d8f5
Deprecate short-form if for message fields
2023-11-03 14:26:57 +00:00
Johannes Kanig
fc8374d6b0
new function Valid_Next_Internal
...
- groups Path_Condition and Valid_Predecessor functionality
- will be used in preconditions of other future internal functions
- adjust sizes for SPDM as this commit seems to slightly increase code
size
For eng/recordflux/recordflux#1382
2023-09-13 23:01:46 +00:00
Tobias Reiher
ba0877d97e
Reduce occurrence of failed code generation in CI
2023-09-06 16:22:36 +02:00
Tobias Reiher
d1310afda4
Unify directory structures of example apps
2023-08-18 19:08:42 +02:00
Tobias Reiher
31ae2485b0
Add SPDM responder example
...
Ref. eng/recordflux/RecordFlux#1367
2023-08-18 14:37:32 +02:00
