diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml index 57d5aa8a9381144c88d0f04973279ad527cb3ff6..9152b5e455fd39d1c64ef5e1836b8beb0872b28a 100644 --- a/src/kernel_services/ast_data/annotations.ml +++ b/src/kernel_services/ast_data/annotations.ml @@ -324,7 +324,7 @@ let merge_loop_assigns_emitters annots = let elt = match Behavior_set_map.find_opt bhvs acc with | Some (a',e') -> - let a' = merge_assigns ~keep_empty:false a' a in + let a' = merge_assigns ~keep_empty:false a a' in let e' = if Emitter.equal e e' then e else Emitter.kernel in a', e' | None -> a,e @@ -350,7 +350,7 @@ let merge_loop_allocation annots = let elt = match Behavior_set_map.find_opt bhvs acc with | Some (a', e') -> - let a' = merge_allocation ~keep_empty:false a' a in + let a' = merge_allocation ~keep_empty:false a a' in let e' = if Emitter.equal e e' then e else Emitter.kernel in a', e' | None -> a,e @@ -377,7 +377,10 @@ let partition_code_annot_emitter l = else if Logic_utils.is_allocation ca then contracts,assigns,v::alloc,others else (contracts,assigns,alloc,v::others) in - List.fold_left add_one_ca ([],[],[],[]) l + let (contracts,assigns,alloc,others) = + List.fold_left add_one_ca ([],[],[],[]) l + in + List.(rev contracts, rev assigns, rev alloc, rev others) let code_annot_emitter ?filter stmt = try @@ -409,7 +412,7 @@ let code_annot_emitter ?filter stmt = merge_stmt_contracts_emitters contracts @ merge_loop_assigns_emitters assigns @ merge_loop_allocation allocation @ - List.rev others + others with Not_found -> [] diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle index ef6224bb447e03550381c8c205c6feb41da0f37e..6c66a3027f5e460bd9c2f940af4e5161e5b44de4 100644 --- a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle +++ b/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle @@ -275,8 +275,8 @@ int main(void) /*@ ghost main_pre_func(); */ /*@ assigns X; */ X ++; - /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf, - in_main; + /*@ assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf, + in_main, X; */ f(); /*@ ghost main_post_func(X); */ diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle index 7e00479c453e3e785b4726a59de9906430c04c39..2434556b05d580bac96d12dfa195f2e84cc9ee09 100644 --- a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle +++ b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle @@ -213,7 +213,7 @@ int main(void) /*@ ghost main_pre_func(); */ /*@ assigns X; */ X ++; - /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; */ + /*@ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, X; */ f(); /*@ ghost main_post_func(X); */ return X;