[kernel] Ast-diff mark func with different code annot has having changed body

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

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

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