You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+5Lines changed: 5 additions & 0 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -16,4 +16,9 @@ Word arrays are a commonly used data structure, especially in low level
16
16
systems, so verifying these would be beneficial as this would reduce the
17
17
overall cost of verification of any project that requires word arrays.
18
18
19
+
The file WordArray.cogent contains the trivial Cogent program to generate the C implementations of the word array functions.
20
+
The file WordArraySpec.thy contains the specification for word arrays.
21
+
The file WordArrayT.thy contains the proofs of functional correctness and frame constraint satisfiability.
22
+
The file main_pp_inferred.c is generated from the files main.ac and entrypoints.cfg from the make file Makefile. This file contains the C implementations of the word array functions.
0 commit comments