diff options
| author | Son Ho | 2022-01-04 22:00:36 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-04 22:00:36 +0100 |
| commit | 6ca4bee9d52a2d9c9e246ef8116121d9018ca101 (patch) | |
| tree | 661df65901ed345edd80ca4fb7f5a3a9a86fab3d | |
| parent | 8bc864615eb8dccfe57f4c783beca82ae2586d5a (diff) | |
| parent | 91ada7cb0e03244a8624773baedb96d3c03f8998 (diff) | |
Merge branch 'main' of github.com:Kachoc/aeneas into main
Diffstat (limited to '')
| -rw-r--r-- | src/Invariants.ml | 6 | ||||
| -rw-r--r-- | src/Modules.ml | 4 |
2 files changed, 1 insertions, 9 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index 08ae6b4a..b67fa3a2 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -3,15 +3,11 @@ module T = Types module V = Values -open Scalars module E = Expressions -open Errors module C = Contexts module Subst = Substitute module A = CfimAst module L = Logging -open TypesUtils -open ValuesUtils open InterpreterUtils let debug_invariants : bool ref = ref false @@ -337,7 +333,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = let info = { outer_borrow = false; outer_shared = false } in visitor#visit_eval_ctx info ctx -let check_typing_invariant (ctx : C.eval_ctx) : unit = () +let check_typing_invariant (_ctx : C.eval_ctx) : unit = () let check_invariants (ctx : C.eval_ctx) : unit = check_loans_borrows_relation_invariant ctx; diff --git a/src/Modules.ml b/src/Modules.ml index 3be1c742..5b76880f 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -1,9 +1,5 @@ open Yojson.Basic -open Identifiers open Types -open OfJsonBasic -open Scalars -open Values open CfimAst (** Module declaration *) |