File tree Expand file tree Collapse file tree 3 files changed +5
-4
lines changed Expand file tree Collapse file tree 3 files changed +5
-4
lines changed Original file line number Diff line number Diff line change 22
33(test
44 (name mainTest)
5- (libraries ounit2 qcheck-ounit goblint.std goblint.lib goblint.sites.dune goblint.build-info.dune)
5+ (libraries ounit2 qcheck-ounit goblint.std goblint.lib goblint.constraint goblint.solver goblint. sites.dune goblint.build-info.dune)
66 (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
77 (flags :standard -linkall))
88
Original file line number Diff line number Diff line change @@ -2,6 +2,8 @@ open Goblint_lib
22open OUnit2
33open GoblintCil
44open Pretty
5+ open ConstrSys
6+ open Goblint_solver
57
68(* variables are strings *)
79module StringVar =
@@ -43,7 +45,7 @@ module ConstrSys = struct
4345 | _ -> None
4446
4547 let iter_vars _ _ _ _ _ = ()
46- let sys_change _ _ = {Analyses. obsolete = [] ; delete = [] ; reluctant = [] ; restart = [] }
48+ let sys_change _ _ = {obsolete = [] ; delete = [] ; reluctant = [] ; restart = [] }
4749end
4850
4951module LH = BatHashtbl. Make (ConstrSys. LVar )
5557 let should_warn = false
5658 let should_save_run = false
5759end
58- module Solver = Constraints. GlobSolverFromEqSolver (Constraints .EqIncrSolverFromEqSolver (EffectWConEq. Make ) (PostSolverArg )) (ConstrSys ) (LH ) (GH )
60+ module Solver = GlobSolverFromEqSolver (PostSolver .EqIncrSolverFromEqSolver (EffectWConEq. Make ) (PostSolverArg )) (ConstrSys ) (LH ) (GH )
5961
6062let test1 _ =
6163 let id x = x in
Original file line number Diff line number Diff line change 11open OUnit2
22open Goblint_std
3- open Goblint_lib
43
54(* If the first operand of a div is negative, Zarith rounds the result away from zero.
65 We thus always transform this into a division with a non-negative first operand. *)
You can’t perform that action at this time.
0 commit comments