diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-07-24 11:42:09 +0200 |
| commit | a4570fed198034e535d0d6d99e23cfbb1d40b926 (patch) | |
| tree | e4e5a9dc845fc0972622ae05fd9084234ed9a44d /backend/CSE3analysisproof.v | |
| parent | 95f918c38b1e59f40ae7af455ec2c6746289375e (diff) | |
| parent | b5c4192c73d7b02e0c90354e26b35a84ee141083 (diff) | |
| download | compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.tar.gz compcert-kvx-a4570fed198034e535d0d6d99e23cfbb1d40b926.zip | |
Merge branch 'kvx-work' into rtl-tunneling
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index d53cf604..382c9f4c 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -502,7 +502,7 @@ Section SOUNDNESS. end with | Some dat => v' = dat - | None => v' = default_notrap_load_value chunk + | None => v' = Vundef end end. |