diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml index 2528fc011f38888c66bb935d669e0b6d05444fe0..1c6eb15b7f70e459f651ddd8b7a710665142a40c 100644 --- a/src/kernel_services/ast_queries/ast_diff.ml +++ b/src/kernel_services/ast_queries/ast_diff.ml @@ -268,6 +268,9 @@ let make_correspondence candidate has_same_spec code_corres = | true, ((`Body_changed|`Callees_changed) as c) -> `Partial(candidate, c) +let make_body_correspondence has_same_spec code_corres = + if has_same_spec then code_corres else `Body_changed + let (&&>) (res,env) f = match res with | `Body_changed -> `Body_changed, env @@ -1169,8 +1172,9 @@ and is_same_stmt s s' env = | _ -> `Body_changed, env end else `Body_changed, env in - let res = make_correspondence s' annot_res code_res in - Stmt.add s res; code_res, env + let corres = make_correspondence s' annot_res code_res in + let res = make_body_correspondence annot_res code_res in + Stmt.add s corres; res, env (* is_same_block will return its modified environment in order to update correspondence table with respect to locals, in case diff --git a/tests/syntax/oracle/ast_diff_1.0.res.oracle b/tests/syntax/oracle/ast_diff_1.0.res.oracle index 29789a1eea1dbdaa1347252d997f2a2840b2e141..fbb86f340f5f9bfe962414c2d0da05c5cd549ea2 100644 --- a/tests/syntax/oracle/ast_diff_1.0.res.oracle +++ b/tests/syntax/oracle/ast_diff_1.0.res.oracle @@ -16,7 +16,6 @@ [AST diff test] Variable has_static_local_x: => has_static_local_y [AST diff test] Variable i: => i [AST diff test] Variable i_0: => i_0 -[AST diff test] Variable i_0: => i_0 [AST diff test] Variable local_var_use: => local_var_use [AST diff test] Variable ptr_func: => ptr_func [AST diff test] Variable s: => s @@ -47,5 +46,5 @@ [AST diff test] Function use_s: => use_s [AST diff test] Function with_goto_changed: -> with_goto_changed (body changed) [AST diff test] Function with_goto_unchanged: => with_goto_unchanged -[AST diff test] Function with_loop_unroll_diff: => with_loop_unroll_diff +[AST diff test] Function with_loop_unroll_diff: -> with_loop_unroll_diff (body changed) [AST diff test] Function with_loop_unroll_same: => with_loop_unroll_same diff --git a/tests/syntax/oracle/ast_diff_1.1.res.oracle b/tests/syntax/oracle/ast_diff_1.1.res.oracle index 05b4855366c2f31722828604d9603954cc227c55..30191fcff0a2c7db4e5c570acdb5667a0d137caf 100644 --- a/tests/syntax/oracle/ast_diff_1.1.res.oracle +++ b/tests/syntax/oracle/ast_diff_1.1.res.oracle @@ -15,7 +15,6 @@ [AST diff test] Variable has_static_local_x: => has_static_local_y [AST diff test] Variable i: => i [AST diff test] Variable i_0: => i_0 -[AST diff test] Variable i_0: => i_0 [AST diff test] Variable local_var_use: => local_var_use [AST diff test] Variable ptr_func: => ptr_func [AST diff test] Variable s: N/A @@ -45,5 +44,5 @@ [AST diff test] Function use_s: N/A [AST diff test] Function with_goto_changed: -> with_goto_changed (body changed) [AST diff test] Function with_goto_unchanged: => with_goto_unchanged -[AST diff test] Function with_loop_unroll_diff: => with_loop_unroll_diff +[AST diff test] Function with_loop_unroll_diff: -> with_loop_unroll_diff (body changed) [AST diff test] Function with_loop_unroll_same: => with_loop_unroll_same