-
Notifications
You must be signed in to change notification settings - Fork 62
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
Limiting values inside char array parameter #1864
Comments
The
Can be used as a Cryptol sequence within an
Here is an explanation of what this is doing:
Of course, this is just a small example. You can change the Does this answer your question? |
When I used that code above, it is setting the value of the char array to 65, which is A in ascii. I am comparing it to cryptol code, that returns a value based on what the char is. But when I have set all values to 'A', the cryptol code: else if char == 'a' then ... else error "invalid char" It returns the error. I have also tried checking if the char is equal to 65. Do you know after changing all the values of the char array to 'A' what would the equivalent be in Cryptol? |
I'm not sure I understand what you are trying to do based on the small amount of Cryptol code you've provided. Can you post a more complete example? |
I have some C code I am verifying through SAW:
}
Saw verification:
module <- llvm_load_module "cfile.bc"
let exampleMethod_spec length = do {
};
llvm_verify module "ExampleMethod" [] true (exampleMethod_spec 78) z3;
However I want to limit the value inside the char array to specific values (some range of letters and some range of numbers).
But I haven’t been able to find a so far to do it. Is there an inbuilt function in SAW such as llvm_precond that can limit values inside an array.
Thanks
The text was updated successfully, but these errors were encountered: