#142 Problem with AddrOfLabel and CopyFunction

[az bro]

CopyFunction doesn't update AddrOfLabel which also
has a ref to the statement containing the label,
just like Goto does.

This is the output I get from the code below:

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
digraph CFG_f_new {
0 [label="0: instr"]
0 -> 1
1 [label="1: goto"]
1 -> 3
2 [label="2: instr"]
2 -> 3
3 [label="3: instr"]
3 -> 4
4 [label="4: return"]

}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
digraph CFG_f_new {
6 [label="6: instr"]
6 -> 7
7 [label="7: goto"]
7 -> 3
8 [label="8: instr"]
8 -> 9
9 [label="9: instr"]
9 -> 10
10 [label="10: return"]

}

====================================================================================

open List

let () = begin
Cil.useComputedGoto := true;
Cil.insertImplicitCasts := true;
Cil.print_CIL_Input := false;
Cil.lineDirectiveStyle := None;
end

let feature : Cil.featureDescr = {
Cil.fd_name = "CFGTest";

Cil.fd_enabled = ref false;

Cil.fd_description = "";

Cil.fd_extraopt = [ ];

Cil.fd_doit = (fun f ->
let funG = List.find (fun g ->
match g with
| GFun(func,) when func.svar.vname = "f" -> true
| _ -> false
) f.globals in
let func = match funG with
| GFun(func,) -> func
| _ -> raise (Failure("GFun"))
in (
ignore(Cfg.clearCFGinfo func);
ignore(Cfg.cfgFun func);

      let newFunc = Cil.copyFunction func "f_new" in (
         print_endline("\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%");
         Cfg.printCfgChannel stdout newFunc;
         print_endline("\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%");

         ignore(Cfg.clearCFGinfo newFunc);
         ignore(Cfg.cfgFun newFunc);

         print_endline("\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%");
         Cfg.printCfgChannel stdout newFunc;
         print_endline("\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%");
      )
  )

);

Cil.fd_post_check = true
}

====================================================================================

include<stdio.h>

int f() {
void lll = &&lab1;
goto lll;
printf("xxx\n");
lab1:
printf("yyy\n");
return 0;
}

int main () {
int v;
v = f();
}

====================================================================================

[Gabriel Kerneis]

Patch pending testing in branch fix-copyfunction.