diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 16:09:31 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 16:09:31 +0100 |
| commit | 52f602db7f306441cfa509cee7cce8cf8567ddc1 (patch) | |
| tree | 62b1e877d71eaf192aab6d9b26e91a65adf86aa2 /riscV/SelectOpproof.v | |
| parent | d2dc422b91ed628f0f8d6286a23f6f4fb9869248 (diff) | |
| download | compcert-kvx-52f602db7f306441cfa509cee7cce8cf8567ddc1.tar.gz compcert-kvx-52f602db7f306441cfa509cee7cce8cf8567ddc1.zip | |
adding builtins
Diffstat (limited to 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 1d13702a..1d713010 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -969,7 +969,10 @@ Theorem eval_platform_builtin: platform_builtin_sem bf vl = Some v -> exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. Proof. - intros. discriminate. + destruct bf; intros until le; intro Heval. + all: try (inversion Heval; subst a; clear Heval; + exists v; split; trivial; + repeat (try econstructor; try eassumption)). Qed. End CMCONSTR. |