2021-01-15 15:54 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001180Frama-CKernelpublic2012-05-16 15:222012-09-19 17:16
Reportermehdi 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001180: Port to OCamlgraph 1.8.2
DescriptionHi,

Recent OCamlgraph 1.8.2 has a non backward compatible change. The change is described in OCamlgraph's changelog as:

 o Topological: fix bug when a cycle depends on another cycle. That breaks
   compatibility: the input graph must implement Sig.COMPARABLE instead of
   Sig.HASHABLE

The attached patch make Frama-c compile (and run properly :)) with OCamlgraph 1.8.2. I wasn't sure whether I should use Pervasives.compare or Datatype.Int.compare. I noticed that the latter is more used so I preferred it over the standard one. Comments on this patch are welcome.

The patch is rather straightforward and easy and I'm (almost) sure you already fixed that but maybe other Frama-C users will need it… and I'm sharing it here.

Regards,

Mehdi
TagsNo tags attached.
Attached Files
  • patch file icon 0007-Port-to-OCamlgraph-1.8.2.patch (2,436 bytes) 2012-05-16 15:22 - 
    From: Mehdi Dogguy <mehdi@debian.org>
Date: Wed, 16 May 2012 14:48:40 +0200
Subject: Port to OCamlgraph 1.8.2

 o Graph.Topological: as of OCamlgraph 1.8.2, the input graph must
   implement Sig.COMPARABLE instead of Sig.HASHABLE
---
 src/misc/service_graph.ml           |    2 +-
 src/misc/service_graph.mli          |    2 +-
 src/semantic_callgraph/register.ml  |    1 +
 src/syntactic_callgraph/register.ml |    1 +
 4 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/misc/service_graph.ml b/src/misc/service_graph.ml
index f30a1be..567698f 100644
--- a/src/misc/service_graph.ml
+++ b/src/misc/service_graph.ml
@@ -24,7 +24,7 @@ module Make
   (G: sig
      type t
      module V: sig
-       include Graph.Sig.HASHABLE
+       include Graph.Sig.COMPARABLE
        val id: t -> int
        val name: t -> string
        val attributes: t -> Graph.Graphviz.DotAttributes.vertex list
diff --git a/src/misc/service_graph.mli b/src/misc/service_graph.mli
index 5ebb570..8006977 100644
--- a/src/misc/service_graph.mli
+++ b/src/misc/service_graph.mli
@@ -28,7 +28,7 @@ module Make
   (G: sig
      type t
      module V: sig
-       include Graph.Sig.HASHABLE
+       include Graph.Sig.COMPARABLE
        val id: t -> int
          (** assume is >= 0 and unique for each vertices of the graph *)
        val name: t -> string
diff --git a/src/semantic_callgraph/register.ml b/src/semantic_callgraph/register.ml
index 0b3b4df..064dca8 100644
--- a/src/semantic_callgraph/register.ml
+++ b/src/semantic_callgraph/register.ml
@@ -107,6 +107,7 @@ module Service =
                (if Kernel_function.is_definition v then `Bold
                 else `Dotted) ]
          let equal = Kernel_function.equal
+         let compare v1 v2 = Datatype.Int.compare (id v1) (id v2)
          let hash = Kernel_function.hash
          let entry_point () =
            try Some (fst (Globals.entry_point ()))
diff --git a/src/syntactic_callgraph/register.ml b/src/syntactic_callgraph/register.ml
index 4efb594..d9d78b9 100644
--- a/src/syntactic_callgraph/register.ml
+++ b/src/syntactic_callgraph/register.ml
@@ -41,6 +41,7 @@ module Service =
              | NIVar (_,b) when not !b -> `Style `Dotted
              | _ -> `Style `Bold ]
          let equal v1 v2 = id v1 = id v2
+         let compare v1 v2 = Datatype.Int.compare (id v1) (id v2)
          let hash = id
          let entry_point () = !entry_point_ref
        end
--
    patch file icon 0007-Port-to-OCamlgraph-1.8.2.patch (2,436 bytes) 2012-05-16 15:22 +

-Relationships
+Relationships

-Notes

~0003017

signoles (manager)

2012-05-16 15:40

 Hi Mehdi,

Thanks for your patch. It is correct.

As you guess, the current SVN version of Frama-C is already up-to-date according to ocamlgraph 1.8.2. Actually, we found the bug in OcamlGraph's topological with a Frama-C's case study: services computed by plug-in "syntactic callgraph" were sometimes wrong in Frama-C Nitrogen (and older release) because of this bug.

Julien
+Notes

-Issue History
Date Modified Username Field Change
2012-05-16 15:22 mehdi New Issue
2012-05-16 15:22 mehdi File Added: 0007-Port-to-OCamlgraph-1.8.2.patch
2012-05-16 15:31 signoles Status new => assigned
2012-05-16 15:31 signoles Assigned To => signoles
2012-05-16 15:40 signoles Note Added: 0003017
2012-05-16 15:40 signoles Status assigned => resolved
2012-05-16 15:40 signoles Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
+Issue History