Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support <stdint.h> for array parameters in cdl-refine spec/proofs #59

Open
ThreeFx opened this issue Mar 13, 2021 · 0 comments
Open

Support <stdint.h> for array parameters in cdl-refine spec/proofs #59

ThreeFx opened this issue Mar 13, 2021 · 0 comments

Comments

@ThreeFx
Copy link
Contributor

ThreeFx commented Mar 13, 2021

Rationale: Many programming languages (in which we would like to write high-assurance code) have support for sized integer types, and being able to use these in array parameters would be very helpful.

They seem to be supported fine using CType when not used in arrays, maybe the fix is as easy as adding CType to the param_type macro in camkes/templates/arch-definitions.thy?

Currently I'm using a workaround passing char instead of uint8_t, but the latter conveys much more cleanly what I want to express (plus char may or may not be unsigned, and unsigned char is not supported).

@ThreeFx ThreeFx changed the title Support <stdint.h> for array parameters Support <stdint.h> for array parameters in cdl-refine spec/proofs Mar 30, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant