[CIL users] Bug in Cfg

[Benjamin M. <ben...@ce...>]

Hello,

On this code  :

void main(void)
{ while(1) {;};
   return;
};

Cfg.computFileCfg computes a graph without any loop.

The problems comes from Cfg.cfgStmt.

Here is a patch that seems to fix this problem :

Add after addBlockSucc:
=======================
   let addBlockSuccFull (next:stmt) (b: block) =
     match b.bstmts with
       [] -> addSucc next
     | hd::_ -> addSucc hd
   in
======================
Replace the Loop case by:
==========================
  | Loop(_,blk,_,_,_) ->
       addBlockSuccFull s blk;
       cfgBlock blk (Some s) next (Some s)
===========================

Am I right ?

Thanks again for making Cil so good !
-- 
| Benjamin Monate         | mailto:ben...@ce...     |
| Ingénieur-Chercheur     | CEA-LIST/DRT/DTSI/SOL/LSL         |
| Bât. 528 Pt. 115a       | 91191 Gif-sur-Yvette CEDEX        |
| Tél. 01 69 08 94 09     | Fax : 01 69 08 83 95              |