diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-07 09:25:53 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-06-07 09:25:53 +0200 |
| commit | 584eac7027cd4d29c5ca8744453ffeea8f18b501 (patch) | |
| tree | 374cd5c593eae420ff4e14e73de4c73709a6a87e /driver/Interp.ml | |
| parent | 9f30d4984863ec655a03996646805202dc2a07c9 (diff) | |
| download | compcert-kvx-584eac7027cd4d29c5ca8744453ffeea8f18b501.tar.gz compcert-kvx-584eac7027cd4d29c5ca8744453ffeea8f18b501.zip | |
Represent external worlds by a coinductive type rather than an inductive type.
As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case.
Diffstat (limited to 'driver/Interp.ml')
| -rw-r--r-- | driver/Interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Interp.ml b/driver/Interp.ml index b16d2cae..f453af95 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -402,7 +402,7 @@ let do_inline_assembly txt sg ge w args m = None (* Implementing external functions producing observable events *) let rec world ge m = - Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m) + lazy (Determinism.World(world_io ge m, world_vload ge m, world_vstore ge m)) and world_io ge m id args = None |