From e0e6eb62dc0548e9a2c42a5a0afddc5a9407334e Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Thu, 16 Mar 2017 23:15:05 +0100
Subject: [PATCH] Fix a few compiler warnings
---
src/lib/CoAlgFormula.ml | 2 +-
src/lib/CoAlgMisc.ml | 7 ++++---
src/lib/CoAlgMisc.mli | 6 +++++-
src/lib/CoAlgReasoner.ml | 4 ++--
src/lib/FunctorParsing.ml | 4 ++--
src/lib/HashConsing.ml | 2 +-
src/lib/genAndComp.ml | 2 +-
src/lib/minisat.ml | 3 +++
8 files changed, 19 insertions(+), 11 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index dcc1856..f3d16e4 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -791,7 +791,7 @@ let rec verifyMuGuarded unguarded formula =
raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
let verifyFormula formula =
- verifyMuAltFree formula;
+ ignore (verifyMuAltFree formula);
verifyMuMonotone [] formula;
verifyMuGuarded [] formula
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 85d08bc..eb2e67b 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -575,7 +575,10 @@ let coreGetChildren core = core.childrenC
let coreAddChild core child = core.childrenC <- child::core.childrenC
let coreGetConstraints core = core.constraintsC
let coreSetConstraints core csets = core.constraintsC <- csets
-let coreGetSolver core = core.solver
+let coreGetSolver core =
+ match core.solver with
+ | Some solver -> solver
+ | None -> raise (Failure "Sat solver not allocated")
let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
let coreGetFht core = core.fht
let coreGetIdx (core:core) = core.idx
@@ -785,8 +788,6 @@ let stateToString (state:state): string =
(csetToString state.sortS cset):: lst
in
let constraints = cssFold helper state.constraintsS [] in
- let core2idx core = core.idx in
- let fst (a,b) = a in
let conclusionList =
List.map (fun (_,lst) ->
List.map (fun (core:core) -> string_of_int core.idx) lst
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index b93b94e..4c605ad 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -253,7 +253,11 @@ val coreGetChildren : core -> state list
val coreAddChild : core -> state -> unit
val coreGetConstraints : core -> csetSet
val coreSetConstraints : core -> csetSet -> unit
-val coreGetSolver : core -> Minisat.solver option
+
+(** Return minisat solver of a core, if allocated
+ @raise Failure if no solver is allocated for this core
+ *)
+val coreGetSolver : core -> Minisat.solver
val coreDeallocateSolver : core -> unit
val coreGetFht : core -> fht
val coreGetIdx : core -> int
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index efb1734..4898269 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -341,7 +341,7 @@ let rec propagateUnsat = function
if comesFromCnstr then coreGetBs core
else
let bs = coreGetBs core in
- let Some solver = coreGetSolver core in
+ let solver = coreGetSolver core in
let fht = coreGetFht core in
let lht = lhtInit () in
let addLits f acc =
@@ -817,7 +817,7 @@ let getNextState core =
in
let fht = coreGetFht core in
let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
- let Some solver = coreGetSolver core in
+ let solver = coreGetSolver core in
let isSat = M.invoke_solver solver litset in
(* Clearly, if the current core is unsatisfiable, no further child state can
be created *)
diff --git a/src/lib/FunctorParsing.ml b/src/lib/FunctorParsing.ml
index 23c4ce1..6671a89 100644
--- a/src/lib/FunctorParsing.ml
+++ b/src/lib/FunctorParsing.ml
@@ -24,10 +24,10 @@ let explode (s:string) : char list =
exp (String.length s - 1) [];;
let implode (l:char list) : string =
- let res = String.create (List.length l) in
+ let res = Bytes.create (List.length l) in
let rec imp i = function
| [] -> res
- | c :: l -> res.[i] <- c; imp (i + 1) l in
+ | c :: l -> Bytes.set res i c; imp (i + 1) l in
imp 0 l;;
let string_of_char : char -> string = String.make 1
diff --git a/src/lib/HashConsing.ml b/src/lib/HashConsing.ml
index 6b75c0b..f19d88d 100644
--- a/src/lib/HashConsing.ml
+++ b/src/lib/HashConsing.ml
@@ -211,7 +211,7 @@ module Make(H : HashedTyped) : (S with type nde = H.nde and type fml = H.fml) =
let idxN = hkeyN mod ds in
let bucketN = data.(idxN) in
try begin
- find ndeN bucketN;
+ ignore (find ndeN bucketN);
hc.size <- succ osize;
end
with Not_found ->
diff --git a/src/lib/genAndComp.ml b/src/lib/genAndComp.ml
index 7d5275d..b75b17e 100644
--- a/src/lib/genAndComp.ml
+++ b/src/lib/genAndComp.ml
@@ -832,7 +832,7 @@ let outputBenchmarks ?(filenameL = "out.tex") ?(filenameG = "plot") ?(filenameD
let t =
if ns = 1 then ts else if nu = 1 then tu else if nd = 1 then td else (assert false)
in
- if t < ft & (fs+fu+fd) = 0 then succ n else n
+ if t < ft && (fs+fu+fd) = 0 then succ n else n
in
List.map2 map2T acc sl
in
diff --git a/src/lib/minisat.ml b/src/lib/minisat.ml
index d98d989..4dd15a4 100644
--- a/src/lib/minisat.ml
+++ b/src/lib/minisat.ml
@@ -3,6 +3,9 @@ type lit = int
type solver
type litstatus = LTRUE | LFALSE | LUNDEF
+(* "noalloc" is deprecated in OCaml 4.03 and should be replaced by [@@noalloc]
+ once 4.03 becomes the minimum required version
+*)
external var_to_lit : var -> bool -> lit = "mkLit_stub" "noalloc"
external lit_to_var : lit -> var = "var_stub" "noalloc"
external sign : lit -> bool = "sign_stub" "noalloc"
--
GitLab