WIP adapting low-level spec to the changes in the code
@@ -132,8 +132,8 @@ let verify_state_machine_elem sm ixt = do {
};
// For now axiomitize this is always false and see if we can prove something
-let s2n_is_caching_enabled_spec = do {
- pconf <- crucible_alloc (llvm_struct "struct.s2n_config");
+let s2n_allowed_to_cache_connection_spec = do {
+ pconf <- crucible_alloc (llvm_struct "struct.s2n_connection");
crucible_execute_func [pconf];
crucible_return (crucible_term {{ 0 : [32] }});
@@ -283,14 +283,14 @@ let s2n_handshake_io_lowlevel = do {
s2n_socket_was_corked <- crucible_llvm_unsafe_assume_spec llvm "s2n_socket_was_corked" s2n_socket_was_corked_spec;
print "s2n_connection_is_managed_corked";
s2n_connection_is_managed_corked <- crucible_llvm_unsafe_assume_spec llvm "s2n_connection_is_managed_corked" s2n_connection_is_managed_corked_spec;
- print "s2n_is_caching_enabled";
- s2n_is_caching_enabled <- crucible_llvm_unsafe_assume_spec llvm "s2n_is_caching_enabled" s2n_is_caching_enabled_spec;
+ print "s2n_allowed_to_cache_connection";
+ s2n_allowed_to_cache_connection <- crucible_llvm_unsafe_assume_spec llvm "s2n_allowed_to_cache_connection" s2n_allowed_to_cache_connection_spec;
let dependencies = [s2n_socket_write_uncork, s2n_socket_write_cork, s2n_socket_was_corked, s2n_connection_is_managed_corked];
print "Proving correctness of s2n_advance_message";
s2n_advance_message_proof <- crucible_llvm_verify llvm "s2n_advance_message" dependencies true s2n_advance_message_spec yices;
print "Proving correctness of s2n_conn_set_handshake_type";
- s2n_conn_set_handshake_type_proof <- crucible_llvm_verify llvm "s2n_conn_set_handshake_type" [s2n_is_caching_enabled] true s2n_conn_set_handshake_type_spec yices;
+ s2n_conn_set_handshake_type_proof <- crucible_llvm_verify llvm "s2n_conn_set_handshake_type" [s2n_allowed_to_cache_connection] true s2n_conn_set_handshake_type_spec yices;
print "done";
return ();
};
