2021-01-15 18:40 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001279Frama-CPlug-in > wppublic2012-10-13 03:35
Reportersjw 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusassignedResolutionopen 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in Version 
Summary0001279: Multiple branches to a label/loop entries crashes wp
DescriptionThe following code:

/*@ ensures \result == x; */
int test(int x)
{
 again:
    if (x > 10)
        goto again;

    if (x > 10)
        goto again;

    return x;
}

gives

$ ~/frama-c/bin/frama-c -wp doublegoto.c
[kernel] preprocessing with "gcc -C -E -I. doublegoto.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] failure: CFG node <loop-1> has 2 successors instead of 1
...

This is caused by the use of a list for loop headers in cil2cfg.ml. The
attached patch fixes this by using a set of nodes.
TagsNo tags attached.
Attached Files
  • diff file icon goto.diff (2,356 bytes) 2012-10-13 03:35 -
    diff -u -r frama-c-Oxygen-20120901-orig/src/wp/cil2cfg.ml frama-c-Oxygen-20120901/src/wp/cil2cfg.ml
    --- frama-c-Oxygen-20120901-orig/src/wp/cil2cfg.ml	2012-10-12 16:09:36.000000000 -0700
    +++ frama-c-Oxygen-20120901/src/wp/cil2cfg.ml	2012-10-12 18:01:48.000000000 -0700
    @@ -1069,14 +1069,14 @@
       type tenv = { graph : t ;
                     dfsp : (node, int) Hashtbl.t;
                     iloop_header : (node, node) Hashtbl.t;
    -                loop_headers : node list ;
    +                loop_headers : Nset.t ; (* We need to remove duplicates *)
                     irreducible : node list ;
                     unstruct_coef : int }
     
       let init cfg =
         let env = { graph = cfg ;
                     dfsp = Hashtbl.create 97; iloop_header =  Hashtbl.create 7;
    -                loop_headers = []; irreducible = []; unstruct_coef = 0 } in
    +                loop_headers = Nset.empty; irreducible = []; unstruct_coef = 0 } in
           env, cfg_start cfg
     
       let eq_nodes = CFG.V.equal
    @@ -1091,7 +1091,7 @@
       let get_iloop_header env b =
         try Some (Hashtbl.find env.iloop_header b) with Not_found -> None
     
    -  let add_loop_header env h = { env with loop_headers = h :: env.loop_headers}
    +  let add_loop_header env h = { env with loop_headers = Nset.add h env.loop_headers}
       let add_irreducible env h = { env with irreducible = h :: env.irreducible}
       let add_reentry_edge env _ _ = (* TODO *) env
     
    @@ -1099,6 +1099,8 @@
     
       let fold_succ f env n = fold_succ (fun v env -> f env v) env.graph n env
     
    +  let fold_loops f env n = Nset.fold f (env.loop_headers) n
    +
       let unstructuredness env =
         let k = float_of_int env.unstruct_coef in
         let k = k /. (float_of_int (CFG.nb_edges (cfg_graph env.graph))) in
    @@ -1141,7 +1143,7 @@
                 debug "to loop edge %a@." pp_edge e
             in iter_pred_e mark_back_edge cfg h; true
       in
    -  let mark_loop loops h =
    +  let mark_loop h loops =
         debug "loop head in %a@." VL.pretty h;
         let is_natural =
           if (LoopInfo.is_irreducible env h) then
    @@ -1165,7 +1167,7 @@
                 insert_loop_node cfg h (Vloop2 (false, n))
         in loop::loops
       in
    -  let loops = List.fold_left mark_loop [] env.LoopInfo.loop_headers in
    +  let loops = LoopInfo.fold_loops mark_loop env [] in
         debug2 "unstructuredness coef = %f@." (LoopInfo.unstructuredness env);
         { cfg with loop_nodes = Some loops }
    
    diff file icon goto.diff (2,356 bytes) 2012-10-13 03:35 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2012-10-13 03:35 sjw New Issue
2012-10-13 03:35 sjw Status new => assigned
2012-10-13 03:35 sjw Assigned To => correnson
2012-10-13 03:35 sjw File Added: goto.diff
+Issue History