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
I have tried running the result of this function through crucible_array, but get type mismatches between SetupValue and CrucibleSetup...so, I'm lost right now. Any help would be appreciated.
The text was updated successfully, but these errors were encountered:
Here's what I have, which seems to work. It initializes numElements objects using init_function which takes the position of the current element being worked on as well as a set of constant parameters. Thank you to everyone who helped!
leterror=do {
crucible_precond {{ True }};
crucible_postcond {{ True }};
return {{ True }};
};
let noerror =do {
return {{ True }};
};
let struct_list_empty =do {
return {s=[], c={{ [] }}} :CrucibleSetup {s : [SetupValue], c :Term};
};
rec struct_list_rec (numElements :Int) (init_function :Int-> a ->CrucibleSetup {s :SetupValue, c :Term}) (params : a) =do {
err <-if (eval_bool {{ (`numElements : [32]) ==0 }}) thenerrorelse noerror; //numElements must be greater than 0
element <- init_function (eval_int {{ (`numElements : [32]) -1 }}) params;
rest <-if (eval_bool {{ (`numElements : [32]) ==1 }}) then struct_list_empty
else struct_list_rec (eval_int {{ (`numElements : [32]) -1 }}) init_function params;
let ret_s = (concat [element.s] rest.s);
let element_c = element.c;
let rest_c = rest.c;
let ret_c = {{ [element_c] # rest_c : [numElements]_ }};
return {s=ret_s, c=ret_c};
};
I'm really struggling to specify an array of arrays in
saw
Consider the following example. How can I (for a given nNumElements and nLength) prove that
clear
zeroes out eachpList
?Using the generic function below, I am able to create a list of the structures, but I can't figure out how to transform this list to an array.
I have tried running the result of this function through
crucible_array
, but get type mismatches betweenSetupValue
andCrucibleSetup
...so, I'm lost right now. Any help would be appreciated.The text was updated successfully, but these errors were encountered: