dune

banal/banal_rat.ml

@@ -1,54 +1,58 @@
-(* 
-   Mathematical rationals.
-
-   Copyright (C) 2011 Antoine Miné
-*)
+(* Mathematical rationals. Copyright (C) 2011 Antoine Miné *)
 
 open Apron
-
 module Int = Banal_int
 module Intinf = Banal_intinf
 module Datatypes = Banal_datatypes
-
 include Q
 
 type base = t
 
 (* conversions are exact *)
 let of_base x = x
-let of_int_up = of_bigint 
+
+let of_int_up = of_bigint
+
 let of_int_down = of_bigint
+
 let of_float_up = of_float
+
 let of_float_down = of_float
+
 let to_base x = x
 
 (* arithmetics is exact *)
 let add_up = add
+
 let sub_up = sub
+
 let mul_up = mul
+
 let div_up = div
+
 let add_down = add
+
 let sub_down = sub
+
 let mul_down = mul
-let div_down = div 
 
-let is_finite x = Int.sign x.den <> 0
+let div_down = div
 
+let is_finite x = Stdlib.( <> ) (Int.sign x.den) 0
 
 (* apron and mlgmpidl *)
 
-let to_mpqf x = 
+let to_mpqf x =
   match classify x with
-  | INF ->  Mpqf.of_mpq Intinf.mpq_inf
-  | MINF ->  Mpqf.of_mpq Intinf.mpq_minf
+  | INF -> Mpqf.of_mpq Intinf.mpq_inf
+  | MINF -> Mpqf.of_mpq Intinf.mpq_minf
   | UNDEF -> invalid_arg "Rat: undefined rational"
   | _ -> Mpqf.of_mpz2 (Int.to_mpz (num x)) (Int.to_mpz (den x))
 
 let of_mpqf x =
   make (Int.of_mpzf (Mpqf.get_num x)) (Int.of_mpzf (Mpqf.get_den x))
 
-let to_apron x =
-  Scalar.Mpqf (to_mpqf x)
+let to_apron x = Scalar.Mpqf (to_mpqf x)
 
 let of_apron_up = function
   | Scalar.Float x -> of_float_up x

banal/dune

@@ -0,0 +1,14 @@
+(library
+ (name banal)
+ (libraries zarith utils apron frontend oUnit apron.boxMPQ apron.octMPQ
+   apron.polkaMPQ)
+ (foreign_stubs
+  (language c)
+  (names ml_float))
+ (flags
+  (:standard -open Utils -open Frontend -open Apron)))
+
+(env
+ (dev
+  (flags
+   (:standard -w -9-27-32-33-35 -warn-error -A))))

banal/ml_float.c

@@ -47,25 +47,25 @@ double ml_div_flt_f(double a, double b)
 value ml_add_flt(value a, value b)
 {
   CAMLparam2(a,b);
-  CAMLreturn(copy_double((float)(Double_val(a) + Double_val(b))));
+  CAMLreturn(caml_copy_double((float)(Double_val(a) + Double_val(b))));
 }
 
 value ml_sub_flt(value a, value b)
 {
   CAMLparam2(a,b);
-  CAMLreturn(copy_double((float)(Double_val(a) - Double_val(b))));
+  CAMLreturn(caml_copy_double((float)(Double_val(a) - Double_val(b))));
 }
 
 value ml_mul_flt(value a, value b)
 {
   CAMLparam2(a,b);
-  CAMLreturn(copy_double((float)(Double_val(a) * Double_val(b))));
+  CAMLreturn(caml_copy_double((float)(Double_val(a) * Double_val(b))));
 }
 
 value ml_div_flt(value a, value b)
 {
   CAMLparam2(a,b);
-  CAMLreturn(copy_double((float)(Double_val(a) / Double_val(b))));
+  CAMLreturn(caml_copy_double((float)(Double_val(a) / Double_val(b))));
 }
 
 double ml_round_flt_f(double a)
@@ -76,7 +76,7 @@ double ml_round_flt_f(double a)
 value ml_round_flt(value a)
 {
   CAMLparam1(a);
-  CAMLreturn(copy_double((float)(Double_val(a))));
+  CAMLreturn(caml_copy_double((float)(Double_val(a))));
 }
 
 double ml_of_int_flt_f(value a)
@@ -86,5 +86,5 @@ double ml_of_int_flt_f(value a)
 value ml_of_int_flt(value a)
 {
   CAMLparam1(a);
-  CAMLreturn(copy_double((float)(Long_val(a))));
+  CAMLreturn(caml_copy_double((float)(Long_val(a))));
 }

cfgfrontend/dune

@@ -0,0 +1,18 @@
+(library
+ (name cfgfrontend)
+ (libraries zarith utils frontend)
+ (flags
+  (:standard -open Utils -open Frontend)))
+
+(ocamllex
+ (modules program_lexer))
+
+(menhir
+ (modules program_parser))
+
+;;(flags --explain))
+
+(env
+ (dev
+  (flags
+   (:standard -w -9-27-32-33-35 -warn-error -A))))

domains/dune

@@ -0,0 +1,11 @@
+(library
+ (name domains)
+ (libraries utils frontend banal apron apron.boxMPQ apron.octMPQ
+   apron.polkaMPQ)
+ (flags
+  (:standard -open Utils -open Banal -open Frontend -open Apron)))
+
+(env
+ (dev
+  (flags
+   (:standard -w -9-27-32-33-35 -warn-error -A))))

dune-project

@@ -0,0 +1,3 @@
+(lang dune 2.4) 
+( using menhir 2.0)
+(wrapped_executables false)

frontend/dune

@@ -0,0 +1,14 @@
+(library
+ (name frontend)
+ (libraries apron))
+
+(ocamllex
+ (modules Lexer PropertyLexer CTLPropertyLexer))
+
+(menhir
+ (modules Parser PropertyParser CTLPropertyParser))
+
+(env
+ (dev
+  (flags
+   (:standard -w -9-27-32-33-35 -warn-error -A))))

function.opam

@@ -0,0 +1,31 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "A short synopsis"
+description: "A longer description"
+maintainer: ["Maintainer Name"]
+authors: ["Author Name"]
+license: "LICENSE"
+tags: ["topics" "to describe" "your" "project"]
+homepage: "https://github.com/username/reponame"
+doc: "https://url/to/documentation"
+bug-reports: "https://github.com/username/reponame/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.6"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/username/reponame.git"

main/CFGInterpreter.ml

@@ -121,7 +121,7 @@ let execute
       let nodeProcessed = processed.(node.node_id) in
       if !trace then begin
         Format.fprintf !fmt "### processing node %d (iter: %d): \n" node.node_id nodeProcessed; 
-        Pervasives.print_newline ();
+        Stdlib.print_newline ();
       end;
       let isLoopHead = NodeMap.find node loop_heads in
       (* run abstract transformer for node to get new abstract state *)

main/dune

@@ -0,0 +1,14 @@
+(executable
+ (public_name main)
+ (name main)
+ (promote
+  (until-clean)
+  (into ..))
+ (flags
+  (:standard -open Frontend -open Domains -open Cfgfrontend -open Utils))
+ (libraries frontend cfgfrontend utils domains))
+
+(env
+ (dev
+  (flags
+   (:standard -w -9-27-32-33-35 -warn-error -A))))

utils/dune

@@ -0,0 +1,10 @@
+(library
+ (name utils)
+ (libraries frontend)
+ (flags
+  (:standard -open Frontend)))
+
+(env
+ (dev
+  (flags
+   (:standard -w -9-27-32-33-35 -warn-error -A))))