I just tested and it seems only one error related to this bug (error[HAX0010]) is emitted now.

Command: cargo-hax -C -p edhoc-rs -p edhoc-crypto -p edhoc-ead --no-default-features --features="crypto-hacspec, ead-none" --release \; into -i '-c_wrapper::**' fstar

Code version: main, specifically commit 567669d.

Hax logs:

error[HAX0008]: (reject_RawOrMutPointer) ExplicitRejection { reason: "unknown reason" }
                                                           
error[HAX0010]: (RefMut) At this position, Hax was expecting an expression of the shape `&mut _`. Hax forbids `f(x)` (where `f` expects a mutable reference as input) when `x` is not a place expression[1] or when it is a dereference expres
sion.                                               
                                                           
                [1]: https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions      
   --> lib/src/edhoc.rs:849:17                                                                                                                                                                                                                
    |                                                                                                                  
849 | /                 g_x.copy_from_slice(             
850 | |                     &rcvd_message_1.content[3 + raw_suites_len..3 + raw_suites_len + P256_ELEM_LEN],
851 | |                 );
    | |_________________^                        
                                                           
error[HAX0001]: (CfIntoMonads) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hacspec-v2/issues/96.
                Please upvote or comment this issue if you see this error message.
                TODO: Monad for loop-related control flow
   --> lib/src/lib.rs:332:5                                                                                            
    |                                                                                                                  
332 | /     while conn_id < -24 || conn_id > 23 {
333 | |         conn_id = Crypto::get_random_byte() as i8;
334 | |     }                                    
    | |_____^                                             
                                                           
error[HAX0001]: (FunctionalizeLoops) something is not implemented yet.
                Only for loop are being functionalized for now   
   --> lib/src/lib.rs:332:5                      
    |                        
332 | /     while conn_id < -24 || conn_id > 23 {
333 | |         conn_id = Crypto::get_random_byte() as i8;
334 | |     }                               
    | |_____^

copy_from_slice on a array is not accepted #256

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`copy_from_slice` on a array is not accepted #256