File tree Expand file tree Collapse file tree 1 file changed +16
-0
lines changed
Expand file tree Collapse file tree 1 file changed +16
-0
lines changed Original file line number Diff line number Diff line change @@ -23,6 +23,7 @@ private import parser::tables
2323import mixin
2424private import model ::serialize_model
2525private import frontend ::explain_assert_api
26+ private import contracts
2627
2728redef class ToolContext
2829 # --discover-call-trace
@@ -74,6 +75,9 @@ class NaiveInterpreter
7475 # Name of all supported functional names
7576 var routine_types : Set [String ] = new HashSet [String ]
7677
78+ # Flag used to know if we are currently checking some assertions.
79+ var in_assertion : Bool = false
80+
7781 init
7882 do
7983 if mainmodule .model .get_mclasses_by_name ("Bool " ) != null then
@@ -1827,6 +1831,18 @@ redef class AIfexprExpr
18271831 end
18281832end
18291833
1834+
1835+ redef class AIfInAssertion
1836+ redef fun stmt (v )
1837+ do
1838+ if not v .in_assertion then
1839+ v .in_assertion = true
1840+ v .stmt (self .n_body )
1841+ v .in_assertion = false
1842+ end
1843+ end
1844+ end
1845+
18301846redef class ADoExpr
18311847 redef fun stmt (v )
18321848 do
You can’t perform that action at this time.
0 commit comments