diff --git a/bin/dune b/bin/dune index c02e79b7..7b572c03 100644 --- a/bin/dune +++ b/bin/dune @@ -5,7 +5,7 @@ (modes exe byte) (modules asli) (flags (-cclib -lstdc++)) - (libraries libASL libASL_native linenoise pprint) + (libraries asli.libASL linenoise pprint) ) (executable @@ -14,7 +14,7 @@ (modes exe) (modules server) (flags (-cclib -lstdc++)) - (libraries libASL libASL_native pprint lwt.unix yojson cohttp-lwt cohttp-lwt-unix)) + (libraries asli.libASL pprint lwt.unix yojson cohttp-lwt cohttp-lwt-unix)) (executable @@ -23,7 +23,7 @@ ; (public_name test_asl_lexer) (modules testlexer) (flags (-cclib -lstdc++)) - (libraries libASL)) + (libraries asli.libASL)) (executable (name processops) @@ -31,7 +31,7 @@ ; (public_name test_asl_lexer) (modules processops) (flags (-cclib -lstdc++)) - (libraries libASL unix)) + (libraries asli.libASL unix)) (executable (name offline_coverage) @@ -39,7 +39,7 @@ (modes exe) (modules offline_coverage) (flags (-cclib -lstdc++)) - (libraries libASL libASL_native offlineASL)) + (libraries asli.libASL offlineASL)) (executable (name offline_sem) @@ -47,4 +47,4 @@ (modes exe) (modules offline_sem) (flags (-cclib -lstdc++)) - (libraries libASL libASL_native offlineASL)) + (libraries asli.libASL offlineASL)) diff --git a/libASL/dune b/libASL/dune index 1ca4d24a..7282ac08 100644 --- a/libASL/dune +++ b/libASL/dune @@ -15,18 +15,17 @@ (with-stdout-to asl_parser.mly (run cat asl_parser_head.mly asl_parser_tail.mly))))) (library - (name libASL_ast) - (public_name asli.libASL-ast) + (name libASL_base) + (public_name asli.libASL-base) (flags (:standard -w -27)) - (wrapped false) (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor visitor utils) (libraries pprint (re_export zarith))) (library - (name libASL) - (public_name asli.libASL) + (name libASL_virtual) + (public_name asli.libASL-virtual) (flags - (:standard -w -27 -cclib -lstdc++)) + (:standard -w -27 -cclib -lstdc++ -open LibASL_base)) (modules cpu dis elf eval lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value symbolic_lifter decoder_program call_graph req_analysis @@ -35,5 +34,17 @@ ) (preprocessor_deps (alias ../asl_files)) (preprocess (pps ppx_blob)) - (libraries libASL_support (re_export libASL_ast) str)) + (libraries libASL_support str)) +(library + (name libASL) + (public_name asli.libASL-merged) + (modules libASL) + (wrapped false) + (libraries libASL_virtual libASL_base)) + +(library + (name libASL_dummy) + (public_name asli.libASL) + (modules) + (libraries (re_export libASL) libASL_native)) diff --git a/libASL/libASL.ml b/libASL/libASL.ml new file mode 100644 index 00000000..7130e4ef --- /dev/null +++ b/libASL/libASL.ml @@ -0,0 +1,2 @@ +include LibASL_base +include LibASL_virtual diff --git a/libASL/support/dune b/libASL/support/dune index 4d907e49..aed79f34 100644 --- a/libASL/support/dune +++ b/libASL/support/dune @@ -3,5 +3,5 @@ (library (name libASL_support) (public_name asli.libASL-support) - (libraries libASL_ast) + (libraries libASL_base) (virtual_modules solver)) diff --git a/libASL/support/native/dune b/libASL/support/native/dune index f01935ce..7df5046b 100644 --- a/libASL/support/native/dune +++ b/libASL/support/native/dune @@ -1,4 +1,5 @@ (library (name libASL_native) + (public_name asli.libASL-support-native) (implements libASL_support) - (libraries z3 libASL_ast)) + (libraries z3 libASL_base)) diff --git a/libASL/support/native/solver.ml b/libASL/support/native/solver.ml index 7870f10b..acac8cd9 100644 --- a/libASL/support/native/solver.ml +++ b/libASL/support/native/solver.ml @@ -17,7 +17,8 @@ we can reason that "F(x) == F(x)" without knowing "F". *) -module AST = Asl_ast +module AST = LibASL_base.Asl_ast +module Asl_utils = LibASL_base.Asl_utils let verbose = false diff --git a/libASL/support/solver.mli b/libASL/support/solver.mli index 759dcce3..764ae71a 100644 --- a/libASL/support/solver.mli +++ b/libASL/support/solver.mli @@ -3,4 +3,4 @@ (****************************************************************) (** check that bs => cs *) -val check_constraints : (Asl_ast.expr list) -> (Asl_ast.expr list) -> bool +val check_constraints : (LibASL_base.Asl_ast.expr list) -> (LibASL_base.Asl_ast.expr list) -> bool diff --git a/libASL/support/web/dune b/libASL/support/web/dune index 380dcf39..b69b8598 100644 --- a/libASL/support/web/dune +++ b/libASL/support/web/dune @@ -2,4 +2,4 @@ (name libASL_web) (public_name asli.libASL-web) (implements libASL_support) - (libraries libASL_ast zarith_stubs_js)) + (libraries libASL_base zarith_stubs_js)) diff --git a/libASL/support/web/solver.ml b/libASL/support/web/solver.ml index fa6b9717..111ee86e 100644 --- a/libASL/support/web/solver.ml +++ b/libASL/support/web/solver.ml @@ -1,4 +1,4 @@ -module AST = Asl_ast +module AST = LibASL_base.Asl_ast let check_constraints (_bs: AST.expr list) (_cs: AST.expr list): bool = true