Skip to content

Commit

Permalink
naive_interpreter: Change the contract lock mechanism
Browse files Browse the repository at this point in the history
Signed-off-by: Delja <[email protected]>
  • Loading branch information
Delja committed Aug 4, 2020
1 parent 5a2bf16 commit fb893df
Showing 1 changed file with 16 additions and 0 deletions.
16 changes: 16 additions & 0 deletions src/interpreter/naive_interpreter.nit
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ private import parser::tables
import mixin
private import model::serialize_model
private import frontend::explain_assert_api
private import contracts

redef class ToolContext
# --discover-call-trace
Expand Down Expand Up @@ -74,6 +75,9 @@ class NaiveInterpreter
# Name of all supported functional names
var routine_types: Set[String] = new HashSet[String]

# Flag used to know if we are currently checking some assertions.
var in_assertion: Bool = false

init
do
if mainmodule.model.get_mclasses_by_name("Bool") != null then
Expand Down Expand Up @@ -1827,6 +1831,18 @@ redef class AIfexprExpr
end
end


redef class AIfInAssertion
redef fun stmt(v)
do
if not v.in_assertion then
v.in_assertion = true
v.stmt(self.n_body)
v.in_assertion = false
end
end
end

redef class ADoExpr
redef fun stmt(v)
do
Expand Down

0 comments on commit fb893df

Please sign in to comment.