fix sawscript for bitfields
@@ -59,8 +59,18 @@ let config_cca_type config = (crucible_field config "client_cert_auth_type");
let ocsp_status_size cert_and_key =
crucible_field (crucible_field (cert_and_key) "ocsp_status") "size";
-//conn->config->use_tickets
-let config_use_tickets config = (crucible_field config "use_tickets");
+//conn->config->use_tickets is the field we care about, but it is
+// in a bitfield. For now, we only care about that, so we point
+// at the entire bitfield and say it must all be initialized to
+// a value of 0 for the proof to go through. This is a stronger
+// statement than we stricly need to make, and will limit
+// compositional proofs in the future, but we can make more
+// precise statements at that time
+
+// It's also noteworthy that we use the crucible_elem here, which will
+// cause problems if the fields are reordered. This is reasonably unlikely
+// because it makes sense to have the bitfield at the start
+let config_bitfield config = (crucible_elem config 0);
//conn->session_ticket_status
let conn_session_ticket_status pconn = (crucible_field pconn "session_ticket_status");
@@ -142,9 +152,11 @@ let setup_connection = do {
crucible_points_to (ocsp_status_size cak) (crucible_term status_size);
crucible_equal (crucible_term status_size) (crucible_term {{zero : [32]}});
- use_tickets <- crucible_fresh_var "use_tickets" (llvm_int 8);
- crucible_points_to (config_use_tickets config) (crucible_term use_tickets);
- crucible_equal (crucible_term use_tickets) (crucible_term {{zero : [8]}});
+ config_bitfield_value <- crucible_fresh_var "config_bitfield" (llvm_int 8);
+ crucible_points_to (config_bitfield config) (crucible_term config_bitfield_value);
+ // The following line could be made more precise, we only care that the use_tickets
+ // bit is zero
+ crucible_equal (crucible_term config_bitfield_value) (crucible_term {{zero : [8]}});
session_ticket_status <- crucible_fresh_var "session_ticket_status" (llvm_int 32);
crucible_points_to (conn_session_ticket_status pconn) (crucible_term session_ticket_status);
