From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 7DFABBC57 for ; Wed, 21 Jul 2010 04:59:27 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvUBAI7/RUzRVdg2kGdsb2JhbACTMow5CBUBAQEBCQkMBxEDH68FghCGBC6IVAEBAwWFLQSDfoRb X-IronPort-AV: E=Sophos;i="4.55,235,1278280800"; d="scan'208";a="54548110" Received: from mail-qw0-f54.google.com ([209.85.216.54]) by mail3-smtp-sop.national.inria.fr with ESMTP; 21 Jul 2010 04:59:26 +0200 Received: by qwg5 with SMTP id 5so3389704qwg.27 for ; Tue, 20 Jul 2010 19:59:26 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:date:message-id :subject:from:to:content-type; bh=OW/Z8N7FE2rXucHVNkb/DtU5UcACESBFlOsNIqFJMBw=; b=hn9lLN+tikn2HIDZLpERK4LIAnVyXVCuombo/fG8LoVfqohuR8KLNHoflXEAApepX8 rT04MZLzsrV6qVeBeFRD6B+b3ZQzkI3Xq5RrPdd07RMJ80WgHu4TRVfnvFuYxrfnDg5U 1n6ZyId+XvlDwJrDrD74L02+gud4Y/7OGQP68= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=e4g1QhXtxCB3VAM5++RU5M+Yc12XM/NWJb/aXjC7sZ8wjMILedPrWfQYUQIxjd+Re9 /4h8+oQNRJ171ja4rMqpgdDtejMt5LmyBw2LkltGRmw2HIqpNxG/nYem2g/Q6+QfzsU4 fTQx3YWonU+fr3Zh+XulOfGyhaQuzLtyk+YNs= MIME-Version: 1.0 Received: by 10.224.54.69 with SMTP id p5mr6360008qag.264.1279681165245; Tue, 20 Jul 2010 19:59:25 -0700 (PDT) Received: by 10.229.231.80 with HTTP; Tue, 20 Jul 2010 19:59:25 -0700 (PDT) Date: Wed, 21 Jul 2010 10:59:25 +0800 Message-ID: Subject: issues on modifying code in ext/cfg.ml in CIL From: haihao shen To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=0015175cdee247bd70048bdcfded X-Spam: no; 0.00; becuase:01 becuase:01 highlighted:98 W12:98 W12:98 highlighted:98 cfg:01 cfg:01 modifying:02 match:02 match:02 let:03 let:03 conditional:04 conditional:04 --0015175cdee247bd70048bdcfded Content-Type: text/plain; charset=ISO-8859-1 Hi all, Currently I am doing some work on CIL. I would like to obtain the conditional result (true/false) in the DOT file generated by CIL. Therefore, I modified the code in ext/cfg.ml. let d_cfgedge (src) () (dest) = match src.skind with | If (_, tb, fb, _) -> (if (List.mem dest tb.bstmts) then dprintf "%a -> %a [label=\"true\"]" d_cfgnodename src d_cfgnodename dest else if (List.mem dest fb.bstmts) then dprintf "%a -> %a [label=\"false\"]" d_cfgnodename src d_cfgnodename dest else dprintf "%a -> %a [label=\"true$\"]"(*true likely, note that no false likely!!!*) d_cfgnodename src d_cfgnodename dest); | _ -> dprintf "%a -> %a" d_cfgnodename src d_cfgnodename dest However, I am wondering whether my solution is correct becuase there is no related document explaining this issue. In particularly, in my real cases, I found the highlighted case is also hit. I am also wondering whether there are other cases that I don't consider here. Look forward to your reply. Any concern or feedback would be greatly appreciated. Thanks, Haihao --0015175cdee247bd70048bdcfded Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Hi all,
=A0
Currently I am doing some work on CIL. I would like to obtain the cond= itional result (true/false) in the DOT file generated by CIL. Therefore, I = modified the code in ext/cfg.ml.
=A0
let d_cfgedge (src) () (dest) =3D=A0
=A0=A0=A0 match src.skind with=
=A0=A0=A0=A0=A0 | If (_, tb, fb, _) ->
=A0=A0 (if (List.mem dest = tb.bstmts) then
=A0=A0=A0=A0=A0 dprintf "%a -> %a [label=3D\&quo= t;true\"]"
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 d_cfgnodename = src
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 d_cfgnodename dest
=A0=A0=A0 else i= f (List.mem dest fb.bstmts) then
=A0=A0=A0=A0=A0 dprintf "%a -> = %a [label=3D\"false\"]"
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0 d_cfgnodename src
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 d_cfgnodename= dest
=A0=A0=A0 else
=A0=A0=A0=A0=A0 dprintf "%a -> %a [label=3D\"true$\"]&quo= t;(*true likely, note that no false likely!!!*)
=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0 d_cfgnodename src
=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 d_cf= gnodename dest);
=A0=A0=A0=A0=A0 | _ -> dprintf "%a ->= %a"
=A0=A0=A0=A0=A0=A0=A0 d_cfgnodename src
=A0=A0=A0=A0=A0=A0=A0 d_cfgnoden= ame dest
=A0
However, I am wondering whether my solution is correct becuase there i= s no related document explaining this issue. In particularly, in my real ca= ses, I found the highlighted case is also hit. I am also wondering whether = there are other cases that I don't consider here.
=A0
Look forward to your reply. Any=A0concern or feedback=A0would be great= ly appreciated.=A0
=A0
Thanks,
Haihao
--0015175cdee247bd70048bdcfded--