diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/coq/pass/while_PP_terminating.sail | 2 | ||||
| -rw-r--r-- | test/coq/skip | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/coq/pass/while_PP_terminating.sail b/test/coq/pass/while_PP_terminating.sail index 00a4450b..80840ac9 100644 --- a/test/coq/pass/while_PP_terminating.sail +++ b/test/coq/pass/while_PP_terminating.sail @@ -11,3 +11,5 @@ function test n : int -> int = { }; j } + +termination_measure test while n - i diff --git a/test/coq/skip b/test/coq/skip index a4be9719..259df4b0 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -49,5 +49,3 @@ while_PM.sail while_PP.sail XXXXX Not yet - haven't decided whether to support register reads in measures while_MM_terminating.sail -XXXXX Not yet - haven't arranged for lifting pure loops into the monad (or proving termination outright) yet -while_PP_terminating.sail |